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 reflectsF
-split equalizers, seeCategoryTheory.Monad.comonadicOfHasPreservesReflectsFSplitEqualizers
F
createsF
-split coequalizers, seeCategoryTheory.Monad.comonadicOfCreatesFSplitEqualizers
(The converse of this is also shown, seeCategoryTheory.Monad.createsFSplitEqualizersOfComonadic
)C
has andF
preservesF
-split equalizers, andF
reflects isomorphisms, seeCategoryTheory.Monad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms
C
has andF
preserves coreflexive equalizers, andF
reflects isomorphisms, seeCategoryTheory.Monad.comonadicOfHasPreservesCoreflexiveEqualizersOfReflectsIsomorphisms
This file has been adapted from Mathlib.CategoryTheory.Monad.Monadicity
.
Please try to keep them in sync.
Tags #
Beck, comonadicity, descent
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
- ⋯ = ⋯
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
- ⋯ = ⋯
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))
Instances For
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.
Instances For
Construct the adjunction to the comparison functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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)))) ⋯
Instances For
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) ⋯
Instances For
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))
Instances For
The unit fork is a limit provided F
coreflects it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
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
Instances For
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 anF
-cosplit pair, then they have an equalizer.
Instances
If f, g
is an F
-cosplit pair, then they have an equalizer.
Equations
- ⋯ = ⋯
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 anF
-cosplit pair, thenF
preserves limits ofparallelPair f g
.
Instances
Equations
- One or more equations did not get rendered due to their size.
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 anF
-cosplit pair, thenF
reflects limits forparallelPair f g
.
Instances
Equations
- One or more equations did not get rendered due to their size.
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 := ⋯ }
Instances For
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 anF
-cosplit pair, thenF
creates limits ofparallelPair f g
.
Instances
Equations
- One or more equations did not get rendered due to their size.
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
Instances For
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
Instances For
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, thenF
preserves limits ofparallelPair f g
.
Instances
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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 := ⋯ }