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:
Dhas,Gpreserves and reflectsG-split coequalizers, seeCategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizersGcreatesG-split coequalizers, seeCategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers(The converse of this is also shown, seeCategoryTheory.Monad.createsGSplitCoequalizersOfMonadic)Dhas andGpreservesG-split coequalizers, andGreflects isomorphisms, seeCategoryTheory.Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphismsDhas andGpreserves reflexive coequalizers, andGreflects 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
instance
CategoryTheory.Monad.MonadicityInternal.main_pair_reflexive
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
(A : adj.toMonad.Algebra)
:
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.
instance
CategoryTheory.Monad.MonadicityInternal.main_pair_G_split
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
(A : adj.toMonad.Algebra)
:
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.
def
CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
(A : adj.toMonad.Algebra)
[Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
:
D
The object function for the left adjoint to the comparison functor.
Equations
Instances For
def
CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
(A : adj.toMonad.Algebra)
(B : D)
[Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
:
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
@[simp]
theorem
CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
(A : adj.toMonad.Algebra)
(B : D)
[Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
(a✝ : A ⟶ (comparison adj).obj B)
:
@[simp]
theorem
CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
(A : adj.toMonad.Algebra)
(B : D)
[Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
(a✝ : comparisonLeftAdjointObj adj A ⟶ B)
:
def
CategoryTheory.Monad.MonadicityInternal.leftAdjointComparison
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[∀ (A : adj.toMonad.Algebra), Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
:
Construct the adjunction to the comparison functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[∀ (A : adj.toMonad.Algebra), Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
:
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
@[simp]
theorem
CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[∀ (A : adj.toMonad.Algebra), Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
:
(comparisonAdjunction adj).counit = {
app := fun (Y : D) =>
(Limits.Cofork.IsColimit.homIso
(Limits.colimit.isColimit
(Limits.parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y)))))
Y).symm
⟨(adj.homEquiv (G.obj Y) Y).symm (CategoryStruct.id (G.obj Y)), ⋯⟩,
naturality := ⋯ }
theorem
CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
{adj : F ⊣ G}
[∀ (A : adj.toMonad.Algebra), Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
(A : adj.toMonad.Algebra)
:
def
CategoryTheory.Monad.MonadicityInternal.unitCofork
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
{adj : F ⊣ G}
(A : adj.toMonad.Algebra)
[Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
:
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
Instances For
@[simp]
theorem
CategoryTheory.Monad.MonadicityInternal.unitCofork_pt
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
{adj : F ⊣ G}
(A : adj.toMonad.Algebra)
[Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
:
@[simp]
theorem
CategoryTheory.Monad.MonadicityInternal.unitCofork_π
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
{adj : F ⊣ G}
(A : adj.toMonad.Algebra)
[Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
:
theorem
CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
{adj : F ⊣ G}
[∀ (A : adj.toMonad.Algebra), Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
(A : adj.toMonad.Algebra)
:
def
CategoryTheory.Monad.MonadicityInternal.counitCofork
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
(B : D)
:
The cofork which describes the counit of the adjunction: the morphism from the coequalizer of this pair to this morphism is the counit.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Monad.MonadicityInternal.counitCofork_pt
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
(B : D)
:
@[simp]
theorem
CategoryTheory.Monad.MonadicityInternal.counitCofork_ι_app
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
(B : D)
(X : Limits.WalkingParallelPair)
:
def
CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizer
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
{adj : F ⊣ G}
(A : adj.toMonad.Algebra)
[Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
[Limits.PreservesColimit (Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G]
:
The unit cofork is a colimit provided G preserves it.
Equations
Instances For
def
CategoryTheory.Monad.MonadicityInternal.counitCoequalizerOfReflectsCoequalizer
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
(B : D)
[Limits.ReflectsColimit (Limits.parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B)))) G]
:
Limits.IsColimit (counitCofork adj B)
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
instance
CategoryTheory.Monad.MonadicityInternal.instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[∀ (A : adj.toMonad.Algebra), Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
(B : D)
:
Limits.HasColimit (Limits.parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))
theorem
CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit_app
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[∀ (A : adj.toMonad.Algebra), Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
(B : D)
:
def
CategoryTheory.Monad.createsGSplitCoequalizersOfMonadic
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
(G : Functor D C)
[MonadicRightAdjoint G]
⦃A B : D⦄
(f g : A ⟶ B)
[G.IsSplitPair f g]
:
CreatesColimit (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.
Equations
Instances For
class
CategoryTheory.Monad.HasCoequalizerOfIsSplitPair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
(G : Functor D C)
:
Instances
instance
CategoryTheory.Monad.instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[HasCoequalizerOfIsSplitPair G]
(A : adj.toMonad.Algebra)
:
class
CategoryTheory.Monad.PreservesColimitOfIsSplitPair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
(G : Functor D C)
:
- out {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g] : Limits.PreservesColimit (Limits.parallelPair f g) G
Instances
instance
CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsSplitPairOfPreservesColimitOfIsSplitPair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{A B : D}
(f g : A ⟶ B)
[G.IsSplitPair f g]
[PreservesColimitOfIsSplitPair G]
:
instance
CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[PreservesColimitOfIsSplitPair G]
(A : adj.toMonad.Algebra)
:
Limits.PreservesColimit (Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G
class
CategoryTheory.Monad.ReflectsColimitOfIsSplitPair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
(G : Functor D C)
:
- out {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g] : Limits.ReflectsColimit (Limits.parallelPair f g) G
Instances
instance
CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairOfIsSplitPairOfReflectsColimitOfIsSplitPair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{A B : D}
(f g : A ⟶ B)
[G.IsSplitPair f g]
[ReflectsColimitOfIsSplitPair G]
:
instance
CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[ReflectsColimitOfIsSplitPair G]
(A : adj.toMonad.Algebra)
:
Limits.ReflectsColimit (Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G
def
CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[HasCoequalizerOfIsSplitPair G]
[PreservesColimitOfIsSplitPair G]
[ReflectsColimitOfIsSplitPair G]
:
To show G is a monadic right adjoint, we can show it preserves and reflects G-split
coequalizers, and D has them.
Equations
Instances For
class
CategoryTheory.Monad.CreatesColimitOfIsSplitPair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
(G : Functor D C)
:
Type (max (max u₁ u₂) v₁)
Instances
instance
CategoryTheory.Monad.instCreatesColimitWalkingParallelPairParallelPairOfIsSplitPairOfCreatesColimitOfIsSplitPair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{A B : D}
(f g : A ⟶ B)
[G.IsSplitPair f g]
[CreatesColimitOfIsSplitPair G]
:
CreatesColimit (Limits.parallelPair f g) G
instance
CategoryTheory.Monad.instCreatesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfCreatesColimitOfIsSplitPair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[CreatesColimitOfIsSplitPair G]
(A : adj.toMonad.Algebra)
:
CreatesColimit (Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[CreatesColimitOfIsSplitPair G]
:
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
def
CategoryTheory.Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[G.ReflectsIsomorphisms]
[HasCoequalizerOfIsSplitPair G]
[PreservesColimitOfIsSplitPair 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.
Equations
Instances For
class
CategoryTheory.Monad.PreservesColimitOfIsReflexivePair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
(G : Functor C D)
:
- out ⦃A B : C⦄ (f g : A ⟶ B) [IsReflexivePair f g] : Limits.PreservesColimit (Limits.parallelPair f g) G
Instances
instance
CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsReflexivePairOfPreservesColimitOfIsReflexivePair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{A B : D}
(f g : A ⟶ B)
[IsReflexivePair f g]
[PreservesColimitOfIsReflexivePair G]
:
instance
CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[PreservesColimitOfIsReflexivePair G]
(X : adj.toMonad.Algebra)
:
Limits.PreservesColimit (Limits.parallelPair (F.map X.a) (adj.counit.app (F.obj X.A))) G
def
CategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₁, u₂} D]
{G : Functor D C}
{F : Functor C D}
(adj : F ⊣ G)
[Limits.HasReflexiveCoequalizers D]
[G.ReflectsIsomorphisms]
[PreservesColimitOfIsReflexivePair 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.