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 left 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

This file has been adapted to Mathlib/CategoryTheory/Monad/Comonadicity.lean. Please try to keep them in sync.

Tags

Beck, monadicity, descent

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

instance CategoryTheory.Monad.MonadicityInternal.main_pair_G_split {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : 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.

noncomputable def CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) [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.

noncomputable def CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) (B : D) [Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : (comparisonLeftAdjointObj adj A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)

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

@[simp]

theorem CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) (B : D) [Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (a✝ : A ⟶ (comparison adj).obj B) : (comparisonLeftAdjointHomEquiv adj A B).symm a✝ = (Limits.Cofork.IsColimit.homIso (Limits.colimit.isColimit (Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A)))) B).symm ⟨(adj.homEquiv A.A B).symm a✝.f, ⋯⟩

@[simp]

theorem CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) (B : D) [Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (a✝ : comparisonLeftAdjointObj adj A ⟶ B) : ((comparisonLeftAdjointHomEquiv adj A B) a✝).f = (adj.homEquiv A.A B) ↑((Limits.Cofork.IsColimit.homIso (Limits.colimit.isColimit (Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A)))) B) a✝)

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

Construct the adjunction to the comparison functor.

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

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

@[simp]

theorem CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} (adj : F ⊣ G) [∀ (A : adj.toMonad.Algebra), Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : (comparisonAdjunction adj).counit = { app := fun (Y : D) => (Limits.Cofork.IsColimit.homIso (Limits.colimit.isColimit (Limits.parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))) Y).symm ⟨(adj.homEquiv (G.obj Y) Y).symm (CategoryStruct.id (G.obj Y)), ⋯⟩, naturality := ⋯ }

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

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

@[simp]

theorem CategoryTheory.Monad.MonadicityInternal.unitCofork_pt {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} {adj : F ⊣ G} (A : adj.toMonad.Algebra) [Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : (unitCofork A).pt = G.obj (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₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} {adj : F ⊣ G} (A : adj.toMonad.Algebra) [Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : (unitCofork A).π = G.map (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₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} {adj : F ⊣ G} [∀ (A : adj.toMonad.Algebra), Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (A : adj.toMonad.Algebra) : ((comparisonAdjunction adj).unit.app A).f = (beckCoequalizer A).desc (unitCofork A)

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

@[simp]

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

@[simp]

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

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

The unit cofork is a colimit provided G preserves it.

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

The counit cofork is a colimit provided G reflects it.

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

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

@[implicit_reducible]

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

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

Typeclass expressing that for all G-split pairs f,g, f and g have a coequalizer.

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

instance CategoryTheory.Monad.instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} (adj : F ⊣ G) [HasCoequalizerOfIsSplitPair G] (A : adj.toMonad.Algebra) : Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))

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

Typeclass expressing that for all G-split pairs f,g, G preserves colimits of parallelPair f g.

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

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

instance CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} (adj : F ⊣ G) [PreservesColimitOfIsSplitPair G] (A : adj.toMonad.Algebra) : Limits.PreservesColimit (Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G

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

Typeclass expressing that for all G-split pairs f,g, G reflects colimits for parallelPair f g.

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

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

instance CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} (adj : F ⊣ G) [ReflectsColimitOfIsSplitPair G] (A : adj.toMonad.Algebra) : Limits.ReflectsColimit (Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G

@[implicit_reducible]

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

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

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

Typeclass expressing that for all G-split pairs f,g, G creates colimits of parallelPair f g.

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

  For all G-split pairs f,g, G creates colimits of parallelPair f g.

@[implicit_reducible]

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

@[implicit_reducible]

instance CategoryTheory.Monad.instCreatesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfCreatesColimitOfIsSplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} (adj : F ⊣ G) [CreatesColimitOfIsSplitPair G] (A : adj.toMonad.Algebra) : CreatesColimit (Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G

@[implicit_reducible]

def CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} (adj : F ⊣ G) [CreatesColimitOfIsSplitPair G] : MonadicRightAdjoint G

Beck's monadicity theorem: if G has a left adjoint and creates coequalizers of G-split pairs, then it is monadic. This is the converse of createsGSplitCoequalizersOfMonadic.

@[implicit_reducible]

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

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

Typeclass expressing that for all reflexive pairs f,g, G preserves colimits of parallelPair f g.

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

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

instance CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} (adj : F ⊣ G) [PreservesColimitOfIsReflexivePair G] (X : adj.toMonad.Algebra) : Limits.PreservesColimit (Limits.parallelPair (F.map X.a) (adj.counit.app (F.obj X.A))) G

@[implicit_reducible]

def CategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {G : Functor D C} {F : Functor C D} (adj : F ⊣ G) [Limits.HasReflexiveCoequalizers D] [G.ReflectsIsomorphisms] [PreservesColimitOfIsReflexivePair G] : 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.