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. Please try to keep them in sync.

Tags

Beck, comonadicity, descent

instance CategoryTheory.Comonad.ComonadicityInternal.main_pair_coreflexive {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) : CategoryTheory.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.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj adj A = CategoryTheory.Limits.equalizer (G.map A.a) (adj.unit.app (G.toPrefunctor.1 A.A))

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Construct the adjunction to the comparison functor.

Equations

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

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

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

Equations

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

@[simp]

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

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

def CategoryTheory.Comonad.ComonadicityInternal.counitFork {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : CategoryTheory.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.

Equations

• CategoryTheory.Comonad.ComonadicityInternal.counitFork A = CategoryTheory.Limits.Fork.ofι (F.map (CategoryTheory.Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)))) ⋯

@[simp]

theorem CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : (CategoryTheory.Comonad.ComonadicityInternal.counitFork A).pt = F.obj (CategoryTheory.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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : (CategoryTheory.Comonad.ComonadicityInternal.counitFork A).ι = F.map (CategoryTheory.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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (A : adj.toComonad.Coalgebra) : ((CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).counit.app A).f = (CategoryTheory.Comonad.beckEqualizer A).lift (CategoryTheory.Comonad.ComonadicityInternal.counitFork A)

def CategoryTheory.Comonad.ComonadicityInternal.unitFork {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (B : C) : CategoryTheory.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 the equalizer of this pair is the unit.

Equations

• CategoryTheory.Comonad.ComonadicityInternal.unitFork adj B = CategoryTheory.Limits.Fork.ofι (adj.unit.app B) ⋯

@[simp]

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

@[simp]

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

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

The counit fork is a limit provided F preserves it.

Equations

• CategoryTheory.Comonad.ComonadicityInternal.counitLimitOfPreservesEqualizer A = CategoryTheory.Limits.isLimitOfHasEqualizerOfPreservesLimit F (G.map A.a) (adj.unit.app (G.obj A.A))

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

The unit fork is a limit provided F coreflects it.

Equations

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

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

Equations

• ⋯ = ⋯

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

def CategoryTheory.Comonad.createsFSplitEqualizersOfComonadic {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.ComonadicLeftAdjoint F] ⦃A B : C⦄ (f g : A ⟶ B) [F.IsCosplitPair f g] : CategoryTheory.CreatesLimit (CategoryTheory.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.

Equations

• CategoryTheory.Comonad.createsFSplitEqualizersOfComonadic f g = CategoryTheory.comonadicCreatesLimitOfPreservesLimit F (CategoryTheory.Limits.parallelPair f g)

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

Dual to Monad.HasCoequalizerOfIsSplitPair.

• out : ∀ {A B : C} (f g : A ⟶ B) [inst : F.IsCosplitPair f g], CategoryTheory.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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair F] (A : adj.toComonad.Coalgebra) : CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))

Equations

• ⋯ = ⋯

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

Dual to Monad.PreservesColimitOfIsSplitPair.

• out : ∀ {A B : C} (f g : A ⟶ B) [inst : F.IsCosplitPair f g], CategoryTheory.Limits.PreservesLimit (CategoryTheory.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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g] [CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair F] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) F

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Dual to Monad.ReflectsColimitOfIsSplitPair.

• out : ∀ {A B : C} (f g : A ⟶ B) [inst : F.IsCosplitPair f g], CategoryTheory.Limits.ReflectsLimit (CategoryTheory.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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g] [CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair F] : CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.parallelPair f g) F

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• CategoryTheory.Comonad.comonadicOfHasPreservesReflectsFSplitEqualizers adj = { R := G, adj := adj, eqv := ⋯ }

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

Dual to Monad.CreatesColimitOfIsSplitPair.

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

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

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

Equations

• CategoryTheory.Comonad.instCreatesLimitWalkingParallelPairParallelPairOfIsCosplitPairOfCreatesLimitOfIsCosplitPair f g = CategoryTheory.Comonad.CreatesLimitOfIsCosplitPair.out f g

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

Equations

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

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

Equations

• CategoryTheory.Comonad.comonadicOfCreatesFSplitEqualizers adj = CategoryTheory.Comonad.comonadicOfHasPreservesReflectsFSplitEqualizers adj

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

Equations

• CategoryTheory.Comonad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms adj = CategoryTheory.Comonad.comonadicOfHasPreservesReflectsFSplitEqualizers adj

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

Dual to Monad.PreservesColimitOfIsReflexivePair.

• out : ∀ ⦃A B : C⦄ (f g : A ⟶ B) [inst : CategoryTheory.IsCoreflexivePair f g], CategoryTheory.Limits.PreservesLimit (CategoryTheory.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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {A B : C} (f g : A ⟶ B) [CategoryTheory.IsCoreflexivePair f g] [CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair F] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) F

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.Comonad.comonadicOfHasPreservesCoreflexiveEqualizersOfReflectsIsomorphisms adj = { R := G, adj := adj, eqv := ⋯ }