Comonadicity theorems

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

F is a comonadic left adjoint if it has a right adjoint, and:

• C has, F preserves and reflects F-split equalizers, see CategoryTheory.Monad.comonadicOfHasPreservesReflectsFSplitEqualizers
• F creates F-split coequalizers, see CategoryTheory.Monad.comonadicOfCreatesFSplitEqualizers (The converse of this is also shown, see CategoryTheory.Monad.createsFSplitEqualizersOfComonadic)
• C has and F preserves F-split equalizers, and F reflects isomorphisms, see CategoryTheory.Monad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms
• C has and F preserves coreflexive equalizers, and F reflects isomorphisms, see CategoryTheory.Monad.comonadicOfHasPreservesCoreflexiveEqualizersOfReflectsIsomorphisms

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

Tags

Beck, comonadicity, descent

instance CategoryTheory.Comonad.ComonadicityInternal.main_pair_coreflexive {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) : IsCoreflexivePair (G.map A.a) (adj.unit.app (G.obj A.A))

The "main pair" for a coalgebra (A, α) is the pair of morphisms (G α, η_GA). It is always a coreflexive pair, and will be used to construct the left adjoint to the comparison functor and show it is an equivalence.

instance CategoryTheory.Comonad.ComonadicityInternal.main_pair_F_cosplit {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) : F.IsCosplitPair (G.map A.a) (adj.unit.app (G.obj A.A))

The "main pair" for a coalgebra (A, α) is the pair of morphisms (G α, η_GA). It is always a G-cosplit pair, and will be used to construct the right adjoint to the comparison functor and show it is an equivalence.

noncomputable def CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) [Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.1 A.A))] : C

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

noncomputable def CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) (B : C) [Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : ((comparison adj).obj B ⟶ A) ≃ (B ⟶ comparisonRightAdjointObj adj A)

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

@[simp]

theorem CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) (B : C) [Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (f : B ⟶ comparisonRightAdjointObj adj A) : ((comparisonRightAdjointHomEquiv adj A B).symm f).f = (adj.homEquiv B A.A).symm (CategoryStruct.comp f (Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))))

@[simp]

theorem CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) (B : C) [Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (f : (comparison adj).obj B ⟶ A) : (comparisonRightAdjointHomEquiv adj A B) f = Limits.equalizer.lift ((adj.homEquiv B A.A) f.f) ⋯

noncomputable def CategoryTheory.Comonad.ComonadicityInternal.rightAdjointComparison {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : Functor adj.toComonad.Coalgebra C

Construct the adjunction to the comparison functor.

noncomputable def CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : comparison adj ⊣ rightAdjointComparison adj

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

@[simp]

theorem CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : (comparisonAdjunction adj).counit = { app := fun (Y : adj.toComonad.Coalgebra) => (comparisonRightAdjointHomEquiv adj Y (comparisonRightAdjointObj adj Y)).symm (CategoryStruct.id (comparisonRightAdjointObj adj Y)), naturality := ⋯ }

theorem CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f_aux {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} {adj : F ⊣ G} [∀ (A : adj.toComonad.Coalgebra), Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (A : adj.toComonad.Coalgebra) : ((comparisonAdjunction adj).counit.app A).f = (adj.homEquiv (Limits.equalizer (G.map A.a) (adj.unit.app (G.obj A.A))) A.A).symm (Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)))

noncomputable def CategoryTheory.Comonad.ComonadicityInternal.counitFork {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : Limits.Fork (F.map (G.map A.a)) (F.map (adj.unit.app (G.obj A.A)))

This is a fork which is helpful for establishing comonadicity: the morphism from this fork to the Beck equalizer is the counit for the adjunction on the comparison functor.

@[simp]

theorem CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : (counitFork A).pt = F.obj (Limits.equalizer (G.map A.a) (adj.unit.app (G.obj A.A)))

@[simp]

theorem CategoryTheory.Comonad.ComonadicityInternal.unitFork_ι {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : (counitFork A).ι = F.map (Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)))

theorem CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} {adj : F ⊣ G} [∀ (A : adj.toComonad.Coalgebra), Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (A : adj.toComonad.Coalgebra) : ((comparisonAdjunction adj).counit.app A).f = (beckEqualizer A).lift (counitFork A)

def CategoryTheory.Comonad.ComonadicityInternal.unitFork {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (B : C) : Limits.Fork (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))

The fork which describes the unit of the adjunction: the morphism from this fork to the equalizer of this pair is the unit.

@[simp]

theorem CategoryTheory.Comonad.ComonadicityInternal.unitFork_pt {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (B : C) : (unitFork adj B).pt = B

@[simp]

theorem CategoryTheory.Comonad.ComonadicityInternal.unitFork_π_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (B : C) (X : Limits.WalkingParallelPair) : (unitFork adj B).π.app X = Limits.WalkingParallelPair.rec (motive := fun (t : Limits.WalkingParallelPair) => X = t → (B ⟶ (Limits.parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))).obj X)) (fun (h : X = Limits.WalkingParallelPair.zero) => ⋯ ▸ adj.unit.app B) (fun (h : X = Limits.WalkingParallelPair.one) => ⋯ ▸ CategoryStruct.comp (adj.unit.app B) (G.map (F.map (adj.unit.app B)))) X ⋯

