From fda6e83350b0b75947475e17269d589f92716171 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia?= Date: Mon, 23 Sep 2024 16:36:39 -0300 Subject: [PATCH] General adjoint functor theorem (#433) Proof from the nLab using joint equalisers and weakly initial objects. Only 3.3.2 and 3.3.3 from Borceux --- src/Borceux.lagda.md | 11 ++ src/Cat/Diagram/Equaliser/Joint.lagda.md | 173 +++++++++++++++++++++++ src/Cat/Diagram/Initial/Weak.lagda.md | 163 +++++++++++++++++++++ src/Cat/Diagram/Limit/Base.lagda.md | 23 ++- src/Cat/Functor/Adjoint/AFT.lagda.md | 125 ++++++++++++++++ src/Cat/Instances/Comma/Limits.lagda.md | 106 ++++++++++++++ 6 files changed, 600 insertions(+), 1 deletion(-) create mode 100644 src/Cat/Diagram/Equaliser/Joint.lagda.md create mode 100644 src/Cat/Diagram/Initial/Weak.lagda.md create mode 100644 src/Cat/Functor/Adjoint/AFT.lagda.md create mode 100644 src/Cat/Instances/Comma/Limits.lagda.md diff --git a/src/Borceux.lagda.md b/src/Borceux.lagda.md index 9e8d1dd0d..523586709 100644 --- a/src/Borceux.lagda.md +++ b/src/Borceux.lagda.md @@ -49,6 +49,7 @@ open import Cat.Diagram.Limit.Finite open import Cat.Functor.Conservative open import Cat.Functor.Hom.Coyoneda open import Cat.Diagram.Coequaliser +open import Cat.Functor.Adjoint.AFT open import Cat.Functor.Adjoint.Hom open import Cat.Functor.Adjoint.Kan open import Cat.Functor.Equivalence @@ -670,6 +671,16 @@ _ = right-adjoint-is-continuous ### 3.3 The adjoint functor theorem + + +* Definition 3.3.2: `Solution-set`{.Agda} +* Theorem 3.3.3: `solution-set→left-adjoint`{.Agda} + ### 3.4 Fully faithful adjoint functors + +```agda +module Cat.Diagram.Equaliser.Joint {o ℓ} (C : Precategory o ℓ) where +``` + + + +# Joint equalisers {defines="joint-equaliser"} + +The **joint equaliser** of a family $(F_i : \hom(a, b))_i$ of parallel +maps is a straightforward generalisation of the notion of [[equaliser]] +to more than two maps. The universal property is straightforward to +state: the joint equaliser of the $F_i$ is an arrow $e : E \to a$, +satisfying $F_i e = F_j e$, which is universal with this property. + +```agda +record is-joint-equaliser {ℓ'} {I : Type ℓ'} {E x y} (F : I → Hom x y) (equ : Hom E x) : Type (o ⊔ ℓ ⊔ ℓ') where + field + equal : ∀ {i j} → F i ∘ equ ≡ F j ∘ equ + universal : ∀ {E'} {e' : Hom E' x} (eq : ∀ i j → F i ∘ e' ≡ F j ∘ e') → Hom E' E + factors : ∀ {E'} {e' : Hom E' x} {eq : ∀ i j → F i ∘ e' ≡ F j ∘ e'} → equ ∘ universal eq ≡ e' + unique + : ∀ {E'} {e' : Hom E' x} {eq : ∀ i j → F i ∘ e' ≡ F j ∘ e'} {o : Hom E' E} + → equ ∘ o ≡ e' + → o ≡ universal eq +``` + + + +A simple calculation tells us that joint equalisers are [[monic]], much +like binary equalisers: + +```agda + is-joint-equaliser→is-monic : is-monic equ + is-joint-equaliser→is-monic g h x = unique₂ (λ i j → extendl equal) refl (sym x) +``` + + + +## Computation + +Joint equalisers are also limits. We can define the figure shape that +they are limits over as a straightforward generalisation of the +parallel-arrows category, where there is an arbitrary [[set]] of arrows +between the two objects. + +```agda +module _ {ℓ'} {I : Type ℓ'} ⦃ _ : H-Level I 2 ⦄ {x y} (F : I → Hom x y) where + private module P = Precategory + + private + shape : Precategory _ _ + shape .P.Ob = Bool + shape .P.Hom false false = Lift ℓ' ⊤ + shape .P.Hom false true = I + shape .P.Hom true false = Lift ℓ' ⊥ + shape .P.Hom true true = Lift ℓ' ⊤ +``` + +
+Giving this the structure of a category is trivial: other than +the $I$-many parallel arrows, there is nothing to compose +with. + +```agda + shape .P.Hom-set true true = hlevel 2 + shape .P.Hom-set true false = hlevel 2 + shape .P.Hom-set false true = hlevel 2 + shape .P.Hom-set false false = hlevel 2 + shape .P.id {true} = _ + shape .P.id {false} = _ + shape .P._∘_ {true} {true} {true} f g = lift tt + shape .P._∘_ {false} {true} {true} f g = g + shape .P._∘_ {false} {false} {true} f g = f + shape .P._∘_ {false} {false} {false} f g = lift tt + shape .P.idr {true} {true} f = refl + shape .P.idr {false} {true} f = refl + shape .P.idr {false} {false} f = refl + shape .P.idl {true} {true} f = refl + shape .P.idl {false} {true} f = refl + shape .P.idl {false} {false} f = refl + shape .P.assoc {true} {true} {true} {true} f g h = refl + shape .P.assoc {false} {true} {true} {true} f g h = refl + shape .P.assoc {false} {false} {true} {true} f g h = refl + shape .P.assoc {false} {false} {false} {true} f g h = refl + shape .P.assoc {false} {false} {false} {false} f g h = refl +``` + +
+ +The family of arrows $I \to \hom(x, y)$ extends straightforwardly to a +functor from this `shape`{.Agda} category to $\cC$. + +```agda + diagram : Functor shape C + diagram .F₀ true = y + diagram .F₀ false = x + diagram .F₁ {true} {true} f = id + diagram .F₁ {false} {true} i = F i + diagram .F₁ {false} {false} f = id + diagram .F-id {true} = refl + diagram .F-id {false} = refl + diagram .F-∘ {true} {true} {true} f g = introl refl + diagram .F-∘ {false} {true} {true} f g = introl refl + diagram .F-∘ {false} {false} {true} f g = intror refl + diagram .F-∘ {false} {false} {false} f g = introl refl +``` + +If the family is pointed, and the `diagram`{.Agda} has a limit, then +this limit is a joint equaliser of the given arrows. The requirement for +a point in the family ensures that we're not taking the joint equaliser +of *no* arrows, which would be a [[product]]. Finally, since joint +equalisers are unique, this construction is invariant under the chosen +point; it would thus suffice for the family to be inhabited instead. + +```agda + is-limit→joint-equaliser : ∀ {L} {l} → I → is-limit diagram L l → is-joint-equaliser F (l .η false) + is-limit→joint-equaliser {L} {l} ix lim = je where + module l = is-limit lim + je : is-joint-equaliser F (l .η false) + je .equal = sym (l .is-natural false true _) ∙ l .is-natural false true _ + je .universal {E'} {e'} eq = l.universal + (λ { true → F ix ∘ e' ; false → e' }) + λ { {true} {true} f → eliml refl + ; {false} {true} f → eq f ix + ; {false} {false} f → eliml refl } + je .factors = l.factors _ _ + je .unique p = l.unique _ _ _ λ where + true → ap₂ _∘_ (intror refl ∙ l .is-natural false true ix) refl ∙ pullr p + false → p + + open Joint-equaliser + + Limit→Joint-equaliser : I → Limit diagram → Joint-equaliser F + Limit→Joint-equaliser ix lim .apex = Limit.apex lim + Limit→Joint-equaliser ix lim .equ = Limit.cone lim .η false + Limit→Joint-equaliser ix lim .has-is-je = is-limit→joint-equaliser ix (Limit.has-limit lim) +``` diff --git a/src/Cat/Diagram/Initial/Weak.lagda.md b/src/Cat/Diagram/Initial/Weak.lagda.md new file mode 100644 index 000000000..a711882ec --- /dev/null +++ b/src/Cat/Diagram/Initial/Weak.lagda.md @@ -0,0 +1,163 @@ + + +```agda +module Cat.Diagram.Initial.Weak where +``` + +# Weakly initial objects and families {defines="weakly-initial-object"} + + + +A **weakly initial object** is like an [[initial object]], but dropping +the requirement of uniqueness. Explicitly, an object $X$ is weakly +initial in $\cC$, if, for every $Y : \cC$, there merely exists an arrow +$X \to Y$. + +```agda + is-weak-initial : ⌞ C ⌟ → Type _ + is-weak-initial X = ∀ Y → ∥ Hom X Y ∥ +``` + +::: {.definition #weakly-initial-family} +We can weaken this even further, by allowing a family of objects rather +than the single object $X$: a family $(F_i)_{i : I}$ is weakly initial +if, for every $Y$, there exists a $j : I$ and a map $F_j \to Y$. Note +that we don't (can't!) impose any compatibility conditions between the +choices of indices. + +```agda + is-weak-initial-fam : ∀ {ℓ'} {I : Type ℓ'} (F : I → ⌞ C ⌟) → Type _ + is-weak-initial-fam {I = I} F = (Y : ⌞ C ⌟) → ∃[ i ∈ I ] (Hom (F i) Y) +``` +::: + +The connection between these notions is the following: the [[indexed +product]] of a weakly initial family $F$ is a weakly initial object. + +```agda + is-wif→is-weak-initial + : ∀ {ℓ'} {I : Type ℓ'} (F : I → ⌞ C ⌟) {ΠF} {πf : ∀ i → Hom ΠF (F i)} + → is-weak-initial-fam F + → is-indexed-product C F πf + → (y : ⌞ C ⌟) → ∥ Hom ΠF y ∥ + is-wif→is-weak-initial F {πf = πf} wif ip y = do + (ix , h) ← wif y + pure (h ∘ πf ix) +``` + +We can also connect these notions to the non-weak initial objects. +Suppose $\cC$ has all [[equalisers]], including [[joint equalisers]] for +small families. If $X$ is a weakly initial object, then the domain of +the joint equaliser $i : L \to X$ of all arrows $X \to X$ is an initial object. + +```agda + is-weak-initial→equaliser + : ∀ (X : ⌞ C ⌟) {L} {l : Hom L X} + → (∀ y → ∥ Hom X y ∥) + → is-joint-equaliser C {I = Hom X X} (λ x → x) l + → has-equalisers C + → is-initial C L + is-weak-initial→equaliser X {L} {i} is-wi lim eqs y = contr cen (p' _) where + open is-joint-equaliser lim +``` + +Since, for any $Y$, the space of maps $e \to Y$ is inhabited, it will +suffice to show that it is a [[proposition]]. To this end, given two +arrows $f, g : L \to Y$, consider their equaliser $j : E \to L$. First, +we have some arrow $k : X \to E$. + +```agda + p' : is-prop (Hom L y) + p' f g = ∥-∥-out! do + let + module fg = Equaliser (eqs f g) + open fg renaming (equ to j) using () + + k ← is-wi fg.apex +``` + +Then, we can calculate: as maps $L \to X$, we have $i = ijki$; + +```agda + let + p = + i ≡⟨ introl refl ⟩ + id ∘ i ≡⟨ equal {j = i ∘ j ∘ k} ⟩ + (i ∘ j ∘ k) ∘ i ≡⟨ pullr (pullr refl) ⟩ + i ∘ j ∘ k ∘ i ∎ +``` + +Then, since a joint equaliser is a [[monomorphism]], we can cancel $i$ +from both sides to get $jki = \id$; + +```agda + r : j ∘ k ∘ i ≡ id + r = is-joint-equaliser→is-monic (j ∘ k ∘ i) id (sym p ∙ intror refl) +``` + +Finally, if we have $g, h : L \to Z$ with $gj = hj$, then we can +calculate $$g = gjki = hjki = h$$, so $j$ is an [[epimorphism]]. So, +since $j$ equalises $f$ and $g$ by construction, we have $f = g$! + +```agda + s : is-epic j + s g h α = intror r ∙ extendl α ∙ elimr r + + pure (s f g fg.equal) + + cen : Hom L y + cen = ∥-∥-out p' ((_∘ i) <$> is-wi y) +``` + +Putting this together, we can show that, if a [[complete category]] has +a small weakly initial family indexed by a [[set]], then it has an +initial object. + +```agda + is-complete-weak-initial→initial + : ∀ {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 +``` + +
+The proof is by pasting together the results above. + +```agda + open Indexed-product + + prod : Indexed-product C F + prod = Limit→IP C (hlevel 3) F (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 _) + 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 _) +``` + +
diff --git a/src/Cat/Diagram/Limit/Base.lagda.md b/src/Cat/Diagram/Limit/Base.lagda.md index 0dac55478..d4e73d285 100644 --- a/src/Cat/Diagram/Limit/Base.lagda.md +++ b/src/Cat/Diagram/Limit/Base.lagda.md @@ -9,6 +9,7 @@ open import Cat.Diagram.Equaliser open import Cat.Functor.Coherence open import Cat.Functor.Constant open import Cat.Functor.Kan.Base +open import Cat.Instances.Lift open import Cat.Functor.Base open import Cat.Prelude @@ -754,7 +755,7 @@ module _ {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} {D : Precategor ``` --> -## Continuity +## Continuity {defines="continuous-functor"} ```agda is-continuous @@ -792,6 +793,26 @@ is-complete : ∀ {oc ℓc} o ℓ → Precategory oc ℓc → Type _ is-complete oj ℓj C = ∀ {J : Precategory oj ℓj} (F : Functor J C) → Limit F ``` + + While this condition might sound very strong, and thus that it would be hard to come by, it turns out we can get away with only two fundamental types of limits: [[products]] and [[equalisers]]. In order to construct the limit for a diagram diff --git a/src/Cat/Functor/Adjoint/AFT.lagda.md b/src/Cat/Functor/Adjoint/AFT.lagda.md new file mode 100644 index 000000000..6fc2893cb --- /dev/null +++ b/src/Cat/Functor/Adjoint/AFT.lagda.md @@ -0,0 +1,125 @@ + + +```agda +module Cat.Functor.Adjoint.AFT where +``` + +# The adjoint functor theorem + +The **adjoint functor theorem** states a sufficient condition for a +[[continuous functor]] $F : \cC \to \cD$ from a locally small, +[[complete category]] to have a [[left adjoint]]. + +In an ideal world, this would always be the case: we want to compute an +[[initial object]] $Lx$ in the [[comma category]] $x \swarrow F$, for +each $x : \cD$. Generalising from the case of [[partial orders]], where +a [[bottom element]] is the intersection of everything in the poset, we +might try to find $Lx$ as the limit of the identity functor on $x +\swarrow F$. Furthermore, each of these comma categories are +[[complete|complete category]], by completeness of $\cC$ and continuity +of $F$, so this functor should have a limit! + +Unfortunately, the only categories which can be shown to admit arbitrary +limits indexed by themselves are the preorders; The existence of a +large-complete *non*-preorder would contradict excluded middle, which we +neither assume nor reject. Therefore, we're left with the task of +finding a condition on the functor $F$ which ensures that we can compute +the limit of $\Id : x \swarrow F \to x \swarrow F$ using only small +data. The result is a technical device called a **solution set**. + + + +A solution set (for $F$ with respect to $Y : \cD$) is a [[set]] $I$, +together with an $I$-indexed family of objects $X_i$ and morphisms $m_i +: Y \to F(X_i)$, which commute in the sense that, for every $X'$ and $h +: Y \to X'$, there exists a $j : I$ and $t : X_i \to X'$ which satisfy +$h = F(t)m_i$. + +```agda + record Solution-set (Y : ⌞ D ⌟) : Type (o ⊔ lsuc ℓ) where + field + {index} : Type ℓ + has-is-set : is-set index + + dom : index → ⌞ C ⌟ + map : ∀ i → D.Hom Y (F.₀ (dom i)) + factor : ∀ {X'} (h : D.Hom Y (F.₀ X')) → ∃[ i ∈ index ] (Σ[ t ∈ C.Hom (dom i) X' ] (h ≡ F.₁ t D.∘ map i)) +``` + + + +Put another way, $F$ has a solution set with respect to $X$ if the +[[comma category]] $X \swarrow F$ has a [[weakly initial family]] of +objects, given by the $m_i$ and their domains, with the complicated +factoring condition corresponding to weak initiality. + +```agda + module _ {X} (S : Solution-set X) where + solution-set→family : S .index → ⌞ X ↙ F ⌟ + solution-set→family i .x = tt + solution-set→family i .y = S .dom i + solution-set→family i .map = S .map i + + solution-set→family-is-weak-initial + : is-weak-initial-fam (X ↙ F) solution-set→family + solution-set→family-is-weak-initial Y = do + (i , t , p) ← S .factor (Y .map) + pure (i , ↓hom (D.elimr refl ∙ p)) +``` + +Then, we can put together the adjoint functor theorem, by showing that +the sea has risen above it: + +* Since $\cC$ is small-complete and $F$ is small-continuous, then each + comma category $x \swarrow F$ is small-complete, by `limits in comma + categories`{.Agda ident=comma-is-complete}; +* Each $x \swarrow F$ has a weakly initial family, and all small + [[equalisers]], so they all have initial objects; +* An initial object for $x \swarrow F$ is exactly a [[universal morphism]] + into $F$, and if $F$ admits all universal maps, then it has a left + adjoint. + +```agda + solution-set→left-adjoint + : is-complete ℓ ℓ C + → is-continuous ℓ ℓ F + → (∀ y → Solution-set y) + → Σ[ G ∈ Functor D C ] G ⊣ F + solution-set→left-adjoint c-compl F-cont ss = + _ , universal-maps→left-adjoint init where module _ x where + instance + H-Level-ix : ∀ {n} → H-Level (ss x .index) (2 + n) + H-Level-ix = basic-instance 2 (ss x .has-is-set) + + init : Initial (x ↙ F) + init = is-complete-weak-initial→initial (x ↙ F) + (solution-set→family (ss x)) + (comma-is-complete F c-compl F-cont) + (solution-set→family-is-weak-initial (ss x)) +``` diff --git a/src/Cat/Instances/Comma/Limits.lagda.md b/src/Cat/Instances/Comma/Limits.lagda.md new file mode 100644 index 000000000..9c10d7782 --- /dev/null +++ b/src/Cat/Instances/Comma/Limits.lagda.md @@ -0,0 +1,106 @@ + + +```agda +module Cat.Instances.Comma.Limits where +``` + + + +# Limits in comma categories + +This short note proves the following fact about [[limits]] in [[comma +categories]] of the form $d \swarrow F$: If $\cC$ has a limit $L$ for +$\operatorname{cod}\circ G$ and $F$ preserves limits the size of $G$'s +shape $\cJ$, then $L$ can be made into an object of $d \swarrow F$, and +this object is the limit of $J$. + + + +```agda + Cod-lift-limit : Limit (Cod _ F F∘ G) → Limit G + Cod-lift-limit limf = to-limit (to-is-limit lim') where + module limf = Limit limf + + flimf = F-cont limf.has-limit + module flimf = is-limit flimf +``` + +The family of maps $d \to FL$ can be given componentwise, since $FL$ is +a limit in $\cD$: it suffices to give a family of maps $d \to FGj$, at +each $j : \cJ$. But $G$ sends objects of $\cJ$ to pairs which include a +map $d \to FGj$, and it does so in a way compatible with $F$, by +definition. + +```agda + apex : ⌞ d ↙ F ⌟ + apex .x = tt + apex .y = limf.apex + apex .map = flimf.universal (λ j → G.₀ j .map) λ f → sym (G.₁ f .sq) ∙ D.elimr refl +``` + +Similarly short calculations show that we can define maps in $d \swarrow +F$ into $L$ componentwise, and these satisfy the universal property. + +```agda + lim' : make-is-limit G apex + lim' .ψ j .α = tt + lim' .ψ j .β = limf.ψ j + lim' .ψ j .sq = sym (flimf.factors _ _ ∙ D.intror refl) + lim' .commutes f = ext (sym (limf.eps .is-natural _ _ _) ∙ C.elimr limf.Ext.F-id) + lim' .universal eta p .α = tt + lim' .universal eta p .β = limf.universal (λ j → eta j .β) λ f → ap β (p f) + lim' .universal eta p .sq = D.elimr refl ∙ sym (flimf.unique _ _ _ λ j → F.pulll (limf.factors _ _) ∙ sym (eta j .sq) ∙ D.elimr refl) + lim' .factors eta p = ext (limf.factors _ _) + lim' .unique eta p other q = ext (limf.unique _ _ _ λ j → ap β (q j)) +``` + +As an easy corollary, we get: if $\cC$ is small-complete and $F$ +small-continuous, then $d \swarrow F$ is small-complete as well. + + + +```agda + comma-is-complete : ∀ {d} → is-complete ℓ ℓ (d ↙ F) + comma-is-complete G = Cod-lift-limit F F-cont (c-compl (Cod _ F F∘ G)) +```