From 6032c6b6bf4d8ca51d220cf2c63129b162001615 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Sat, 19 Oct 2024 07:57:41 -0400 Subject: [PATCH] Knaster-Tarski for categories (#436) # Description This PR proves a Knaster-Tarski theorem for categories, and uses it to prove the usual Knaster-Tarski theorem for suplattices. ## Checklist Before submitting a merge request, please check the items below: - [x] I've read [the contributing guidelines](https://github.com/plt-amy/1lab/blob/main/CONTRIBUTING.md). - [x] The imports of new modules have been sorted with `support/sort-imports.hs` (or `nix run --experimental-features nix-command -f . sort-imports`). - [x] All new code blocks have "agda" as their language. If your change affects many files without adding substantial content, and you don't want your name to appear on those pages (for example, treewide refactorings or reformattings), start the commit message and PR title with `chore:`. --- src/Cat/Diagram/Initial/Weak.lagda.md | 12 +- src/Cat/Functor/Adjoint/AFT.lagda.md | 2 +- src/Cat/Functor/Algebra.lagda.md | 2 +- .../Functor/Algebra/KnasterTarski.lagda.md | 185 ++++++++++++++++++ src/Cat/Functor/Algebra/Limits.lagda.md | 121 ++++++++++++ src/Order/Cat.lagda.md | 16 +- src/Order/Diagram/Fixpoint.lagda.md | 2 + src/Order/Diagram/Glb.lagda.md | 31 +++ src/preamble.tex | 6 +- 9 files changed, 362 insertions(+), 15 deletions(-) create mode 100644 src/Cat/Functor/Algebra/KnasterTarski.lagda.md create mode 100644 src/Cat/Functor/Algebra/Limits.lagda.md diff --git a/src/Cat/Diagram/Initial/Weak.lagda.md b/src/Cat/Diagram/Initial/Weak.lagda.md index a711882ec..2f694369f 100644 --- a/src/Cat/Diagram/Initial/Weak.lagda.md +++ b/src/Cat/Diagram/Initial/Weak.lagda.md @@ -133,11 +133,11 @@ initial object. ```agda is-complete-weak-initial→initial - : ∀ {I : Type ℓ} (F : I → ⌞ C ⌟) ⦃ _ : ∀ {n} → H-Level I (2 + n) ⦄ - → is-complete ℓ ℓ C + : ∀ {κ} {I : Type κ} (F : I → ⌞ C ⌟) ⦃ _ : ∀ {n} → H-Level I (2 + n) ⦄ + → is-complete κ (ℓ ⊔ κ) C → is-weak-initial-fam F → Initial C - is-complete-weak-initial→initial F compl wif = record { has⊥ = equal-is-initial } where + is-complete-weak-initial→initial {κ = κ} F compl wif = record { has⊥ = equal-is-initial } where ```
@@ -147,17 +147,17 @@ initial object. open Indexed-product prod : Indexed-product C F - prod = Limit→IP C (hlevel 3) F (compl _) + prod = Limit→IP C (hlevel 3) F (is-complete-lower κ ℓ κ κ compl _) prod-is-wi : is-weak-initial (prod .ΠF) prod-is-wi = is-wif→is-weak-initial F wif (prod .has-is-ip) equal : Joint-equaliser C {I = Hom (prod .ΠF) (prod .ΠF)} λ h → h - equal = Limit→Joint-equaliser C _ id (is-complete-lower ℓ ℓ lzero ℓ compl _) + equal = Limit→Joint-equaliser C _ id (is-complete-lower κ κ lzero ℓ compl _) open Joint-equaliser equal using (has-is-je) equal-is-initial = is-weak-initial→equaliser _ prod-is-wi has-is-je λ f g → - Limit→Equaliser C (is-complete-lower ℓ ℓ lzero lzero compl _) + Limit→Equaliser C (is-complete-lower κ (ℓ ⊔ κ) lzero lzero compl _) ```
diff --git a/src/Cat/Functor/Adjoint/AFT.lagda.md b/src/Cat/Functor/Adjoint/AFT.lagda.md index 6fc2893cb..ef81f5439 100644 --- a/src/Cat/Functor/Adjoint/AFT.lagda.md +++ b/src/Cat/Functor/Adjoint/AFT.lagda.md @@ -16,7 +16,7 @@ import Cat.Reasoning as Cat module Cat.Functor.Adjoint.AFT where ``` -# The adjoint functor theorem +# The adjoint functor theorem {defines="adjoint-functor-theorem"} The **adjoint functor theorem** states a sufficient condition for a [[continuous functor]] $F : \cC \to \cD$ from a locally small, diff --git a/src/Cat/Functor/Algebra.lagda.md b/src/Cat/Functor/Algebra.lagda.md index d837ac9ac..2fbf80b3c 100644 --- a/src/Cat/Functor/Algebra.lagda.md +++ b/src/Cat/Functor/Algebra.lagda.md @@ -38,8 +38,8 @@ module _ {o ℓ} {C : Precategory o ℓ} (F : Functor C C) where +```agda +module Cat.Functor.Algebra.KnasterTarski where +``` + +# The Knaster-Tarski fixpoint theorem {defines="knaster-tarski"} + +The **Knaster-Tarski theorem** gives a recipe for constructing [[initial]] +[[F-algebras]] in [[complete categories]]. + +The big idea is that if a category $\cC$ is complete, then we can construct +an initial algebra of a functor $F$ by taking a limit $\rm{Fix}$ over the forgetful +functor $\pi : \FAlg{F} \to \cC$ from the category of $F$-algebras: +the universal property of such a limit let us construct an algebra +$F(\rm{Fix}) \to \rm{Fix}$, and the projections out of $\rm{Fix}$ let +us establish that $\rm{Fix}$ is the initial algebra. + +Unfortunately, this limit is a bit too ambitious. If we examine the universe +levels involved, we will quickly notice that this argument requires $\cC$ +to admit limits indexed by the \emph{objects} of $\cC$, which in the presence +of excluded middle means that $\cC$ must be a preorder. + +This problem of overly ambitious limits is similar to the one encountered +in the naïve [[adjoint functor theorem]], so we can use a similar technique +to repair our proof. In particular, we will impose a variant of the +**solution set condition** on the category of $F$-algebras that ensures +that the limit we end up computing is determined by a small amount of data, +which lets us relax our large-completeness requirement. + +More precisely, we will require that the category of $F$-algebras has a +small [[weakly initial family]] of algebras. This means that we need: + +- A family $\alpha_i : F(A_i) \to A_i$ of $F$ algebras indexed by a + small set $I$, such that; +- For every $F$-algebra $\beta : F(B) \to B$, there (merely) exists an $i : I$ + along with a $F$-algebra morphism $A_i \to B$. + + + +Once we have a solution set, the theorem pops open like a walnut submerged +in water: + +* First, $\cC$ is small-complete, so the category of $F$-algebras must also + be small-complete, as [[limits of algebras]] are computed by limits + in $\cC$. +* In particular, the category of $F$-algebras has all small [[equalisers]], + so we can upgrade our weakly initial family to an [[initial object]]. + +```agda + solution-set→initial-algebra + : ∀ {κ} {Idx : Type κ} ⦃ _ : ∀ {n} → H-Level Idx (2 + n) ⦄ + → (Aᵢ : Idx → FAlg.Ob F) + → is-complete κ (ℓ ⊔ κ) C + → is-weak-initial-fam (FAlg F) Aᵢ + → Initial (FAlg F) + solution-set→initial-algebra Aᵢ complete soln-set = + is-complete-weak-initial→initial (FAlg F) + Aᵢ + (FAlg-is-complete complete F) + soln-set +``` + +We can obtain the more familiar form of the Knaster-Tarski theorem by +applying [[Lambek's lemma]] to the resulting initial algebra. + +```agda + solution-set→fixpoint + : ∀ {κ} {Idx : Type κ} ⦃ _ : ∀ {n} → H-Level Idx (2 + n) ⦄ + → (Aᵢ : Idx → FAlg.Ob F) + → is-complete κ (ℓ ⊔ κ) C + → is-weak-initial-fam (FAlg F) Aᵢ + → Σ[ Fix ∈ Ob ] (F₀ Fix ≅ Fix) + solution-set→fixpoint Aᵢ complete soln-set = + bot .fst , invertible→iso (bot .snd) (lambek F (bot .snd) has⊥) + where open Initial (solution-set→initial-algebra Aᵢ complete soln-set) +``` + +## Knaster-Tarski for sup-lattices + + + +The "traditional" Knaster-Tarski theorem states that every [[monotone endomap|monotone-map]] +on a [[poset]] $P$ with all [[greatest lower bounds]] has a [[least fixpoint]]. +In the presence of [[propositional resizing]], this theorem follows as a corollary of +our previous theorem. + +```agda + complete→least-fixpoint + : (∀ {I : Type o} → (k : I → Ob) → Glb P k) + → Least-fixpoint P f + complete→least-fixpoint glbs = least-fixpoint where +``` + + + +The key is that resizing lets us prove the solution set condition with +respect to the size of the underlying set of $P$, as we can resize away +the proofs that $f x \leq x$. + +```agda + Idx : Type o + Idx = Σ[ x ∈ Ob ] (□ (f # x ≤ x)) + + soln : Idx → Σ[ x ∈ Ob ] (f # x ≤ x) + soln (x , lt) = x , (□-out! lt) + + is-soln-set : is-weak-initial-fam (FAlg (monotone→functor f)) soln + is-soln-set (x , lt) = inc ((x , inc lt) , total-hom ≤-refl prop!) +``` + +Moreover, $P$ has all [[greatest lower bounds]], so it is `complete as a +category`{.Agda ident=glbs→complete}. This lets us invoke the general +Knaster-Tarski theorem to get an initial $f$-algebra. + +```agda + initial : Initial (FAlg (monotone→functor f)) + initial = + solution-set→initial-algebra (monotone→functor f) + soln + (glbs→complete glbs) + is-soln-set +``` + +Finally, we can inline the proof of [[Lambek's lemma]] to show that this +initial algebra gives the least fixpoint of $f$! + +```agda + open Initial initial + + least-fixpoint : Least-fixpoint P f + least-fixpoint .fixpoint = + bot .fst + least-fixpoint .has-least-fixpoint .fixed = + ≤-antisym + (bot .snd) + (¡ {x = f .hom (bot .fst) , f .pres-≤ (bot .snd)} .hom) + least-fixpoint .has-least-fixpoint .least x fx=x = + ¡ {x = x , ≤-refl' fx=x} .hom +``` diff --git a/src/Cat/Functor/Algebra/Limits.lagda.md b/src/Cat/Functor/Algebra/Limits.lagda.md new file mode 100644 index 000000000..251718cdd --- /dev/null +++ b/src/Cat/Functor/Algebra/Limits.lagda.md @@ -0,0 +1,121 @@ +--- +description: | + Limits in categories of F-algebras. +--- + +```agda +module Cat.Functor.Algebra.Limits where +``` + +# Limits in categories of algebras {defines="limits-of-algebras"} + +This short note details the construction of [[limits]] in categories of +[[F-algebras]] from limits in the underlying category. + + + + + +Let $F : \cC \to \cC$ be an endofunctor, and $K : \cJ \to \FAlg{F}$ be a +diagram of $F$-algebras. If $\cC$ has a limit $L$ of $\pi \circ K$, then +$F(L)$ is the limit of $K$ in $\FAlg{F}$. + + +```agda + Forget-algebra-lift-limit : Limit (πᶠ (F-Algebras F) F∘ K) → Limit K + Forget-algebra-lift-limit L = to-limit (to-is-limit L') where + module L = Limit L + open make-is-limit +``` + +As noted earlier, the underlying object of the limit is $F(L)$. The algebra +$F(L) \to L$ is constructed via the universal property of $L$: to +give a map $F(L) \to L$, it suffices to give maps $F(L) \to K(j)$ for +every $j : \cJ$, which we can construct by composing the projection +$F(\psi_{j}) : F(L) \to F(K(j))$ with the algebra $F(K(j)) \to K(j)$. + +```agda + apex : FAlg.Ob F + apex .fst = L.apex + apex .snd = L.universal (λ j → K.₀ j .snd ∘ F.₁ (L.ψ j)) comm where abstract + comm + : ∀ {i j : J.Ob} (f : J.Hom i j) + → K.₁ f .hom ∘ K.₀ i .snd ∘ F.₁ (L.ψ i) ≡ K.₀ j .snd ∘ F.₁ (L.ψ j) + comm {i} {j} f = + K.₁ f .hom ∘ K.₀ i .snd ∘ F.₁ (L.ψ i) ≡⟨ pulll (K.₁ f .preserves) ⟩ + (K.₀ j .snd ∘ F.₁ (K.₁ f .hom)) ∘ F.₁ (L.ψ i) ≡⟨ F.pullr (L.commutes f) ⟩ + K.₀ j .snd ∘ F.₁ (L.ψ j) ∎ +``` + +A short series of calculations shows that the projections and universal map +associated to $L$ are $F$-algebra homomorphisms. + +```agda + L' : make-is-limit K apex + L' .ψ j .hom = L.ψ j + L' .ψ j .preserves = L.factors _ _ + L' .universal eps p .hom = + L.universal (λ j → eps j .hom) (λ f → ap hom (p f)) + L' .universal eps p .preserves = + L.unique₂ (λ j → K.F₀ j .snd ∘ F.₁ (eps j .hom)) + (λ f → pulll (K.₁ f .preserves) ∙ F.pullr (ap hom (p f))) + (λ j → pulll (L.factors _ _) ∙ eps j .preserves) + (λ j → pulll (L.factors _ _) ∙ F.pullr (L.factors _ _)) +``` + +Finally, equality of morphisms of $F$-algebras is given by equality on +the underlying morphisms, so all of the relevant diagrams in $\FAlg{F}$ +commute. + +```agda + L' .commutes f = + total-hom-path (F-Algebras F) (L.commutes f) prop! + L' .factors eps p = + total-hom-path (F-Algebras F) (L.factors _ _) prop! + L' .unique eps p other q = + total-hom-path (F-Algebras F) (L.unique _ _ _ λ j → ap hom (q j)) prop! +``` + + + +This gives us the following useful corollary: if $\cC$ is $\kappa$-complete, +then $\FAlg{F}$ is also $\kappa$ complete. + +```agda + FAlg-is-complete : (F : Functor C C) → is-complete oκ ℓκ (FAlg F) + FAlg-is-complete F K = Forget-algebra-lift-limit F K (complete (πᶠ (F-Algebras F) F∘ K)) +``` diff --git a/src/Order/Cat.lagda.md b/src/Order/Cat.lagda.md index f56c00a4e..13d85ccd8 100644 --- a/src/Order/Cat.lagda.md +++ b/src/Order/Cat.lagda.md @@ -59,14 +59,18 @@ automatic. ```agda open Functor -Posets↪Strict-cats : ∀ {ℓ ℓ'} → Functor (Posets ℓ ℓ') (Strict-cats ℓ ℓ') -Posets↪Strict-cats .F₀ P = poset→category P , Poset.Ob-is-set P -Posets↪Strict-cats .F₁ f .F₀ = f .hom -Posets↪Strict-cats .F₁ f .F₁ = f .pres-≤ -Posets↪Strict-cats .F₁ {y = y} f .F-id = Poset.≤-thin y _ _ -Posets↪Strict-cats .F₁ {y = y} f .F-∘ g h = Poset.≤-thin y _ _ +monotone→functor + : ∀ {o ℓ o' ℓ'} {P : Poset o ℓ} {Q : Poset o' ℓ'} + → Monotone P Q → Functor (poset→category P) (poset→category Q) +monotone→functor f .F₀ = f .hom +monotone→functor f .F₁ = f .pres-≤ +monotone→functor f .F-id = prop! +monotone→functor f .F-∘ _ _ = prop! +Posets↪Strict-cats : ∀ {ℓ ℓ'} → Functor (Posets ℓ ℓ') (Strict-cats ℓ ℓ') +Posets↪Strict-cats .F₀ P = poset→category P , Poset.Ob-is-set P +Posets↪Strict-cats .F₁ f = monotone→functor f Posets↪Strict-cats .F-id = Functor-path (λ _ → refl) λ _ → refl Posets↪Strict-cats .F-∘ f g = Functor-path (λ _ → refl) λ _ → refl ``` diff --git a/src/Order/Diagram/Fixpoint.lagda.md b/src/Order/Diagram/Fixpoint.lagda.md index 81f37f26b..7c527ab52 100644 --- a/src/Order/Diagram/Fixpoint.lagda.md +++ b/src/Order/Diagram/Fixpoint.lagda.md @@ -19,6 +19,8 @@ open Order.Reasoning P ``` --> +# Least fixpoints {defines="least-fixpoint"} + Let $(P, \le)$ be a poset, and $f : P \to P$ be a monotone map. We say that $f$ has a **least fixpoint** if there exists some $x : P$ such that $f(x) = x$, and for every other $y$ such that $f(y) = y$, $x \le y$. diff --git a/src/Order/Diagram/Glb.lagda.md b/src/Order/Diagram/Glb.lagda.md index 38c58654a..5defa1be9 100644 --- a/src/Order/Diagram/Glb.lagda.md +++ b/src/Order/Diagram/Glb.lagda.md @@ -1,5 +1,6 @@ + +## As limits + +If a poset $P$ has all greatest lower bounds of size $\kappa$, then +it is $\kappa$-[[complete|complete-category]] when [[viewed as a category|posets-as-categories]]. + + + +```agda + glbs→complete + : ∀ {oκ ℓκ} + → (∀ {I : Type oκ} (k : I → Ob) → Glb P k) + → is-complete oκ ℓκ (poset→category P) + glbs→complete glbs K = to-limit (to-is-limit lim) where + open make-is-limit + module K = Functor K + open Glb (glbs K.₀) + + lim : make-is-limit K glb + lim .ψ = glb≤fam + lim .commutes _ = prop! + lim .universal eps _ = greatest _ eps + lim .factors _ _ = prop! + lim .unique _ _ _ _ = prop! +``` diff --git a/src/preamble.tex b/src/preamble.tex index 115eec02e..6c74c0567 100644 --- a/src/preamble.tex +++ b/src/preamble.tex @@ -49,7 +49,11 @@ \newcommand{\ica}[1]{\mathbb{#1}} % Names of internal categories \newcommand{\Arr}[1]{%% The arrow category of a category. - \rm{Arr}(#1)} + \rm{Arr}(#1) +} +\newcommand{\FAlg}[1]{%% The category of F-algebras + \rm{Alg}(#1) +} % \liesover arrow is only allowed in KaTeX: \newcommand{\liesover}\katex{\mathrel{\htmlClass{liesover}{\hspace{1.366em}}}}