noncomputable def CategoryTheory.Comonad.ComonadicityInternal.counitLimitOfPreservesEqualizer {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] [Limits.PreservesLimit (Limits.parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F] : Limits.IsLimit (counitFork A)

The counit fork is a limit provided F preserves it.

noncomputable def CategoryTheory.Comonad.ComonadicityInternal.unitEqualizerOfCoreflectsEqualizer {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) (B : C) [Limits.ReflectsLimit (Limits.parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) F] : Limits.IsLimit (unitFork adj B)

The unit fork is a limit provided F coreflects it.

instance CategoryTheory.Comonad.ComonadicityInternal.instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (B : C) : Limits.HasLimit (Limits.parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B))))

theorem CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_unit_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (B : C) : (comparisonAdjunction adj).unit.app B = Limits.limit.lift (Limits.parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (unitFork adj B)

@[implicit_reducible]

noncomputable def CategoryTheory.Comonad.createsFSplitEqualizersOfComonadic {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} [ComonadicLeftAdjoint F] ⦃A B : C⦄ (f g : A ⟶ B) [F.IsCosplitPair f g] : CreatesLimit (Limits.parallelPair f g) F

If F is comonadic, it creates limits of F-cosplit pairs. This is the "boring" direction of Beck's comonadicity theorem, the converse is given in comonadicOfCreatesFSplitEqualizers.

class CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (F : Functor C D) : Prop

Dual to Monad.HasCoequalizerOfIsSplitPair.

• out {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g] : Limits.HasEqualizer f g

  If f, g is an F-cosplit pair, then they have an equalizer.

instance CategoryTheory.Comonad.instHasEqualizerMapAAppUnitObjAOfHasEqualizerOfIsCosplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [HasEqualizerOfIsCosplitPair F] (A : adj.toComonad.Coalgebra) : Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))

class CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (F : Functor C D) : Prop

Dual to Monad.PreservesColimitOfIsSplitPair.

• out {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g] : Limits.PreservesLimit (Limits.parallelPair f g) F

  If f, g is an F-cosplit pair, then F preserves limits of parallelPair f g.

instance CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairOfIsCosplitPairOfPreservesLimitOfIsCosplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g] [PreservesLimitOfIsCosplitPair F] : Limits.PreservesLimit (Limits.parallelPair f g) F

instance CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [PreservesLimitOfIsCosplitPair F] (A : adj.toComonad.Coalgebra) : Limits.PreservesLimit (Limits.parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F

class CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (F : Functor C D) : Prop

Dual to Monad.ReflectsColimitOfIsSplitPair.

• out {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g] : Limits.ReflectsLimit (Limits.parallelPair f g) F

  If f, g is an F-cosplit pair, then F reflects limits for parallelPair f g.

instance CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairOfIsCosplitPairOfReflectsLimitOfIsCosplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g] [ReflectsLimitOfIsCosplitPair F] : Limits.ReflectsLimit (Limits.parallelPair f g) F

