mathlibdocumentation

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

TODO #

@[protected, instance]
def category_theory.monad.monadicity_internal.main_pair_reflexive {C : Type u₁} {D : Type u₂} {G : D C}  :

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]
def category_theory.monad.monadicity_internal.main_pair_G_split {C : Type u₁} {D : Type u₂} {G : D C}  :

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.

D

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

Equations
@[simp]
theorem category_theory.monad.monadicity_internal.comparison_left_adjoint_hom_equiv_apply_f {C : Type u₁} {D : Type u₂} {G : D C} (B : D)  :
@[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

Construct the adjunction to the comparison functor.

Equations

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

Equations
@[simp]
theorem category_theory.monad.monadicity_internal.unit_cofork_X {C : Type u₁} {D : Type u₂} {G : D C}  :
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]
theorem category_theory.monad.monadicity_internal.unit_cofork_π {C : Type u₁} {D : Type u₂} {G : D C}  :
@[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