Incidence algebras

src/order-theory.lagda.md

@@ -49,6 +49,7 @@ open import order-theory.homomorphisms-meet-semilattices public
 open import order-theory.homomorphisms-meet-sup-lattices public
 open import order-theory.homomorphisms-sup-lattices public
 open import order-theory.ideals-preorders public
+open import order-theory.incidence-algebras public
 open import order-theory.inhabited-finite-total-orders public
 open import order-theory.interval-subposets public
 open import order-theory.join-semilattices public

src/order-theory/incidence-algebras.lagda.md

@@ -0,0 +1,49 @@
+# Incidence algebras
+
+```agda
+module order-theory.incidence-algebras where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+
+open import foundation.dependent-pair-types
+open import foundation.inhabited-types
+open import foundation.universe-levels
+
+open import foundation-core.cartesian-product-types
+
+open import order-theory.interval-subposets
+open import order-theory.locally-finite-posets
+open import order-theory.posets
+```
+
+</details>
+
+## Idea
+
+For a [locally finite poset](order-theory.locally-finite-posets.md) 'P' and
+[commutative ring](commutative-algebra.commutative-rings.md) 'R', there is a
+canonical 'R'-associative algebra whose underlying 'R'-module are the set-maps
+from the nonempty [intervals](order-theory.interval-subposets.md) of 'P' to 'R'
+(which we constructify as the inhabited intervals), and whose multiplication is
+given by a "convolution" of maps. This is the **incidence algebra** of 'P' over
+'R'.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level} (P : Poset l1 l2) (loc-fin : is-locally-finite-Poset P)
+  (x y : type-Poset P) (R : Commutative-Ring l3)
+  where
+
+  interval-map : UU (l1 ⊔ l2 ⊔ l3)
+  interval-map = inhabited-interval P → type-Commutative-Ring R
+```
+
+WIP: complete this definition after _R-modules_ have been defined. Defining
+convolution of maps would be aided as well with a lemma on 'unordered' addition
+in abelian groups over finite sets.

src/order-theory/interval-subposets.lagda.md

@@ -7,9 +7,13 @@ module order-theory.interval-subposets where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.dependent-pair-types
+open import foundation.inhabited-types
 open import foundation.propositions
 open import foundation.universe-levels
 
+open import foundation-core.cartesian-product-types
+
 open import order-theory.posets
 open import order-theory.subposets
 ```
@@ -36,3 +40,23 @@ module _
   poset-interval-Subposet : Poset (l1 ⊔ l2) l2
   poset-interval-Subposet = poset-Subposet X is-in-interval-Poset
 ```
+
+### The predicate of an interval being inhabited
+
+```agda
+module _
+  {l1 l2 : Level} (X : Poset l1 l2) (x y : type-Poset X)
+  where
+
+  is-inhabited-interval : UU (l1 ⊔ l2)
+  is-inhabited-interval =
+    is-inhabited (type-Poset (poset-interval-Subposet X x y))
+
+module _
+  {l1 l2 : Level} (X : Poset l1 l2)
+  where
+
+  inhabited-interval : UU (l1 ⊔ l2)
+  inhabited-interval =
+    Σ (type-Poset X × type-Poset X) λ (p , q) → (is-inhabited-interval X p q)
+```