Monadicity theorems

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

Tags

Beck, monadicity, descent

TODO

Dualise to show comonadicity theorems.

instance CategoryTheory.Monad.MonadicityInternal.main_pair_reflexive {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) : CategoryTheory.IsReflexivePair ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).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

• ⋯ = ⋯

instance CategoryTheory.Monad.MonadicityInternal.main_pair_G_split {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) : CategoryTheory.Functor.IsSplitPair G ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).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

• ⋯ = ⋯

def CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) [CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] : D

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

Equations

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

@[simp]

theorem CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) (B : D) [CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] : ∀ (a : CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj A ⟶ B), ((CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv A B) a).f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.ofRightAdjoint G).unit.app A.A) (G.map ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A)))) B) a))

@[simp]

theorem CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) (B : D) [CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] : ∀ (a : A ⟶ (CategoryTheory.Monad.comparison (CategoryTheory.Adjunction.ofRightAdjoint G)).obj B), (CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv A B).symm a = (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A)))) B).symm { val := CategoryTheory.CategoryStruct.comp ((CategoryTheory.leftAdjoint G).map a.f) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app B), property := ⋯ }

def CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) (B : D) [CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] : (CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj A ⟶ B) ≃ (A ⟶ (CategoryTheory.Monad.comparison (CategoryTheory.Adjunction.ofRightAdjoint G)).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.

def CategoryTheory.Monad.MonadicityInternal.leftAdjointComparison {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [∀ (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))), CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] : CategoryTheory.Functor (CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) D

Construct the adjunction to the comparison functor.

Equations

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

@[simp]

theorem CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [∀ (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))), CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] : CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction.counit = { app := fun (Y : D) => (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair ((CategoryTheory.leftAdjoint G).map (G.map ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app Y))) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj (G.obj Y))))) Y).symm { val := (CategoryTheory.Adjunction.ofRightAdjoint G).counit.app Y, property := ⋯ }, naturality := ⋯ }

def CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [∀ (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))), CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] : CategoryTheory.Monad.MonadicityInternal.leftAdjointComparison ⊣ CategoryTheory.Monad.comparison (CategoryTheory.Adjunction.ofRightAdjoint G)

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.

theorem CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [∀ (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))), CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) : (CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction.unit.app A).f = ((CategoryTheory.Adjunction.ofRightAdjoint G).homEquiv A.A (CategoryTheory.Limits.coequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A)))) (CategoryTheory.Limits.coequalizer.π ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A)))

@[simp]

theorem CategoryTheory.Monad.MonadicityInternal.unitCofork_pt {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) [CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] : (CategoryTheory.Monad.MonadicityInternal.unitCofork A).pt = G.obj (CategoryTheory.Limits.coequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A)))

def CategoryTheory.Monad.MonadicityInternal.unitCofork {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) [CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] : CategoryTheory.Limits.Cofork (G.map ((CategoryTheory.leftAdjoint G).map A.a)) (G.map ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).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

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

@[simp]

theorem CategoryTheory.Monad.MonadicityInternal.unitCofork_π {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) [CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] : CategoryTheory.Limits.Cofork.π (CategoryTheory.Monad.MonadicityInternal.unitCofork A) = G.map (CategoryTheory.Limits.coequalizer.π ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A)))

theorem CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [∀ (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))), CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) : (CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction.unit.app A).f = (CategoryTheory.Monad.beckCoequalizer A).desc (CategoryTheory.Monad.MonadicityInternal.unitCofork A)

@[simp]

theorem CategoryTheory.Monad.MonadicityInternal.counitCofork_ι_app {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (B : D) (X : CategoryTheory.Limits.WalkingParallelPair) : (CategoryTheory.Monad.MonadicityInternal.counitCofork B).ι.app X = CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj (G.obj B))) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app B)) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app B) X

@[simp]

theorem CategoryTheory.Monad.MonadicityInternal.counitCofork_pt {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (B : D) : (CategoryTheory.Monad.MonadicityInternal.counitCofork B).pt = B

def CategoryTheory.Monad.MonadicityInternal.counitCofork {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (B : D) : CategoryTheory.Limits.Cofork ((CategoryTheory.leftAdjoint G).map (G.map ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app B))) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj (G.obj B)))

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

Equations

• CategoryTheory.Monad.MonadicityInternal.counitCofork B = CategoryTheory.Limits.Cofork.ofπ ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app B) ⋯

def CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizer {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) [CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))) G] : CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.MonadicityInternal.unitCofork A)

