Skip to content

Commit b984835

Browse files
JacquesCaretteJacquesCarette
authored
Merge pull request #240 from TOTBWF/monadicity
Crude Monadicity Theorem
2 parents 9bdde16 + 6022bb9 commit b984835

File tree

7 files changed

+460
-8
lines changed

7 files changed

+460
-8
lines changed

‎src/Categories/Adjoint/Monadic.agda‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
-- Monadic Adjunctions
4+
-- https://ncatlab.org/nlab/show/monadic+adjunction
5+
module Categories.Adjoint.Monadic where
6+
7+
open import Level
8+
9+
open import Categories.Adjoint
10+
open import Categories.Adjoint.Properties
11+
open import Categories.Category
12+
open import Categories.Category.Equivalence
13+
open import Categories.Functor
14+
open import Categories.Monad
15+
16+
open import Categories.Category.Construction.EilenbergMoore
17+
open import Categories.Category.Construction.Properties.EilenbergMoore
18+
19+
private
20+
variable
21+
o ℓ e : Level
22+
𝒞 𝒟 : Category o ℓ e
23+
24+
-- An adjunction is monadic if the adjunction "comes from" the induced monad in some sense.
25+
record IsMonadicAdjunction {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) : Set (levelOfTerm 𝒞 ⊔ levelOfTerm 𝒟) where
26+
private
27+
T : Monad 𝒞
28+
T = adjoint⇒monad adjoint
29+
30+
field
31+
Comparison⁻¹ : Functor (EilenbergMoore T) 𝒟
32+
comparison-equiv : WeakInverse (ComparisonF adjoint) Comparison⁻¹

‎src/Categories/Adjoint/Monadic/Crude.agda‎

