From 690eaf5ef99ad09ea7b2f143dc0d8c236c8591bb Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Sat, 13 Apr 2024 16:10:42 -0400 Subject: [PATCH] prose: more prose tweaks --- src/Cat/Instances/Simplex.lagda.md | 108 +++++++++++++++++++---------- 1 file changed, 70 insertions(+), 38 deletions(-) diff --git a/src/Cat/Instances/Simplex.lagda.md b/src/Cat/Instances/Simplex.lagda.md index e98d7fbf9..049ad7811 100644 --- a/src/Cat/Instances/Simplex.lagda.md +++ b/src/Cat/Instances/Simplex.lagda.md @@ -102,8 +102,15 @@ data Δ-Hom⁺ : Nat → Nat → Type where ``` For instance, the map $\delta_{0} \circ \delta_{2} : [2] \to [4]$ -would be written as `shift⁺ (keep⁺ (keep⁺ (shift⁺ done⁺)))`{.Agda}: the -first `shift⁺`{.Agda} denotes the postcomposition of the 0th face maps, +would be written as: + +```agda +private + δ₀∘δ₂ : Δ-Hom⁺ 2 4 + δ₀∘δ₂ = shift⁺ (keep⁺ (keep⁺ (shift⁺ done⁺))) +``` + +The first `shift⁺`{.Agda} denotes the postcomposition of the 0th face maps, and the 2 `keep⁺`{.Agda} constructors bump up the index of the next face map by 2. This means that the final `shift⁺`{.Agda} denotes the 4th face map! @@ -121,8 +128,15 @@ data Δ-Hom⁻ : Nat → Nat → Type where ``` As an example, the map $\sigma_{2} \circ \sigma_{0} : [5] \to [3]$ would -be written as `crush⁻ (keep⁻ (keep⁻ (crush⁻ (keep⁻ done⁻))))`{.Agda}. Here, -the outermost `crush⁻` constructor denotes the precomposition by $\sigma_{0}$. +be written as: + +```agda +private + σ₂∘σ₀ : Δ-Hom⁻ 5 3 + σ₂∘σ₀ = crush⁻ (keep⁻ (keep⁻ (crush⁻ (keep⁻ done⁻)))) +``` + +Here, the outermost `crush⁻` constructor denotes the precomposition by $\sigma_{0}$. Next, the two `keep⁻`{.Agda} constructors bump the index of the next face map we encounter up by 2, so the final `crush⁻` constructor denotes the 2nd degeneracy map. @@ -243,7 +257,10 @@ f ∘⁺ done⁺ = f ``` Next, the composite $(\delta_0 \circ f) \circ (\delta_0 \circ g)$ -can be written in normal form by reassociating as $\delta_0 \circ (f \circ (\delta_0 \circ g))$ +can be written in normal form by reassociating as +$$ +\delta_0 \circ (f \circ (\delta_0 \circ g)) +$$ and then recursively normalizing the right-hand side. ```agda @@ -254,18 +271,23 @@ Now for the tricky case: consider the composite $\uparrow f \circ (\delta_0 \cir where $\uparrow f$ shifts the index of every face map in $f$ by 1. This means that we can repeatedly apply the 1st simplicial identity to commute $\delta_{0}$ past every single face map in $f$ by lowering their -indices by one. This yields the following equality, which we will bake -directly into the definition of composition. +indices by one. This yields the following equality $$ \uparrow f \circ (\delta_0 \circ g) = \delta_0 \circ (f \circ g) $$ +and the right-hand side can be placed into normal form by normalizing +$f \circ g$. ```agda keep⁺ f ∘⁺ shift⁺ g = shift⁺ (f ∘⁺ g) ``` Luckily, the dual case is much easier: the composite $(\delta_0 \circ f) \circ \uparrow g$ -can be written in our normal form as $\delta_0 \circ (f \circ \uparrow g)$. +can directly be reassociated as +$$ +\delta_0 \circ (f \circ \uparrow g) +$$ +We can then recursively normalize the right hand side to obtain a normal form. ```agda shift⁺ f ∘⁺ keep⁺ g = shift⁺ (f ∘⁺ keep⁺ g) @@ -277,20 +299,24 @@ Finally, $\uparrow f \circ \uparrow g = \uparrow (f \circ g)$. keep⁺ f ∘⁺ keep⁺ g = keep⁺ (f ∘⁺ g) ``` -Composing demisimplicial maps follows a similar process. +Composing demisimplicial maps follows a similar process, though it is +slightly trickier. ```agda _∘⁻_ : Δ-Hom⁻ n o → Δ-Hom⁻ m n → Δ-Hom⁻ m o ``` -Precomposing $g$ with the identity map $[0] \to [0]$ just yields $g$. +As before, precomposing $g$ with the identity map $[0] \to [0]$ just yields $g$. ```agda done⁻ ∘⁻ g = g ``` Next, $(f \circ \sigma_0) \circ (g \circ \sigma_0)$ can be written -in our normal form by reassociating as $(f \circ \sigma_0) \circ g) \circ \sigma_0$ +in our normal form by reassociating it as +$$ +(f \circ \sigma_0) \circ g) \circ \sigma_0 +$$ and then recursively normalizing the left-hand side. ```agda @@ -301,12 +327,12 @@ Our first tricky case is when we encounter a composite of the form $(f \circ \sigma_0) \circ (\uparrow g \circ \sigma_1)$. Every degeneracy in $\uparrow g$ must have an index of at least $1$, so we can apply the 2nd simplicial identity to commute the 0th face map past them -by lowering all indices by 1. This yields the following equation, -which we will use definitionally: +by lowering all indices by 1. This yields the following equation $$ (f \circ \sigma_0) \circ (\uparrow g \circ \sigma_1) = (f \circ g) \circ \sigma_0 \circ \sigma_0 $$ - +If we recursively normalize $f \circ g$, then the RHS of this equation will +be in normal form! ```agda crush⁻ f ∘⁻ keep⁻ (crush⁻ g) = crush⁻ (crush⁻ (f ∘⁻ g)) @@ -341,9 +367,10 @@ keep⁻ f ∘⁻ keep⁻ g = keep⁻ (f ∘⁻ g) Composites of simplicial maps are even more tricky, as we need to somehow normalize a string of maps $f^{+} \circ f^{-} \circ g^{+} \circ g^{-}$ into a pair of a semisimplicial and demisimplicial maps. The crux of -the problem is factoring $f^{-} \circ g^{+}$ as a semisimplicial map -$h^{+}$ and demisimplicial map $h^{-}$; once we do this, we can -pre and post-compose $g^{-}$ and $f^{+}$, resp. +the problem is that we need to factor the composite of $f^{-} \circ g^{+}$ +$h^{+} \circ h^{-}$, where $h^{+}$ is semisimplicial and $h^{-}$ is +demisimplicial. Once this is done, we can obtain our final factorization +by pre and post-composing with $g^{-}$ and $f^{+}$, resp. For pedagogic purposes, we will define the image and semi/demisimplicial components of our factorization simultaneously. @@ -429,13 +456,21 @@ _∘Δ_ : Δ-Hom n o → Δ-Hom m n → Δ-Hom m o At this point, we could prove the associativity/unitality laws for $\Delta^{+}, \Delta^{-}$, and $\Delta$ by a series of brutal inductions. Luckily for us, there is a more elegant approach: all of these maps -have interpretations as maps `Fin m → Fin n`, and these interpretations -are both injective and functorial. This allows us to lift equations from functions -back to equations on their syntactic presentations, which gives us associativity +have interpretations as maps `Fin m → Fin n`. This interpretation is +has 2 key properties: + +1. The interpretation is functorial: both $\llbracket id \rrbracket = id$, + and $\llbracket f \circ g \rrbracket = \llbracket f \rrbracket \circ \llbracket g \rrbracket$. +2. The interpretation is injective: if $\llbracket f \rrbracket = \llbracket g \rrbracket$, then $f = g$. + +Together, this ensures that our interpretations form a series [[faithful functors]], +which allows us to lift equations from functions back to equations on their +syntactic presentations. In particular, composition of functions is associative +and unital, so constructing these interpretations gives us associativity and unitality "for free". -With that plan outlined, we begin by constructing interpretations -of (semi/demi) simplicial maps as functions. +With that plan outlined, we begin by constructing interpretations of (semi/demi) +simplicial maps as functions. ```agda Δ-hom⁺ : ∀ {m n} → Δ-Hom⁺ m n → Fin m → Fin n @@ -458,36 +493,35 @@ of (semi/demi) simplicial maps as functions. ``` --> -We will denote each of these interpretations with `⟦ f ⟧ i` to avoid +We will denote each of these interpretations as `⟦ f ⟧ i` to avoid too much syntactic overhead. + -Note that semisimplicial maps always encode inflationary functions. +Now that we have our interpretations, we can start to charaterize their +behaviour. First, note that semisimplicial maps always encode inflationary +functions. ```agda Δ-hom⁺-incr @@ -611,7 +645,7 @@ Semisimplicial maps are not just monotonic; they are *strictly* monotonic! Nat.s≤s (Δ-hom⁺-pres-< f⁺ (Nat.≤-peel i -These follow by some more brutal inductions that we will -shield the innocent reader from. +These follow by some more brutal inductions. ```agda @@ -773,7 +805,7 @@ directly from these lemmas. (Δ-hom-uniquep⁻ (f .hom⁺) (g .hom⁺) (f .hom⁻) (g .hom⁻) p) ``` -Injectivity the interpretaion of semi and demisimplicial maps follow +Injectivity the interpretation of semi and demisimplicial maps follow neatly as corollaries. ```agda