The unit cofork is a colimit provided G preserves it.

Equations

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

def CategoryTheory.Monad.MonadicityInternal.counitCoequalizerOfReflectsCoequalizer {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] (B : D) [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair ((CategoryTheory.leftAdjoint G).map (G.map ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app B))) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj (G.obj B)))) G] : CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.MonadicityInternal.counitCofork B)

The counit cofork is a colimit provided G reflects it.

Equations

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

instance CategoryTheory.Monad.MonadicityInternal.instHasColimitWalkingParallelPairWalkingParallelPairHomCategoryParallelPairObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorLeftAdjointObjToPrefunctorObjToPrefunctorCompIdMapMapAppCounitOfRightAdjoint {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [∀ (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))), CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] (B : D) : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair ((CategoryTheory.leftAdjoint G).map (G.map ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app B))) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj (G.obj B))))

Equations

• ⋯ = ⋯

theorem CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit_app {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [∀ (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))), CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))] (B : D) : CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction.counit.app B = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair ((CategoryTheory.leftAdjoint G).map (G.map ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app B))) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj (G.obj B)))) (CategoryTheory.Monad.MonadicityInternal.counitCofork B)

def CategoryTheory.Monad.createsGSplitCoequalizersOfMonadic {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.MonadicRightAdjoint G] ⦃A : D⦄ ⦃B : D⦄ (f : A ⟶ B) (g : A ⟶ B) [CategoryTheory.Functor.IsSplitPair G f g] : CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair f g) 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

• CategoryTheory.Monad.createsGSplitCoequalizersOfMonadic f g = CategoryTheory.monadicCreatesColimitOfPreservesColimit G (CategoryTheory.Limits.parallelPair f g)

class CategoryTheory.Monad.HasCoequalizerOfIsSplitPair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] (G : CategoryTheory.Functor D C) : Prop

• out : ∀ {A B : D} (f g : A ⟶ B) [inst : CategoryTheory.Functor.IsSplitPair G f g], CategoryTheory.Limits.HasCoequalizer f g

instance CategoryTheory.Monad.instForAllAlgebraToMonadLeftAdjointOfRightAdjointHasCoequalizerObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorObjToPrefunctorToFunctorAMapAAppCompIdCounit {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [CategoryTheory.Monad.HasCoequalizerOfIsSplitPair G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) : CategoryTheory.Limits.HasCoequalizer ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))

Equations

• ⋯ = ⋯

class CategoryTheory.Monad.PreservesColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] (G : CategoryTheory.Functor D C) : Type (max (max u₁ u₂) v₁)

• out : {A B : D} → (f g : A ⟶ B) → [inst : CategoryTheory.Functor.IsSplitPair G f g] → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G

instance CategoryTheory.Monad.instPreservesColimitWalkingParallelPairWalkingParallelPairHomCategoryParallelPair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {A : D} {B : D} (f : A ⟶ B) (g : A ⟶ B) [CategoryTheory.Functor.IsSplitPair G f g] [CategoryTheory.Monad.PreservesColimitOfIsSplitPair G] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G

Equations

• CategoryTheory.Monad.instPreservesColimitWalkingParallelPairWalkingParallelPairHomCategoryParallelPair f g = CategoryTheory.Monad.PreservesColimitOfIsSplitPair.out f g

instance CategoryTheory.Monad.instForAllAlgebraToMonadLeftAdjointOfRightAdjointPreservesColimitWalkingParallelPairWalkingParallelPairHomCategoryParallelPairObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorObjToPrefunctorToFunctorAMapAAppCompIdCounit {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [CategoryTheory.Monad.PreservesColimitOfIsSplitPair G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))) G

Equations

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

class CategoryTheory.Monad.ReflectsColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] (G : CategoryTheory.Functor D C) : Type (max (max u₁ u₂) v₁)

• out : {A B : D} → (f g : A ⟶ B) → [inst : CategoryTheory.Functor.IsSplitPair G f g] → CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair f g) G

instance CategoryTheory.Monad.instReflectsColimitWalkingParallelPairWalkingParallelPairHomCategoryParallelPair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {A : D} {B : D} (f : A ⟶ B) (g : A ⟶ B) [CategoryTheory.Functor.IsSplitPair G f g] [CategoryTheory.Monad.ReflectsColimitOfIsSplitPair G] : CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair f g) G

Equations

• CategoryTheory.Monad.instReflectsColimitWalkingParallelPairWalkingParallelPairHomCategoryParallelPair f g = CategoryTheory.Monad.ReflectsColimitOfIsSplitPair.out f g