instance CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [ReflectsLimitOfIsCosplitPair F] (A : adj.toComonad.Coalgebra) : Limits.ReflectsLimit (Limits.parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F

@[implicit_reducible]

def CategoryTheory.Comonad.comonadicOfHasPreservesReflectsFSplitEqualizers {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [HasEqualizerOfIsCosplitPair F] [PreservesLimitOfIsCosplitPair F] [ReflectsLimitOfIsCosplitPair F] : ComonadicLeftAdjoint F

To show F is a comonadic left adjoint, we can show it preserves and reflects F-split equalizers, and C has them.

class CategoryTheory.Comonad.CreatesLimitOfIsCosplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (F : Functor C D) : Type (max (max u₁ u₂) v₁)

Dual to Monad.CreatesColimitOfIsSplitPair.

• out {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g] : CreatesLimit (Limits.parallelPair f g) F

  If f, g is an F-cosplit pair, then F creates limits of parallelPair f g.

@[implicit_reducible]

instance CategoryTheory.Comonad.instCreatesLimitWalkingParallelPairParallelPairOfIsCosplitPairOfCreatesLimitOfIsCosplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g] [CreatesLimitOfIsCosplitPair F] : CreatesLimit (Limits.parallelPair f g) F

@[implicit_reducible]

instance CategoryTheory.Comonad.instCreatesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfCreatesLimitOfIsCosplitPair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [CreatesLimitOfIsCosplitPair F] (A : adj.toComonad.Coalgebra) : CreatesLimit (Limits.parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F

@[implicit_reducible]

def CategoryTheory.Comonad.comonadicOfCreatesFSplitEqualizers {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [CreatesLimitOfIsCosplitPair F] : ComonadicLeftAdjoint F

Beck's comonadicity theorem. If F has a right adjoint and creates equalizers of F-cosplit pairs, then it is comonadic. This is the converse of createsFSplitEqualizersOfComonadic.

@[implicit_reducible]

def CategoryTheory.Comonad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.ReflectsIsomorphisms] [HasEqualizerOfIsCosplitPair F] [PreservesLimitOfIsCosplitPair F] : ComonadicLeftAdjoint F

An alternate version of Beck's comonadicity theorem. If F reflects isomorphisms, preserves equalizers of F-cosplit pairs and C has equalizers of F-cosplit pairs, then it is comonadic.

class CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (F : Functor C D) : Prop

Dual to Monad.PreservesColimitOfIsReflexivePair.

• out ⦃A B : C⦄ (f g : A ⟶ B) [IsCoreflexivePair f g] : Limits.PreservesLimit (Limits.parallelPair f g) F

  f, g is a coreflexive pair, then F preserves limits of parallelPair f g.

instance CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairOfIsCoreflexivePairOfPreservesLimitOfIsCoreflexivePair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {A B : C} (f g : A ⟶ B) [IsCoreflexivePair f g] [PreservesLimitOfIsCoreflexivePair F] : Limits.PreservesLimit (Limits.parallelPair f g) F

instance CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [PreservesLimitOfIsCoreflexivePair F] (X : adj.toComonad.Coalgebra) : Limits.PreservesLimit (Limits.parallelPair (G.map X.a) (adj.unit.app (G.obj X.A))) F

@[implicit_reducible]

def CategoryTheory.Comonad.comonadicOfHasPreservesCoreflexiveEqualizersOfReflectsIsomorphisms {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [Limits.HasCoreflexiveEqualizers C] [F.ReflectsIsomorphisms] [PreservesLimitOfIsCoreflexivePair F] : ComonadicLeftAdjoint F

Coreflexive (crude) comonadicity theorem. If F has a right adjoint, C has and F preserves coreflexive equalizers and F reflects isomorphisms, then F is comonadic.