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}}}}