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.

@[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.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.

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

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

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

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.

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

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.

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.

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

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.