# Documentation

We prove monadicity theorems which can establish a given functor is monadic. In particular, we show three versions of Beck's monadicity theorem, and the reflexive (crude) monadicity theorem:

G is a monadic right adjoint if it has a right adjoint, and:

• D has, G preserves and reflects G-split coequalizers, see CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers
• G creates G-split coequalizers, see CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers (The converse of this is also shown, see CategoryTheory.Monad.createsGSplitCoequalizersOfMonadic)
• D has and G preserves G-split coequalizers, and G reflects isomorphisms, see CategoryTheory.Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms
• D has and G preserves reflexive coequalizers, and G reflects isomorphisms, see CategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms

## TODO #

CategoryTheory.IsReflexivePair (F.map A.a) (adj.counit.app (F.obj A.A))

The "main pair" for an algebra (A, α) is the pair of morphisms (F α, ε_FA). It is always a reflexive pair, and will be used to construct the left adjoint to the comparison functor and show it is an equivalence.

Equations
• =
G.IsSplitPair (F.map A.a) (adj.counit.app (F.obj A.A))

The "main pair" for an algebra (A, α) is the pair of morphisms (F α, ε_FA). It is always a G-split pair, and will be used to construct the left adjoint to the comparison functor and show it is an equivalence.

Equations
• =
D

The object function for the left adjoint to the comparison functor.

Equations
Instances For
@[simp]
@[simp]
∀ (a : A .obj B), = (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A)))) B).symm CategoryTheory.CategoryStruct.comp (F.map a.f) (adj.counit.app B),
(A .obj B)

We have a bijection of homsets which will be used to construct the left adjoint to the comparison functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Construct the adjunction to the comparison functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
= { app := fun (Y : D) => (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))) Y).symm adj.counit.app Y, , naturality := }

Provided we have the appropriate coequalizers, we have an adjunction to the comparison functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
(.app A).f = (adj.homEquiv A.A (CategoryTheory.Limits.coequalizer (F.map A.a) (adj.counit.app (F.obj A.A)))) (CategoryTheory.Limits.coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
@[simp]
= G.obj (CategoryTheory.Limits.coequalizer (F.map A.a) (adj.counit.app (F.obj A.A)))
CategoryTheory.Limits.Cofork (G.map (F.map A.a)) (G.map (adj.counit.app (F.obj A.A)))

This is a cofork which is helpful for establishing monadicity: the morphism from the Beck coequalizer to this cofork is the unit for the adjunction on the comparison functor.

Equations
Instances For
@[simp]
= G.map (CategoryTheory.Limits.coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
@[simp]
theorem CategoryTheory.Monad.MonadicityInternal.counitCofork_ι_app {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } (adj : F G) (B : D) :
@[simp]
theorem CategoryTheory.Monad.MonadicityInternal.counitCofork_pt {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } (adj : F G) (B : D) :
def CategoryTheory.Monad.MonadicityInternal.counitCofork {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } (adj : F G) (B : D) :

The cofork which describes the counit of the adjunction: the morphism from the coequalizer of this pair to this morphism is the counit.

Equations
Instances For
def CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizer {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } {adj : F G} (A : adj.toMonad.Algebra) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G] :

The unit cofork is a colimit provided G preserves it.

Equations
Instances For
def CategoryTheory.Monad.MonadicityInternal.counitCoequalizerOfReflectsCoequalizer {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } (adj : F G) (B : D) [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B)))) G] :

The counit cofork is a colimit provided G reflects it.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Monad.MonadicityInternal.instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } (adj : F G) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (B : D) :
Equations
• =
.app B = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))
def CategoryTheory.Monad.createsGSplitCoequalizersOfMonadic {C : Type u₁} {D : Type u₂} [] [] (G : ) ⦃A : D ⦃B : D (f : A B) (g : A B) [G.IsSplitPair f g] :

If G is monadic, it creates colimits of G-split pairs. This is the "boring" direction of Beck's monadicity theorem, the converse is given in monadicOfCreatesGSplitCoequalizers.

