From f5702e9303558eb7281415205f7190d32cc6e452 Mon Sep 17 00:00:00 2001
From: Garrett Figueroa <garrett.figueroa@gmail.com>
Date: Thu, 14 Nov 2024 09:15:57 -0700
Subject: [PATCH] Incidence algebras (#1221)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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 <e.m.rijke@gmail.com>
---
 src/order-theory.lagda.md                    |  1 +
 src/order-theory/incidence-algebras.lagda.md | 49 ++++++++++++++++++++
 src/order-theory/interval-subposets.lagda.md | 24 ++++++++++
 3 files changed, 74 insertions(+)
 create mode 100644 src/order-theory/incidence-algebras.lagda.md

diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md
index 1de24c0872..55ffbd3d3f 100644
--- a/src/order-theory.lagda.md
+++ b/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
diff --git a/src/order-theory/incidence-algebras.lagda.md b/src/order-theory/incidence-algebras.lagda.md
new file mode 100644
index 0000000000..3ce4a89e69
--- /dev/null
+++ b/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.
diff --git a/src/order-theory/interval-subposets.lagda.md b/src/order-theory/interval-subposets.lagda.md
index 6788934942..4cd0f385a6 100644
--- a/src/order-theory/interval-subposets.lagda.md
+++ b/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)
+```