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 reflectsG
-split coequalizers, seeCategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers
G
createsG
-split coequalizers, seeCategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers
(The converse of this is also shown, seeCategoryTheory.Monad.createsGSplitCoequalizersOfMonadic
)D
has andG
preservesG
-split coequalizers, andG
reflects isomorphisms, seeCategoryTheory.Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms
D
has andG
preserves reflexive coequalizers, andG
reflects isomorphisms, seeCategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms
This file has been adapted to Mathlib.CategoryTheory.Monad.Comonadicity
.
Please try to keep them in sync.
Tags #
Beck, monadicity, descent
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.
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.
The object function for the left adjoint to the comparison functor.
Equations
- CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj adj A = CategoryTheory.Limits.coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
Instances For
We have a bijection of homsets which will be used to construct the left 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 coequalizers, 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 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.
Equations
- CategoryTheory.Monad.MonadicityInternal.unitCofork A = CategoryTheory.Limits.Cofork.ofπ (G.map (CategoryTheory.Limits.coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))) ⋯
Instances For
The cofork which describes the counit of the adjunction: the morphism from the coequalizer of this pair to this morphism is the counit.
Equations
- CategoryTheory.Monad.MonadicityInternal.counitCofork adj B = CategoryTheory.Limits.Cofork.ofπ (adj.counit.app B) ⋯
Instances For
The unit cofork is a colimit provided G
preserves it.
Equations
- CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizer A = CategoryTheory.Limits.isColimitOfHasCoequalizerOfPreservesColimit G (F.map A.a) (adj.counit.app (F.obj A.A))
Instances For
The counit cofork is a colimit provided G
reflects it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
.
Equations
Instances For
- out : ∀ {A B : D} (f g : A ⟶ B) [inst : G.IsSplitPair f g], CategoryTheory.Limits.HasCoequalizer f g
Instances
- out : ∀ {A B : D} (f g : A ⟶ B) [inst : G.IsSplitPair f g], CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G
Instances
- out : ∀ {A B : D} (f g : A ⟶ B) [inst : G.IsSplitPair f g], CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair f g) G
Instances
To show G
is a monadic right adjoint, we can show it preserves and reflects G
-split
coequalizers, and D
has them.
Equations
- CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers adj = { L := F, adj := adj, eqv := ⋯ }
Instances For
- out : {A B : D} → (f g : A ⟶ B) → [inst : G.IsSplitPair f g] → CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair f g) G
Instances
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
Instances For
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.
Equations
Instances For
- out : ∀ ⦃A B : C⦄ (f g : A ⟶ B) [inst : CategoryTheory.IsReflexivePair f g], CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G
Instances
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.
Equations
- CategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms adj = { L := F, adj := adj, eqv := ⋯ }