Equations
Instances For
class CategoryTheory.Monad.HasCoequalizerOfIsSplitPair {C : Type u₁} {D : Type u₂} [] [] (G : ) :
• out : ∀ {A B : D} (f g : A B) [inst : G.IsSplitPair f g],
Instances
theorem CategoryTheory.Monad.HasCoequalizerOfIsSplitPair.out {C : Type u₁} {D : Type u₂} [] [] (G : ) {A : D} {B : D} (f : A B) (g : A B) [G.IsSplitPair f g] :
instance CategoryTheory.Monad.instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } (adj : F G) (A : adj.toMonad.Algebra) :
CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
Equations
• =
class CategoryTheory.Monad.PreservesColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [] [] (G : ) :
Type (max (max u₁ u₂) v₁)
• out : {A B : D} → (f g : A B) → [inst : G.IsSplitPair f g] →
Instances
instance CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsSplitPairOfPreservesColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [] [] {G : } {A : D} {B : D} (f : A B) (g : A B) [G.IsSplitPair f g] :
Equations
instance CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } (adj : F G) (A : adj.toMonad.Algebra) :
Equations
• One or more equations did not get rendered due to their size.
class CategoryTheory.Monad.ReflectsColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [] [] (G : ) :
Type (max (max u₁ u₂) v₁)
• out : {A B : D} → (f g : A B) → [inst : G.IsSplitPair f g] →
Instances
instance CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairOfIsSplitPairOfReflectsColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [] [] {G : } {A : D} {B : D} (f : A B) (g : A B) [G.IsSplitPair f g] :
Equations
instance CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } (adj : F G) (A : adj.toMonad.Algebra) :
Equations
• One or more equations did not get rendered due to their size.

To show G is a monadic right adjoint, we can show it preserves and reflects G-split coequalizers, and C has them.

Equations
• = { L := F, adj := adj, eqv := }
Instances For
class CategoryTheory.Monad.CreatesColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [] [] (G : ) :
Type (max (max u₁ u₂) v₁)
• out : {A B : D} → (f g : A B) → [inst : G.IsSplitPair f g] →
Instances
instance CategoryTheory.Monad.instCreatesColimitWalkingParallelPairParallelPairOfIsSplitPairOfCreatesColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [] [] {G : } {A : D} {B : D} (f : A B) (g : A B) [G.IsSplitPair f g] :
Equations
instance CategoryTheory.Monad.instCreatesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfCreatesColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } (adj : F G) (A : adj.toMonad.Algebra) :
CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G
Equations
• One or more equations did not get rendered due to their size.
def CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } (adj : F G) :

Beck's monadicity theorem. If G has a right adjoint and creates coequalizers of G-split pairs, then it is monadic. This is the converse of createsGSplitOfMonadic.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } (adj : F G) [G.ReflectsIsomorphisms] :

An alternate version of Beck's monadicity theorem. If G reflects isomorphisms, preserves coequalizers of G-split pairs and C has coequalizers of G-split pairs, then it is monadic.

Equations
• One or more equations did not get rendered due to their size.
Instances For
class CategoryTheory.Monad.PreservesColimitOfIsReflexivePair {C : Type u₁} {D : Type u₂} [] [] (G : ) :
Type (max (max u₁ u₂) v₁)
• out : A B : C⦄ → (f g : A B) →
Instances
instance CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } (adj : F G) (X : adj.toMonad.Algebra) :
Equations
• One or more equations did not get rendered due to their size.
def CategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms {C : Type u₁} {D : Type u₂} [] [] {G : } {F : } (adj : F G) [G.ReflectsIsomorphisms] :

Reflexive (crude) monadicity theorem. If G has a right adjoint, D has and G preserves reflexive coequalizers and G reflects isomorphisms, then G is monadic.

Equations
• = { L := F, adj := adj, eqv := }
Instances For