Duskin's Monadicity Theorem

src/Cat/Diagram/Coequaliser/Split.lagda.md

@@ -0,0 +1,203 @@
+```agda
+open import Cat.Prelude
+
+module Cat.Diagram.Coequaliser.Split {o ℓ} (C : Precategory o ℓ) where
+open import Cat.Diagram.Coequaliser C
+```
+
+<!--
+```agda
+open import Cat.Reasoning C
+private variable
+  A B E : Ob
+  f g h e s t : Hom A B
+```
+-->
+
+# Split Coequalizers
+
+Split Coequalizers are one of those definitions that seem utterly opaque when first
+presented, but are actually quite natural when viewed through the correct lens.
+With this in mind, we are going to provide the motivation _first_, and then
+define the general construct.
+
+To start, let $R \subseteq B \times B$ be some equivalence relation. A natural thing
+to consider is the quotient $B/R$, which gives us the following diagram:
+~~~{.quiver}
+\[\begin{tikzcd}
+	R & {B \times B} & B & {B/R}
+	\arrow[hook, from=1-1, to=1-2]
+	\arrow["{p_1}", shift left=2, from=1-2, to=1-3]
+	\arrow["{p_2}"', shift right=2, from=1-2, to=1-3]
+	\arrow["q", from=1-3, to=1-4]
+\end{tikzcd}\]
+~~~
+
+Now, when one has a quotient, it's useful to have a means of picking representatives
+for each equivalence class. This is essentially what normalization algorithms do,
+which we can both agree are very useful indeed. This ends up defining a map
+$s : B/R \to B$ that is a section of $q$ (i.e: $q \circ s = id$).
+
+This gives us the following diagram (We've omited the injection of $R$ into
+$B \times B$ for clarity).
+~~~{.quiver}
+\[\begin{tikzcd}
+	R & B & {B/R}
+	\arrow["q", shift left=2, from=1-2, to=1-3]
+	\arrow["s", shift left=2, from=1-3, to=1-2]
+	\arrow["{p_1}", shift left=2, from=1-1, to=1-2]
+	\arrow["{p_2}"', shift right=2, from=1-1, to=1-2]
+\end{tikzcd}\]
+~~~
+
+This lets us define yet another map $r : B \to R$, which will witness the fact that
+any $b : B$ is related to its representative $s(q(b))$. We can define this map explicitly
+as so:
+$$
+  r(b) = (b, s(q(b)))
+$$
+
+Now, how do we encode this diagramatically? To start, $p_1 \circ r = id$ by the
+$\beta$ law for products. Furthermore, $p_2 \circ r = s \circ q$, also by the
+$\beta$ law for products. This gives us a diagram that captures the essence of having
+a quotient by an equivalence relation, along with a means of picking representatives.
+
+~~~{.quiver}
+\[\begin{tikzcd}
+	R & B & {B/R}
+	\arrow["q", shift left=2, from=1-2, to=1-3]
+	\arrow["s", shift left=2, from=1-3, to=1-2]
+	\arrow["{p_1}", shift left=5, from=1-1, to=1-2]
+	\arrow["{p_2}"', shift right=5, from=1-1, to=1-2]
+	\arrow["r"', from=1-2, to=1-1]
+\end{tikzcd}\]
+~~~
+
+Such a situation is called a **split coequaliser**.
+
+```agda
+record is-split-coequaliser (f g : Hom A B) (e : Hom B E)
+                            (s : Hom E B) (t : Hom B A) : Type (o ⊔ ℓ) where
+  field
+    coequal : e ∘ f ≡ e ∘ g
+    rep-section : e ∘ s ≡ id
+    witness-section : f ∘ t ≡ id
+    commute : s ∘ e ≡ g ∘ t
+```
+
+Now, let's show that this thing actually deserves the name Coequaliser.
+```agda
+is-split-coequaliser→is-coequalizer :
+  is-split-coequaliser f g e s t → is-coequaliser f g e
+is-split-coequaliser→is-coequalizer
+  {f = f} {g = g} {e = e} {s = s} {t = t} split-coeq =
+  coequalizes
+  where
+    open is-split-coequaliser split-coeq
+```
+
+The proof here is mostly a diagram shuffle. We construct the universal
+map by going back along $s$, and then following $e'$ to our destination,
+like so:
+
+~~~{.quiver}
+\[\begin{tikzcd}
+	A && B && E \\
+	\\
+	&&&& X
+	\arrow["q", shift left=2, from=1-3, to=1-5]
+	\arrow["s", shift left=2, from=1-5, to=1-3]
+	\arrow["{p_1}", shift left=5, from=1-1, to=1-3]
+	\arrow["{p_2}"', shift right=5, from=1-1, to=1-3]
+	\arrow["r"', from=1-3, to=1-1]
+	\arrow["{e'}", from=1-3, to=3-5]
+	\arrow["{e' \circ s}", color={rgb,255:red,214;green,92;blue,92}, from=1-5, to=3-5]
+\end{tikzcd}\]
+~~~
+
+```agda
+    coequalizes : is-coequaliser f g e
+    coequalizes .is-coequaliser.coequal = coequal
+    coequalizes .is-coequaliser.coequalise {e′ = e′} _ = e′ ∘ s
+    coequalizes .is-coequaliser.universal {e′ = e′} {p = p} =
+      (e′ ∘ s) ∘ e ≡⟨ extendr commute ⟩
+      (e′ ∘ g) ∘ t ≡˘⟨ p ⟩∘⟨refl ⟩
+      (e′ ∘ f) ∘ t ≡⟨ cancelr witness-section ⟩
+      e′           ∎
+    coequalizes .is-coequaliser.unique {e′ = e′} {p} {colim′} q =
+      colim′         ≡⟨ intror rep-section ⟩
+      colim′ ∘ e ∘ s ≡⟨ pulll (sym q) ⟩
+      e′ ∘ s         ∎
+```
+
+Intuitively, we can think of this as constructing a map out of the quotient $B/R$
+from a map out of $B$ by picking a representative, and then applying the map out
+of $B$. Universality follows by the fact that the representative is related to
+the original element of $B$, and uniqueness by the fact that $s$ is a section.
+
+```agda
+record Split-coequaliser (f g : Hom A B) : Type (o ⊔ ℓ) where
+  field
+    {coapex}  : Ob
+    coeq      : Hom B coapex
+    rep       : Hom coapex B
+    witness   : Hom B A
+    has-is-split-coeq : is-split-coequaliser f g coeq rep witness
+
+  open is-split-coequaliser has-is-split-coeq public
+```
+
+## Split coequalizers and split epimorphisms
+
+Much like the situation with coequalizers, the coequalizing map of a
+split coequalizer is a split epimorphism. This follows directly from the fact
+that $s$ is a section of $e$.
+
+```agda
+is-split-coequaliser→is-split-epic
+  : is-split-coequaliser f g e s t → is-split-epic e
+is-split-coequaliser→is-split-epic {e = e} {s = s} split-coeq =
+  split-epic
+  where
+    open is-split-epic
+    open is-split-coequaliser split-coeq
+
+    split-epic : is-split-epic e
+    split-epic .split = s
+    split-epic .section = rep-section
+```
+
+Also of note, if $e$ is a split epimorphism with splitting $s$, then
+the following diagram is a split coequalizer.
+~~~{.quiver}
+\[\begin{tikzcd}
+	A & A & B
+	\arrow["id", shift left=3, from=1-1, to=1-2]
+	\arrow["{s \circ e}"', shift right=3, from=1-1, to=1-2]
+	\arrow["id"{description}, from=1-2, to=1-1]
+	\arrow["e", shift left=1, from=1-2, to=1-3]
+	\arrow["s", shift left=2, from=1-3, to=1-2]
+\end{tikzcd}\]
+~~~
+
+Using the intuition that split coequalizers are quotients of equivalence relations
+equipped with a choice of representatives, we can decode this diagram as constructing
+an equivalence relation on $A$ out of a section of $e$, where $a ~ b$ if and only
+if they get taken to the same cross section of $A$ via $s \circ e$.
+
+```agda
+is-split-epic→is-split-coequalizer
+  : s is-section-of e → is-split-coequaliser id (s ∘ e) e s id
+is-split-epic→is-split-coequalizer {s = s} {e = e} section = split-coeq
+  where
+    open is-split-coequaliser
+
+    split-coeq : is-split-coequaliser id (s ∘ e) e s id
+    split-coeq .coequal =
+      e ∘ id    ≡⟨ idr e ⟩
+      e         ≡⟨ insertl section ⟩
+      e ∘ s ∘ e ∎
+    split-coeq .rep-section = section
+    split-coeq .witness-section = id₂
+    split-coeq .commute = sym (idr (s ∘ e))
+```

src/Cat/Diagram/Coequaliser/Split/Properties.lagda.md

@@ -0,0 +1,153 @@
+```agda
+open import Cat.Prelude
+
+open import Cat.Diagram.Limit.Finite
+
+import Cat.Diagram.Coequaliser.Split as SplitCoeq
+import Cat.Diagram.Pullback
+import Cat.Diagram.Congruence
+import Cat.Reasoning
+import Cat.Functor.Reasoning
+
+module Cat.Diagram.Coequaliser.Split.Properties where
+```
+
+# Properties of split coequalizers
+
+This module proves some general properties of [split coequalisers].
+
+[split coequalisers]: Cat.Diagram.Coequaliser.Split.html
+
+## Absoluteness
+
+The property of being a split coequaliser is a purely diagrammatic one, which has
+the lovely property of being preserved by _all_ functors. We call such colimits
+**absolute**.
+
+```agda
+module _ {o o′ ℓ ℓ′}
+         {C : Precategory o ℓ} {D : Precategory o′ ℓ′}
+         (F : Functor C D) where
+```
+<!--
+```agda
+  private
+    module C = Cat.Reasoning C
+    module D = Cat.Reasoning D
+    open Cat.Functor.Reasoning F
+    open SplitCoeq
+    variable
+      A B E : C.Ob 
+      f g e s t : C.Hom A B
+```
+-->
+
+The proof follows the fact that functors preserve diagrams, and reduces to a bit
+of symbol shuffling.
+
+```agda
+  is-split-coequaliser-absolute
+    : is-split-coequaliser C f g e s t
+    → is-split-coequaliser D (F₁ f) (F₁ g) (F₁ e) (F₁ s) (F₁ t)
+  is-split-coequaliser-absolute
+    {f = f} {g = g} {e = e} {s = s} {t = t} split-coeq = F-split-coeq
+    where
+      open is-split-coequaliser split-coeq
+
+      F-split-coeq : is-split-coequaliser D _ _ _ _ _
+      F-split-coeq .coequal = weave coequal
+      F-split-coeq .rep-section = annihilate rep-section
+      F-split-coeq .witness-section = annihilate witness-section
+      F-split-coeq .commute = weave commute
+```
+
+## Congruences and Quotients
+
+When motivating split coequalisers, we discussed how they arise naturally from
+quotients equipped with a choice of representatives of equivalence classes.
+Let's go the other direction, and show that split coequalizers induce [quotients].
+The rough idea of the construction is that we can construct an idempotent $A \to A$
+that takes every $a : A$ to it's canonical representative, and then to take
+the kernel pair of that morphism to construct a congruence.
+
+[quotients]: Cat.Diagram.Congruence.html#quotient-objects
+[kernel pair]: Cat.Diagram.Congruence.html#quotient-objects
+
+```agda
+module _ {o ℓ}
+         {C : Precategory o ℓ}
+         (fc : Finitely-complete C)
+         where
+```
+
+<!--
+```agda
+  open Cat.Reasoning C
+  open Cat.Diagram.Pullback C
+  open Cat.Diagram.Congruence fc
+  open SplitCoeq C
+  open Finitely-complete fc
+  open Cart
+```
+-->
+
+```agda
+  split-coequaliser→is-quotient-of 
+    : ∀ {R A A/R} {i r : Hom R A} {q : Hom A A/R}
+        {rep : Hom A/R A} {witness : Hom A R}
+      → is-split-coequaliser i r q rep witness
+      → is-quotient-of (Kernel-pair (r ∘ witness)) q
+  split-coequaliser→is-quotient-of
+    {i = i} {r = r} {q = q} {rep = rep} {witness = witness} split-coeq =
+    is-split-coequaliser→is-coequalizer quotient-split
+      where
+        open is-split-coequaliser split-coeq
+        module R′ = Pullback (pullbacks (r ∘ witness) (r ∘ witness))
+```
+
+We will need to do a bit of symbol munging to get the right split coequaliser here,
+as the morphisms don't precisely line up due to the fact that we want to be working
+with the kernel pair, not `R`.
+
+However, we first prove a small helper lemma. If we use the intuition of `R`
+as a set of pairs of elements and their canonical representatives, then this
+lemma states that the representative of $a : A$ is the same as the representative _of_
+the representative of $a$.
+
+```agda
+        same-rep : (r ∘ witness) ∘ i ≡ (r ∘ witness) ∘ r
+        same-rep =
+          (r ∘ witness) ∘ i ≡˘⟨ commute ⟩∘⟨refl ⟩
+          (rep ∘ q) ∘ i     ≡⟨ extendr coequal ⟩
+          (rep ∘ q) ∘ r     ≡⟨ commute ⟩∘⟨refl ⟩
+          (r ∘ witness) ∘ r ∎
+```
+
+Now, onto the meat of the proof. This is mostly mindless algebraic manipulation
+to get things to line up correctly.
+
+```agda
+        quotient-split :
+          is-split-coequaliser
+            (π₁ ∘ ⟨ R′.p₁ , R′.p₂ ⟩) (π₂ ∘ ⟨ R′.p₁ , R′.p₂ ⟩)
+            q rep (R′.limiting same-rep ∘ witness)
+        quotient-split .coequal = retract→is-monic rep-section _ _ $
+          rep ∘ q ∘ π₁ ∘ ⟨ R′.p₁ , R′.p₂ ⟩ ≡⟨ refl⟩∘⟨ refl⟩∘⟨ π₁∘⟨⟩ ⟩
+          rep ∘ q ∘ R′.p₁                  ≡⟨ pulll commute ⟩
+          (r ∘ witness) ∘ R′.p₁            ≡⟨ R′.square ⟩
+          (r ∘ witness) ∘ R′.p₂            ≡⟨ pushl (sym commute) ⟩
+          rep ∘ q ∘ R′.p₂                  ≡˘⟨ refl⟩∘⟨ refl⟩∘⟨ π₂∘⟨⟩ ⟩
+          rep ∘ q ∘ π₂ ∘ ⟨ R′.p₁ , R′.p₂ ⟩ ∎
+        quotient-split .rep-section = rep-section
+        quotient-split .witness-section =
+          (π₁ ∘ ⟨ R′.p₁ , R′.p₂ ⟩) ∘ R′.limiting same-rep ∘ witness ≡⟨ π₁∘⟨⟩ ⟩∘⟨refl ⟩
+          R′.p₁ ∘ R′.limiting same-rep ∘ witness                    ≡⟨ pulll R′.p₁∘limiting ⟩
+          i ∘ witness                                               ≡⟨ witness-section ⟩
+          id ∎
+        quotient-split .commute =
+          rep ∘ q                                                   ≡⟨ commute ⟩
+          r ∘ witness                                               ≡⟨ pushl (sym R′.p₂∘limiting) ⟩
+          R′.p₂ ∘ R′.limiting same-rep ∘ witness                    ≡˘⟨ π₂∘⟨⟩ ⟩∘⟨refl ⟩
+          (π₂ ∘ ⟨ R′.p₁ , R′.p₂ ⟩) ∘ R′.limiting same-rep ∘ witness ∎
+```
+

src/Cat/Diagram/Limit/Finite.lagda.md

@@ -72,8 +72,8 @@ to give a terminal object and binary products.
     Pb : ∀ {A B C} (f : Hom A C) (g : Hom B C) → Ob
     Pb f g = pullbacks f g .Pullback.apex
 
-    module Cart = Cartesian C products
-    open Cart using (_⊗_) public
+    module Cart = Cartesian C products hiding (_⊗_)
+    open Cartesian C products using (_⊗_) public
 
   open Finitely-complete
 ```