|
| 1 | +```agda |
| 2 | +open import Cat.Functor.Adjoint.Monadic |
| 3 | +open import Cat.Functor.Adjoint.Monad |
| 4 | +open import Cat.Functor.Monadic.Beck |
| 5 | +open import Cat.Functor.Conservative |
| 6 | +open import Cat.Functor.Equivalence |
| 7 | +open import Cat.Diagram.Coequaliser |
| 8 | +open import Cat.Functor.Adjoint |
| 9 | +open import Cat.Diagram.Monad |
| 10 | +open import Cat.Prelude |
| 11 | +
|
| 12 | +import Cat.Functor.Reasoning as F-r |
| 13 | +import Cat.Reasoning as C-r |
| 14 | +
|
| 15 | +module |
| 16 | + Cat.Functor.Monadic.Crude |
| 17 | + {o ℓ o′ ℓ′} {C : Precategory o ℓ} {D : Precategory o′ ℓ′} |
| 18 | + {F : Functor C D} {U : Functor D C} |
| 19 | + (F⊣U : F ⊣ U) |
| 20 | + where |
| 21 | +``` |
| 22 | + |
| 23 | +<!-- |
| 24 | +```agda |
| 25 | +private |
| 26 | + module F = F-r F |
| 27 | + module U = F-r U |
| 28 | + module C = C-r C |
| 29 | + module D = C-r D |
| 30 | + module UF = F-r (U F∘ F) |
| 31 | + module T = Monad (Adjunction→Monad F⊣U) |
| 32 | +
|
| 33 | + T : Monad C |
| 34 | + T = Adjunction→Monad F⊣U |
| 35 | + C^T : Precategory _ _ |
| 36 | + C^T = Eilenberg-Moore C T |
| 37 | +
|
| 38 | + module C^T = C-r C^T |
| 39 | +
|
| 40 | +open _⊣_ F⊣U |
| 41 | +open _=>_ |
| 42 | +open Algebra-hom |
| 43 | +open Algebra-on |
| 44 | +``` |
| 45 | +--> |
| 46 | + |
| 47 | +# Crude monadicity |
| 48 | + |
| 49 | +We present a refinement of the conditions laid out in [Beck's |
| 50 | +coequaliser] for when an adjunction $F \dashv G$ is [monadic]: The |
| 51 | +**crude monadicity theorem**. The proof we present is adapted from |
| 52 | +[@SIGL, chap. IV; sect. 4], where it is applied to the setting of |
| 53 | +elementary topoi, but carried out in full generality. |
| 54 | + |
| 55 | +[Beck's coequaliser]: Cat.Functor.Monadic.Beck.html#becks-coequaliser |
| 56 | +[monadic]: Cat.Functor.Adjoint.Monadic.html |
| 57 | + |
| 58 | +Recall our setup. We have a [left adjoint][ladj] functor $F : \ca{C} \to |
| 59 | +\ca{D}$ (call its right adjoint $U$), and we're interested in |
| 60 | +characterising exactly when the [comparison functor][comp] $K : \ca{D} |
| 61 | +\to \ca{C}^{UF}$ into the [Eilenberg-Moore category][emc] of the [monad |
| 62 | +from the adjunction][madj] is an equivalence. Our refinement here gives |
| 63 | +a _sufficient_ condition. |
| 64 | + |
| 65 | +[ladj]: Cat.Functor.Adjoint.html |
| 66 | +[comp]: Cat.Functor.Adjoint.Monadic.html#Comparison |
| 67 | +[emc]: Cat.Diagram.Monad.html#eilenberg-moore-category |
| 68 | +[madj]: Cat.Functor.Adjoint.Monad.html |
| 69 | + |
| 70 | +**Theorem** (Crude monadicity). Let the functors $F$, $U$ be as in the |
| 71 | +paragraph above, and abbreviate the resulting monad by $T$; Denote the |
| 72 | +comparison functor by $K$. |
| 73 | + |
| 74 | +1. If $\ca{D}$ has [Beck's coequalisers] for any $T$-algebra, then $K$ |
| 75 | +has a left adjoint $K^{-1} \dashv K$; |
| 76 | + |
| 77 | +2. If, in addition, $U$ preserves coequalisers for any pair which has a |
| 78 | +common right inverse, then the unit of the adjunction $\eta$ is a |
| 79 | +natural isomorphism; |
| 80 | + |
| 81 | +3. If, in addition, $U$ is [conservative], then the counit of the |
| 82 | +adjunction $\eta$ is also a natural isomorphism, and $K$ is an |
| 83 | +[equivalence of precategories][eqv]. |
| 84 | + |
| 85 | +[Beck's coequalisers]: Cat.Functor.Monadic.Beck.html#presented-algebras |
| 86 | +[conservative]: Cat.Functor.Conservative.html |
| 87 | +[eqv]: Cat.Functor.Equivalence.html |
| 88 | + |
| 89 | +**Proof** We already established (1) [here][Beck's coequalisers]. |
| 90 | + |
| 91 | +Let us show (2). Suppose that $\ca{D}$ has Beck's coequalisers and that |
| 92 | +$U$ preserves coequalisers of pairs of morphisms with a common right |
| 93 | +inverse (we call these coequalisers **reflexive**): |
| 94 | + |
| 95 | +```agda |
| 96 | +private |
| 97 | + U-preserves-reflexive-coeqs : Type _ |
| 98 | + U-preserves-reflexive-coeqs = |
| 99 | + ∀ {A B} {f g : D.Hom A B} (i : D.Hom B A) |
| 100 | + → (f D.∘ i ≡ D.id) → (g D.∘ i ≡ D.id) |
| 101 | + → (coequ : Coequaliser D f g) |
| 102 | + → is-coequaliser C (U.₁ f) (U.₁ g) (U.₁ (coequ .Coequaliser.coeq)) |
| 103 | +
|
| 104 | +module _ |
| 105 | + (has-coeq : (M : Algebra C T) → Coequaliser D (F.₁ (M .snd .ν)) (counit.ε _)) |
| 106 | + (U-pres : U-preserves-reflexive-coeqs) |
| 107 | + where |
| 108 | +``` |
| 109 | + |
| 110 | +<!-- |
| 111 | +```agda |
| 112 | + open is-coequaliser |
| 113 | + open Coequaliser |
| 114 | + open Functor |
| 115 | +
|
| 116 | + private |
| 117 | + K⁻¹ : Functor C^T D |
| 118 | + K⁻¹ = Comparison⁻¹ F⊣U has-coeq |
| 119 | +
|
| 120 | + K⁻¹⊣K : K⁻¹ ⊣ Comparison F⊣U |
| 121 | + K⁻¹⊣K = Comparison⁻¹⊣Comparison F⊣U has-coeq |
| 122 | +
|
| 123 | + module adj = _⊣_ K⁻¹⊣K |
| 124 | +``` |
| 125 | +--> |
| 126 | + |
| 127 | +```agda |
| 128 | + -- N.B.: In the code we abbreviate "preserves reflexive coequalisers" |
| 129 | + -- by "prcoeq". |
| 130 | + prcoeq→unit-is-iso : ∀ {o} → C^T.is-invertible (adj.unit.η o) |
| 131 | + prcoeq→unit-is-iso {o} = C^T.make-invertible inverse |
| 132 | + (Algebra-hom-path C η⁻¹η) (Algebra-hom-path C ηη⁻¹) where |
| 133 | +``` |
| 134 | + |
| 135 | +The first thing we note is that Beck's coequaliser is reflexive: The |
| 136 | +common right inverse is $F\eta$. It's straightforward to calculate that |
| 137 | +this map _is_ a right inverse; let me point out that it follows from the |
| 138 | +triangle identities for $F \dashv U$ and the algebra laws. |
| 139 | + |
| 140 | +```agda |
| 141 | + abstract |
| 142 | + preserved : is-coequaliser C |
| 143 | + (UF.₁ (o .snd .ν)) (U.₁ (counit.ε (F.₀ (o .fst)))) |
| 144 | + (U.₁ (has-coeq o .coeq)) |
| 145 | + preserved = |
| 146 | + U-pres (F.₁ (unit.η _)) (F.annihilate (o .snd .ν-unit)) zig |
| 147 | + (has-coeq o) |
| 148 | +``` |
| 149 | + |
| 150 | +It follows, since $U$ preserves coequalisers, that both rows of the diagram |
| 151 | + |
| 152 | +~~~{.quiver} |
| 153 | +\[\begin{tikzcd} |
| 154 | + {T^2o} & UFo & o \\ |
| 155 | + {T^2o} & UFo & {UK^{-1}(o)} |
| 156 | + \arrow[shift left=1, from=1-1, to=1-2] |
| 157 | + \arrow[shift right=1, from=1-1, to=1-2] |
| 158 | + \arrow[shift left=1, from=2-1, to=2-2] |
| 159 | + \arrow[shift right=1, from=2-1, to=2-2] |
| 160 | + \arrow[Rightarrow, no head, from=1-1, to=2-1] |
| 161 | + \arrow[Rightarrow, from=1-2, to=2-2] |
| 162 | + \arrow["e", from=1-2, to=1-3] |
| 163 | + \arrow["Ue"', from=2-2, to=2-3] |
| 164 | + \arrow["{\eta_o^{-1}}", dashed, from=1-3, to=2-3] |
| 165 | +\end{tikzcd}\] |
| 166 | +~~~ |
| 167 | + |
| 168 | +are coequalisers, hence there is a unique isomorphism $\eta_o^{-1}$ |
| 169 | +making the diagram commute. This is precisely the inverse to $\eta_o$ |
| 170 | +we're seeking. |
| 171 | + |
| 172 | +```agda |
| 173 | + η⁻¹ : C.Hom (U.₀ (coapex (has-coeq o))) (o .fst) |
| 174 | + η⁻¹η : adj.unit.η _ .morphism C.∘ η⁻¹ ≡ C.id |
| 175 | + ηη⁻¹ : η⁻¹ C.∘ adj.unit.η _ .morphism ≡ C.id |
| 176 | +
|
| 177 | + η⁻¹ = preserved .coequalise {e′ = o .snd .ν} (o .snd .ν-mult) |
| 178 | +
|
| 179 | + η⁻¹η = is-coequaliser.unique₂ preserved |
| 180 | + {e′ = U.₁ (has-coeq o .coeq)} {p = preserved .coequal} |
| 181 | + (sym (C.pullr (preserved .universal) |
| 182 | + ∙ C.pullr (unit.is-natural _ _ _) |
| 183 | + ∙ C.pulll (preserved .coequal) |
| 184 | + ∙ C.cancelr zag)) |
| 185 | + (C.introl refl) |
| 186 | +
|
| 187 | + ηη⁻¹ = C.pulll (preserved .universal) ∙ o .snd .ν-unit |
| 188 | +``` |
| 189 | + |
| 190 | +It remains to show that $\eta^{-1}$ is a homomorphism of algebras. This |
| 191 | +is a calculation reusing the established proof that $\eta^{-1}\eta = |
| 192 | +\id{id}$ established using the universal property of coequalisers above. |
| 193 | + |
| 194 | +```agda |
| 195 | + inverse : C^T.Hom (U.₀ _ , _) o |
| 196 | + inverse .morphism = η⁻¹ |
| 197 | + inverse .commutes = |
| 198 | + η⁻¹ C.∘ U.₁ (counit.ε _) ≡⟨ C.refl⟩∘⟨ ap U.₁ (D.intror (F.annihilate (C.assoc _ _ _ ∙ η⁻¹η))) ⟩ |
| 199 | + η⁻¹ C.∘ U.₁ (counit.ε _ D.∘ F.₁ (U.₁ (has-coeq o .coeq)) D.∘ F.₁ (unit.η _ C.∘ η⁻¹)) ≡⟨ C.refl⟩∘⟨ ap U.₁ (D.extendl (counit.is-natural _ _ _)) ⟩ |
| 200 | + η⁻¹ C.∘ U.₁ (has-coeq o .coeq D.∘ counit.ε _ D.∘ F.₁ (unit.η _ C.∘ η⁻¹)) ≡⟨ C.refl⟩∘⟨ U.F-∘ _ _ ⟩ |
| 201 | + η⁻¹ C.∘ U.₁ (has-coeq o .coeq) C.∘ U.₁ (counit.ε _ D.∘ F.₁ (unit.η _ C.∘ η⁻¹)) ≡⟨ C.pulll (preserved .universal) ⟩ |
| 202 | + o .snd .ν C.∘ U.₁ (counit.ε _ D.∘ F.₁ (unit.η _ C.∘ η⁻¹)) ≡⟨ C.refl⟩∘⟨ ap U.₁ (ap (counit.ε _ D.∘_) (F.F-∘ _ _) ∙ D.cancell zig) ⟩ |
| 203 | + o .snd .ν C.∘ UF.₁ η⁻¹ ∎ |
| 204 | +``` |
| 205 | + |
| 206 | +For (3), suppose additionally that $U$ is conservative. Recall that the |
| 207 | +counit $\epsilon$ for the $K^{-1} \dashv K$ adjunction is defined as the |
| 208 | +unique dotted map which fits into |
| 209 | + |
| 210 | +~~~{.quiver} |
| 211 | +\[\begin{tikzcd} |
| 212 | + FUFUA & FUA & {K^{-1}KA} \\ |
| 213 | + && {A.} |
| 214 | + \arrow[two heads, from=1-2, to=1-3] |
| 215 | + \arrow["{\varepsilon'_{FUA}}"', shift right=1, from=1-1, to=1-2] |
| 216 | + \arrow["{\varepsilon'}"', from=1-2, to=2-3] |
| 217 | + \arrow["\epsilon", from=1-3, to=2-3] |
| 218 | + \arrow["{FU\varepsilon_A'}", shift left=1, from=1-1, to=1-2] |
| 219 | +\end{tikzcd}\] |
| 220 | +~~~ |
| 221 | + |
| 222 | +But observe that the diagram |
| 223 | + |
| 224 | +~~~{.quiver .short-1} |
| 225 | +\[\begin{tikzcd} |
| 226 | + UFUFUA && UFUA & {UA,} |
| 227 | + \arrow[two heads, from=1-3, to=1-4] |
| 228 | + \arrow["{U\varepsilon'_{FUA}}"', shift right=1, from=1-1, to=1-3] |
| 229 | + \arrow["{UFU\varepsilon_A'}", shift left=1, from=1-1, to=1-3] |
| 230 | +\end{tikzcd}\] |
| 231 | +~~~ |
| 232 | + |
| 233 | +is _also_ a coequaliser; Hence, since $U$ preserves the coequaliser $FUA |
| 234 | +\epi K^{-1}KA$, the map $U\eps : UK^{-1}KA \cong UA$; But by assumption |
| 235 | +$U$ is conservative, so $\eps$ is an isomorphism, as desired. |
| 236 | + |
| 237 | +```agda |
| 238 | + conservative-prcoeq→counit-is-iso |
| 239 | + : ∀ {o} → is-conservative U → D.is-invertible (adj.counit.ε o) |
| 240 | + conservative-prcoeq→counit-is-iso {o} reflect-iso = reflect-iso $ |
| 241 | + C.make-invertible |
| 242 | + (U.₁ (coequ .coeq) C.∘ unit.η _) (U.pulll (coequ .universal) ∙ zag) |
| 243 | + inversel |
| 244 | + where |
| 245 | +
|
| 246 | + oalg = Comparison F⊣U .F₀ o |
| 247 | + coequ = has-coeq oalg |
| 248 | +
|
| 249 | + abstract |
| 250 | + preserved : is-coequaliser C |
| 251 | + (UF.₁ (oalg .snd .ν)) (U.₁ (counit.ε (F.₀ (oalg .fst)))) |
| 252 | + (U.₁ (coequ .coeq)) |
| 253 | + preserved = |
| 254 | + U-pres (F.₁ (unit.η _)) (F.annihilate (oalg .snd .ν-unit)) zig coequ |
| 255 | +
|
| 256 | + inversel = |
| 257 | + is-coequaliser.unique₂ preserved |
| 258 | + {e′ = U.₁ (coequ .coeq)} {p = preserved .coequal} |
| 259 | + (sym (C.pullr (U.collapse (coequ .universal)) |
| 260 | + ∙ C.pullr (unit.is-natural _ _ _) |
| 261 | + ∙ C.pulll (preserved .coequal) |
| 262 | + ∙ C.cancelr zag)) |
| 263 | + (C.introl refl) |
| 264 | +``` |
| 265 | + |
| 266 | +Packaging it all up, we get the claimed theorem: If $\ca{D}$ has Beck's |
| 267 | +coequalisers, and $U$ is a conservative functor which preserves |
| 268 | +reflexive coequalisers, then the adjunction $F \dashv U$ is monadic. |
| 269 | + |
| 270 | +```agda |
| 271 | +crude-monadicity |
| 272 | + : (has-coeq : (M : Algebra C T) → Coequaliser D (F.₁ (M .snd .ν)) (counit.ε _)) |
| 273 | + (U-pres : U-preserves-reflexive-coeqs) |
| 274 | + (U-conservative : is-conservative U) |
| 275 | + → is-monadic F⊣U |
| 276 | +crude-monadicity coeq pres cons = eqv′ where |
| 277 | + open is-equivalence |
| 278 | + eqv : is-equivalence (Comparison⁻¹ F⊣U coeq) |
| 279 | + eqv .F⁻¹ = Comparison F⊣U |
| 280 | + eqv .F⊣F⁻¹ = Comparison⁻¹⊣Comparison F⊣U coeq |
| 281 | + eqv .unit-iso _ = prcoeq→unit-is-iso coeq pres |
| 282 | + eqv .counit-iso _ = conservative-prcoeq→counit-is-iso coeq pres cons |
| 283 | + eqv′ = inverse-equivalence eqv |
| 284 | +``` |
0 commit comments