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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) : 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

• ⋯ = ⋯

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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) : 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

• ⋯ = ⋯

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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : D

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

Equations

• CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj adj A = CategoryTheory.Limits.coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))

@[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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) (B : D) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : ∀ (a : CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj adj A ⟶ B), ((CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv adj A B) a).f = CategoryTheory.CategoryStruct.comp (adj.unit.app A.A) (G.map ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) (B : D) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : ∀ (a : A ⟶ (CategoryTheory.Monad.comparison adj).obj B), (CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv adj A B).symm a = (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), ⋯⟩

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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) (B : D) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : (CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj adj A ⟶ B) ≃ (A ⟶ (CategoryTheory.Monad.comparison adj).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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : CategoryTheory.Functor adj.toMonad.Algebra 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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : (CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).counit = { 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 := ⋯ }

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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : CategoryTheory.Monad.MonadicityInternal.leftAdjointComparison adj ⊣ CategoryTheory.Monad.comparison adj

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} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (A : adj.toMonad.Algebra) : ((CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).unit.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]

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} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} (A : adj.toMonad.Algebra) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : (CategoryTheory.Monad.MonadicityInternal.unitCofork A).pt = G.obj (CategoryTheory.Limits.coequalizer (F.map A.a) (adj.counit.app (F.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} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} (A : adj.toMonad.Algebra) [CategoryTheory.Limits.HasCoequalizer (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

• CategoryTheory.Monad.MonadicityInternal.unitCofork A = CategoryTheory.Limits.Cofork.ofπ (G.map (CategoryTheory.Limits.coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))) ⋯

@[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} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} (A : adj.toMonad.Algebra) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : (CategoryTheory.Monad.MonadicityInternal.unitCofork A).π = G.map (CategoryTheory.Limits.coequalizer.π (F.map A.a) (adj.counit.app (F.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} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (A : adj.toMonad.Algebra) : ((CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (B : D) (X : CategoryTheory.Limits.WalkingParallelPair) : (CategoryTheory.Monad.MonadicityInternal.counitCofork adj B).ι.app X = CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.CategoryStruct.comp (adj.counit.app (F.obj (G.obj B))) (adj.counit.app B)) (adj.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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (B : D) : (CategoryTheory.Monad.MonadicityInternal.counitCofork adj 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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (B : D) : CategoryTheory.Limits.Cofork (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.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 adj B = CategoryTheory.Limits.Cofork.ofπ (adj.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} {F : CategoryTheory.Functor C D} {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] : CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.MonadicityInternal.unitCofork A)

The unit cofork is a colimit provided G preserves it.

Equations

• CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizer A = CategoryTheory.Limits.isColimitOfHasCoequalizerOfPreservesColimit G (F.map A.a) (adj.counit.app (F.obj A.A))

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} {F : CategoryTheory.Functor C D} (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] : CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.MonadicityInternal.counitCofork adj 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.instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (B : D) : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (B : D) : (CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).counit.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)))) (CategoryTheory.Monad.MonadicityInternal.counitCofork adj 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) [G.IsSplitPair 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 G 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 : G.IsSplitPair f g], CategoryTheory.Limits.HasCoequalizer f g

theorem CategoryTheory.Monad.HasCoequalizerOfIsSplitPair.out {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] (G : CategoryTheory.Functor D C) [self : CategoryTheory.Monad.HasCoequalizerOfIsSplitPair G] {A : D} {B : D} (f : A ⟶ B) (g : A ⟶ B) [G.IsSplitPair f g] : CategoryTheory.Limits.HasCoequalizer f g

instance CategoryTheory.Monad.instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [CategoryTheory.Monad.HasCoequalizerOfIsSplitPair 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₂} [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 : G.IsSplitPair f g] → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G

instance CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsSplitPairOfPreservesColimitOfIsSplitPair {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) [G.IsSplitPair f g] [CategoryTheory.Monad.PreservesColimitOfIsSplitPair G] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G

Equations

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

instance CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [CategoryTheory.Monad.PreservesColimitOfIsSplitPair G] (A : adj.toMonad.Algebra) : CategoryTheory.Limits.PreservesColimit (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.

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 : G.IsSplitPair f g] → CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair f g) G

instance CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairOfIsSplitPairOfReflectsColimitOfIsSplitPair {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) [G.IsSplitPair f g] [CategoryTheory.Monad.ReflectsColimitOfIsSplitPair G] : CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair f g) G

Equations

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

instance CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [CategoryTheory.Monad.ReflectsColimitOfIsSplitPair G] (A : adj.toMonad.Algebra) : CategoryTheory.Limits.ReflectsColimit (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.monadicOfHasPreservesReflectsGSplitCoequalizers {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ 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

• CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers adj = { L := F, adj := adj, eqv := ⋯ }

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 : G.IsSplitPair f g] → CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair f g) G

instance CategoryTheory.Monad.instCreatesColimitWalkingParallelPairParallelPairOfIsSplitPairOfCreatesColimitOfIsSplitPair {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) [G.IsSplitPair f g] [CategoryTheory.Monad.CreatesColimitOfIsSplitPair G] : CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair f g) G

Equations

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

instance CategoryTheory.Monad.instCreatesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfCreatesColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [CategoryTheory.Monad.CreatesColimitOfIsSplitPair 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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ 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

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

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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [G.ReflectsIsomorphisms] [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

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

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.instPreservesColimitWalkingParallelPairParallelPairOfIsReflexivePairOfPreservesColimitOfIsReflexivePair {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.instPreservesColimitWalkingParallelPairParallelPairOfIsReflexivePairOfPreservesColimitOfIsReflexivePair f g = CategoryTheory.Monad.PreservesColimitOfIsReflexivePair.out f g

instance CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [CategoryTheory.Monad.PreservesColimitOfIsReflexivePair G] (X : adj.toMonad.Algebra) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (F.map X.a) (adj.counit.app (F.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} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [CategoryTheory.Limits.HasReflexiveCoequalizers D] [G.ReflectsIsomorphisms] [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

• CategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms adj = { L := F, adj := adj, eqv := ⋯ }