Lines changed: 174 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,174 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
open import Categories.Adjoint
4+
open import Categories.Category
5+
open import Categories.Functor renaming (id to idF)
6+
7+
-- The crude monadicity theorem. This proof is based off of the version
8+
-- provided in "Sheaves In Geometry and Logic" by Maclane and Moerdijk.
9+
module Categories.Adjoint.Monadic.Crude {o ℓ e o′ ℓ′ e′} {𝒞 : Category o ℓ e} {𝒟 : Category o′ ℓ′ e′}
10+
{L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) where
11+
12+
open import Level
13+
open import Function using (_$_)
14+
open import Data.Product using (Σ-syntax; _,_)
15+
16+
open import Categories.Adjoint.Properties
17+
open import Categories.Adjoint.Monadic
18+
open import Categories.Adjoint.Monadic.Properties
19+
open import Categories.Category.Equivalence using (StrongEquivalence)
20+
open import Categories.Category.Equivalence.Properties using (pointwise-iso-equivalence)
21+
open import Categories.Functor.Properties
22+
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
23+
open import Categories.NaturalTransformation
24+
open import Categories.Monad
25+
26+
open import Categories.Diagram.Coequalizer
27+
open import Categories.Diagram.ReflexivePair
28+
29+
open import Categories.Adjoint.Construction.EilenbergMoore
30+
open import Categories.Category.Construction.EilenbergMoore
31+
open import Categories.Category.Construction.Properties.EilenbergMoore
32+
33+
open import Categories.Morphism
34+
open import Categories.Morphism.Notation
35+
open import Categories.Morphism.Properties
36+
import Categories.Morphism.Reasoning as MR
37+
38+
private
39+
module L = Functor L
40+
module R = Functor R
41+
42+
module 𝒞 = Category 𝒞
43+
module 𝒟 = Category 𝒟
44+
45+
module adjoint = Adjoint adjoint
46+
47+
T : Monad 𝒞
48+
T = adjoint⇒monad adjoint
49+
50+
𝒞ᵀ : Category _ _ _
51+
𝒞ᵀ = EilenbergMoore T
52+
53+
Comparison : Functor 𝒟 𝒞ᵀ
54+
Comparison = ComparisonF adjoint
55+
56+
module Comparison = Functor Comparison
57+
58+
open Coequalizer
59+
60+
-- We could do this with limits, but this is far easier.
61+
PreservesReflexiveCoequalizers : (F : Functor 𝒟 𝒞) → Set _
62+
PreservesReflexiveCoequalizers F = ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → (coeq : Coequalizer 𝒟 f g) → IsCoequalizer 𝒞 (F.F₁ f) (F.F₁ g) (F.F₁ (arr coeq))
63+
where
64+
module F = Functor F
65+
66+
module _ {F : Functor 𝒟 𝒞} (preserves-reflexive-coeq : PreservesReflexiveCoequalizers F) where
67+
open Functor F
68+
69+
-- Unfortunately, we need to prove that the 'coequalize' arrows are equal as a lemma
70+
preserves-coequalizer-unique : ∀ {A B C} {f g : 𝒟 [ A , B ]} {h : 𝒟 [ B , C ]} {eq : 𝒟 [ 𝒟 [ h ∘ f ] ≈ 𝒟 [ h ∘ g ] ]}
71+
→ (reflexive-pair : ReflexivePair 𝒟 f g) → (coe : Coequalizer 𝒟 f g)
72+
→ 𝒞 [ F₁ (coequalize coe eq) ≈ IsCoequalizer.coequalize (preserves-reflexive-coeq reflexive-pair coe) ([ F ]-resp-square eq) ]
73+
preserves-coequalizer-unique reflexive-pair coe = IsCoequalizer.unique (preserves-reflexive-coeq reflexive-pair coe) (F-resp-≈ (universal coe) ○ homomorphism)
74+
where
75+
open 𝒞.HomReasoning
76+
77+
78+
-- If 𝒟 has coequalizers of reflexive pairs, then the comparison functor has a left adjoint.
79+
module _ (has-reflexive-coequalizers : ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → Coequalizer 𝒟 f g) where
80+
81+
private
82+
reflexive-pair : (M : Module T) → ReflexivePair 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M)))
83+
reflexive-pair M = record
84+
{ s = L.F₁ (adjoint.unit.η (Module.A M))
85+
; isReflexivePair = record
86+
{ sectionₗ = begin
87+
𝒟 [ L.F₁ (Module.action M) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ≈˘⟨ L.homomorphism ⟩
88+
L.F₁ (𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] ) ≈⟨ L.F-resp-≈ (Module.identity M) ⟩
89+
L.F₁ 𝒞.id ≈⟨ L.identity ⟩
90+
𝒟.id ∎
91+
; sectionᵣ = begin
92+
𝒟 [ adjoint.counit.η (L.₀ (Module.A M)) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ≈⟨ adjoint.zig ⟩
93+
𝒟.id ∎
94+
}
95+
}
96+
where
97+
open 𝒟.HomReasoning
98+
99+
-- The key part of the proof. As we have all reflexive coequalizers, we can create the following coequalizer.
100+
-- We can think of this as identifying the action of the algebra lifted to a "free" structure
101+
-- and the counit of the adjunction, as the unit of the adjunction (also lifted to the "free structure") is a section of both.
102+
has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M)))
103+
has-coequalizer M = has-reflexive-coequalizers (reflexive-pair M)
104+
105+
module Comparison⁻¹ = Functor (Comparison⁻¹ adjoint has-coequalizer)
106+
module Comparison⁻¹⊣Comparison = Adjoint (Comparison⁻¹⊣Comparison adjoint has-coequalizer)
107+
108+
-- We have one interesting coequalizer in 𝒞 built out of a T-module's action.
109+
coequalizer-action : (M : Module T) → Coequalizer 𝒞 (R.F₁ (L.F₁ (Module.action M))) (R.F₁ (adjoint.counit.η (L.₀ (Module.A M))))
110+
coequalizer-action M = record
111+
{ arr = Module.action M
112+
; isCoequalizer = record
113+
{ equality = Module.commute M
114+
; coequalize = λ {X} {h} eq → 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ]
115+
; universal = λ {C} {h} {eq} → begin
116+
h ≈⟨ introʳ adjoint.zag ○ 𝒞.sym-assoc ⟩
117+
𝒞 [ 𝒞 [ h ∘ R.F₁ (adjoint.counit.η (L.₀ (Module.A M))) ] ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ pushˡ (⟺ eq) ⟩
118+
𝒞 [ h ∘ 𝒞 [ R.F₁ (L.F₁ (Module.action M)) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ] ≈⟨ pushʳ (adjoint.unit.sym-commute (Module.action M)) ⟩
119+
𝒞 [ 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] ∘ Module.action M ] ∎
120+
; unique = λ {X} {h} {i} {eq} eq′ → begin
121+
i ≈⟨ introʳ (Module.identity M) ⟩
122+
𝒞 [ i ∘ 𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] ] ≈⟨ pullˡ (⟺ eq′) ⟩
123+
𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] ∎
124+
}
125+
}
126+
where
127+
open 𝒞.HomReasoning
128+
open MR 𝒞
129+
130+
-- If 'R' preserves reflexive coequalizers, then the unit of the adjunction is a pointwise isomorphism
131+
unit-iso : PreservesReflexiveCoequalizers R → (X : Module T) → Σ[ h ∈ 𝒞ᵀ [ Comparison.F₀ (Comparison⁻¹.F₀ X) , X ] ] (Iso 𝒞ᵀ (Comparison⁻¹⊣Comparison.unit.η X) h)
132+
unit-iso preserves-reflexive-coeq X =
133+
let
134+
coequalizerˣ = has-coequalizer X
135+
coequalizerᴿˣ = ((IsCoequalizer⇒Coequalizer 𝒞 (preserves-reflexive-coeq (reflexive-pair X) (has-coequalizer X))))
136+
coequalizer-iso = up-to-iso 𝒞 (coequalizer-action X) coequalizerᴿˣ
137+
module coequalizer-iso = _≅_ coequalizer-iso
138+
open 𝒞
139+
open 𝒞.HomReasoning
140+
open MR 𝒞
141+
α = record
142+
{ arr = coequalizer-iso.to
143+
; commute = begin
144+
coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _) ≈⟨ introʳ (R.F-resp-≈ L.identity ○ R.identity) ⟩
145+
(coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)) ∘ R.F₁ (L.F₁ 𝒞.id) ≈⟨ pushʳ (R.F-resp-≈ (L.F-resp-≈ (⟺ coequalizer-iso.isoʳ)) ○ R.F-resp-≈ L.homomorphism ○ R.homomorphism) ⟩
146+
((coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)) ∘ R.F₁ (L.F₁ (R.F₁ (arr coequalizerˣ) ∘ adjoint.unit.η _))) ∘ R.F₁ (L.F₁ coequalizer-iso.to) ≈⟨ (refl⟩∘⟨ (R.F-resp-≈ L.homomorphism ○ R.homomorphism)) ⟩∘⟨refl ⟩
147+
((coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)) ∘ R.F₁ (L.F₁ (R.F₁ (arr coequalizerˣ))) ∘ R.F₁ (L.F₁ (adjoint.unit.η _))) ∘ R.F₁ (L.F₁ coequalizer-iso.to) ≈⟨ center ([ R ]-resp-square (adjoint.counit.commute _)) ⟩∘⟨refl ⟩
148+
((coequalizer-iso.to ∘ (R.F₁ (arr coequalizerˣ) ∘ R.F₁ (adjoint.counit.η (L.F₀ _))) ∘ R.F₁ (L.F₁ (adjoint.unit.η _))) ∘ R.F₁ (L.F₁ coequalizer-iso.to)) ≈⟨ (refl⟩∘⟨ cancelʳ (⟺ R.homomorphism ○ R.F-resp-≈ adjoint.zig ○ R.identity)) ⟩∘⟨refl ⟩
149+
(coequalizer-iso.to ∘ R.F₁ (arr coequalizerˣ)) ∘ R.F₁ (L.F₁ coequalizer-iso.to) ≈˘⟨ universal coequalizerᴿˣ ⟩∘⟨refl ⟩
150+
Module.action X ∘ R.F₁ (L.F₁ coequalizer-iso.to) ∎
151+
}
152+
in α , record { isoˡ = coequalizer-iso.isoˡ ; isoʳ = coequalizer-iso.isoʳ }
153+
154+
-- If 'R' preserves reflexive coequalizers and reflects isomorphisms, then the counit of the adjunction is a pointwise isomorphism.
155+
counit-iso : PreservesReflexiveCoequalizers R → Conservative R → (X : 𝒟.Obj) → Σ[ h ∈ 𝒟 [ X , Comparison⁻¹.F₀ (Comparison.F₀ X) ] ] Iso 𝒟 (Comparison⁻¹⊣Comparison.counit.η X) h
156+
counit-iso preserves-reflexive-coeq conservative X =
157+
let coequalizerᴿᴷˣ = IsCoequalizer⇒Coequalizer 𝒞 (preserves-reflexive-coeq (reflexive-pair (Comparison.F₀ X)) (has-coequalizer (Comparison.F₀ X)))
158+
coequalizerᴷˣ = has-coequalizer (Comparison.F₀ X)
159+
coequalizer-iso = up-to-iso 𝒞 coequalizerᴿᴷˣ (coequalizer-action (Comparison.F₀ X))
160+
module coequalizer-iso = _≅_ coequalizer-iso
161+
open 𝒞.HomReasoning
162+
open 𝒞.Equiv
163+
in conservative (Iso-resp-≈ 𝒞 coequalizer-iso.iso (⟺ (preserves-coequalizer-unique {R} preserves-reflexive-coeq (reflexive-pair (Comparison.F₀ X)) coequalizerᴷˣ)) refl)
164+
165+
-- Now, for the final result. Both the unit and counit of the adjunction between the comparison functor and it's inverse are isomorphisms,
166+
-- so therefore they form natural isomorphism. Therfore, we have an equivalence of categories.
167+
crude-monadicity : PreservesReflexiveCoequalizers R → Conservative R → StrongEquivalence 𝒞ᵀ 𝒟
168+
crude-monadicity preserves-reflexlive-coeq conservative = record
169+
{ F = Comparison⁻¹ adjoint has-coequalizer
170+
; G = Comparison
171+
; weak-inverse = pointwise-iso-equivalence (Comparison⁻¹⊣Comparison adjoint has-coequalizer)
172+
(counit-iso preserves-reflexlive-coeq conservative)
173+
(unit-iso preserves-reflexlive-coeq)
174+
}

0 commit comments

Comments
 (0)