# mathlib3documentation

category_theory.monad.monadicity

# Monadicity theorems #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 right adjoint, and:

• D has, G preserves and reflects G-split coequalizers, see category_theory.monad.monadic_of_has_preserves_reflects_G_split_coequalizers
• G creates G-split coequalizers, see category_theory.monad.monadic_of_creates_G_split_coequalizers (The converse of this is also shown, see category_theory.monad.creates_G_split_coequalizers_of_monadic)
• D has and G preserves G-split coequalizers, and G reflects isomorphisms, see category_theory.monad.monadic_of_has_preserves_G_split_coequalizers_of_reflects_isomorphisms
• D has and G preserves reflexive coequalizers, and G reflects isomorphisms, see category_theory.monad.monadic_of_has_preserves_reflexive_coequalizers_of_reflects_isomorphisms

## Tags #

Beck, monadicity, descent

## TODO #

Dualise to show comonadicity theorems.

@[protected, instance]

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.

@[protected, instance]

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.

noncomputable def category_theory.monad.monadicity_internal.comparison_left_adjoint_obj {C : Type u₁} {D : Type u₂} {G : D C}  :
D

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

Equations
@[simp]
@[simp]
noncomputable def category_theory.monad.monadicity_internal.comparison_left_adjoint_hom_equiv {C : Type u₁} {D : Type u₂} {G : D C} (B : D)  :

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

Equations
noncomputable def category_theory.monad.monadicity_internal.left_adjoint_comparison {C : Type u₁} {D : Type u₂} {G : D C}  :

Construct the adjunction to the comparison functor.

Equations

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

Equations
@[simp]
noncomputable def category_theory.monad.monadicity_internal.unit_cofork {C : Type u₁} {D : Type u₂} {G : D C}  :
(G.map

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
@[simp]
@[simp]
theorem category_theory.monad.monadicity_internal.counit_cofork_ι_app {C : Type u₁} {D : Type u₂} {G : D C} (B : D)  :
= category_theory.limits.walking_parallel_pair.rec X
def category_theory.monad.monadicity_internal.counit_cofork {C : Type u₁} {D : Type u₂} {G : D C} (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
@[simp]
theorem category_theory.monad.monadicity_internal.counit_cofork_X {C : Type u₁} {D : Type u₂} {G : D C} (B : D) :

The unit cofork is a colimit provided G preserves it.

Equations

The counit cofork is a colimit provided G reflects it.

Equations
noncomputable def category_theory.monad.creates_G_split_coequalizers_of_monadic {C : Type u₁} {D : Type u₂} (G : D C) ⦃A B : D⦄ (f g : A B) [ 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 monadic_of_creates_G_split_coequalizers.

Equations
noncomputable def category_theory.monad.monadic_of_has_preserves_reflects_G_split_coequalizers {C : Type u₁} {D : Type u₂} (G : D C) [ ⦃A B : D⦄ (f g : A B) [_inst_5 : g], ] [Π ⦃A B : D⦄ (f g : A B) [_inst_7 : g], ] [Π ⦃A B : D⦄ (f g : A B) [_inst_9 : g], ] :

To show G is a monadic right adjoint, we can show it preserves and reflects G-split coequalizers, and C has them.

Equations
noncomputable def category_theory.monad.monadic_of_creates_G_split_coequalizers {C : Type u₁} {D : Type u₂} (G : D C) [Π ⦃A B : D⦄ (f g : A B) [_inst_5 : g], ] :

Beck's monadicity theorem. If G has a right adjoint and creates coequalizers of G-split pairs, then it is monadic. This is the converse of creates_G_split_of_monadic.

Equations
• = let _inst : ⦃A B : D⦄ (f g : A B) [_inst_6 : g], := _ in
noncomputable def category_theory.monad.monadic_of_has_preserves_G_split_coequalizers_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} (G : D C) [ ⦃A B : D⦄ (f g : A B) [_inst_6 : g], ] [Π ⦃A B : D⦄ (f g : A B) [_inst_8 : 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
noncomputable def category_theory.monad.monadic_of_has_preserves_reflexive_coequalizers_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} (G : D C) [Π ⦃A B : D⦄ (f g : A B) [_inst_7 : , ] :

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