instance CategoryTheory.Monad.instForAllAlgebraToMonadLeftAdjointOfRightAdjointReflectsColimitWalkingParallelPairWalkingParallelPairHomCategoryParallelPairObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorObjToPrefunctorToFunctorAMapAAppCompIdCounit {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [CategoryTheory.Monad.ReflectsColimitOfIsSplitPair G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) : CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj A.A))) G

Equations

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

def CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [CategoryTheory.Monad.HasCoequalizerOfIsSplitPair G] [CategoryTheory.Monad.PreservesColimitOfIsSplitPair G] [CategoryTheory.Monad.ReflectsColimitOfIsSplitPair G] : CategoryTheory.MonadicRightAdjoint G

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

Equations

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

class CategoryTheory.Monad.CreatesColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] (G : CategoryTheory.Functor D C) : Type (max (max u₁ u₂) v₁)

• out : {A B : D} → (f g : A ⟶ B) → [inst : CategoryTheory.Functor.IsSplitPair G f g] → CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair f g) G

instance CategoryTheory.Monad.instCreatesColimitWalkingParallelPairWalkingParallelPairHomCategoryParallelPair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {A : D} {B : D} (f : A ⟶ B) (g : A ⟶ B) [CategoryTheory.Functor.IsSplitPair G f g] [CategoryTheory.Monad.CreatesColimitOfIsSplitPair G] : CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair f g) G

Equations

• CategoryTheory.Monad.instCreatesColimitWalkingParallelPairWalkingParallelPairHomCategoryParallelPair f g = CategoryTheory.Monad.CreatesColimitOfIsSplitPair.out f g

instance CategoryTheory.Monad.instForAllAlgebraToMonadLeftAdjointOfRightAdjointCreatesColimitWalkingParallelPairWalkingParallelPairHomCategoryParallelPairObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorObjToPrefunctorToFunctorAMapAAppCompIdCounit {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [CategoryTheory.Monad.CreatesColimitOfIsSplitPair G] (A : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) : CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair ((CategoryTheory.leftAdjoint G).map A.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [CategoryTheory.Monad.CreatesColimitOfIsSplitPair G] : CategoryTheory.MonadicRightAdjoint 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

• CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers = let I := ⋯; CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers

def CategoryTheory.Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [CategoryTheory.ReflectsIsomorphisms G] [CategoryTheory.Monad.HasCoequalizerOfIsSplitPair G] [CategoryTheory.Monad.PreservesColimitOfIsSplitPair G] : CategoryTheory.MonadicRightAdjoint G

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

• CategoryTheory.Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms = CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers

class CategoryTheory.Monad.PreservesColimitOfIsReflexivePair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] (G : CategoryTheory.Functor C D) : Type (max (max u₁ u₂) v₁)

• out : ⦃A B : C⦄ → (f g : A ⟶ B) → [inst : CategoryTheory.IsReflexivePair f g] → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G

instance CategoryTheory.Monad.instPreservesColimitWalkingParallelPairWalkingParallelPairHomCategoryParallelPair_1 {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {A : D} {B : D} (f : A ⟶ B) (g : A ⟶ B) [CategoryTheory.IsReflexivePair f g] [CategoryTheory.Monad.PreservesColimitOfIsReflexivePair G] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G

Equations

• CategoryTheory.Monad.instPreservesColimitWalkingParallelPairWalkingParallelPairHomCategoryParallelPair_1 f g = CategoryTheory.Monad.PreservesColimitOfIsReflexivePair.out f g

instance CategoryTheory.Monad.instForAllAlgebraToMonadLeftAdjointOfRightAdjointPreservesColimitWalkingParallelPairWalkingParallelPairHomCategoryParallelPairObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorObjToPrefunctorToFunctorAMapAAppCompIdCounit_1 {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [CategoryTheory.Monad.PreservesColimitOfIsReflexivePair G] (X : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint G))) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair ((CategoryTheory.leftAdjoint G).map X.a) ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app ((CategoryTheory.leftAdjoint G).obj X.A))) G

Equations

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

def CategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} [CategoryTheory.IsRightAdjoint G] [CategoryTheory.Limits.HasReflexiveCoequalizers D] [CategoryTheory.ReflectsIsomorphisms G] [CategoryTheory.Monad.PreservesColimitOfIsReflexivePair G] : CategoryTheory.MonadicRightAdjoint G

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

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