Incidence algebras (#1221)

Very preliminary work on defining the incidence algebra of a locally
finite poset, as towards defining more sophisticated objects such as
Möbius inversion. Work stalled pending infrastructure in the commutative
algebra library for "unordered" addition indexed by finite sets and for
some module theory, but want to get this file with a thumbtack in the
upstream before turning that way.

---------

Co-authored-by: Egbert Rijke <[email protected]>

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)
+```