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.

source

@[protected, instance]

def category_theory.monad.monadicity_internal.main_pair_reflexive {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra) :

category_theory.is_reflexive_pair ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))

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.

source

@[protected, instance]

def category_theory.monad.monadicity_internal.main_pair_G_split {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra) :

G.is_split_pair ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))

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.

source

noncomputable def category_theory.monad.monadicity_internal.comparison_left_adjoint_obj {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra) [category_theory.limits.has_coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))] :

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

Equations

category_theory.monad.monadicity_internal.comparison_left_adjoint_obj A = category_theory.limits.coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))

source

@[simp]

theorem category_theory.monad.monadicity_internal.comparison_left_adjoint_hom_equiv_apply_f {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra) (B : D) [category_theory.limits.has_coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))] (ᾰ : category_theory.monad.monadicity_internal.comparison_left_adjoint_obj A ⟶ B) :

source

@[simp]

theorem category_theory.monad.monadicity_internal.comparison_left_adjoint_hom_equiv_symm_apply {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra) (B : D) [category_theory.limits.has_coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))] (ᾰ : A ⟶ (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint G)).obj B) :

source

noncomputable def category_theory.monad.monadicity_internal.comparison_left_adjoint_hom_equiv {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra) (B : D) [category_theory.limits.has_coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))] :

(category_theory.monad.monadicity_internal.comparison_left_adjoint_obj A ⟶ B) ≃ (A ⟶ (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint G)).obj B)

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

Equations

category_theory.monad.monadicity_internal.comparison_left_adjoint_hom_equiv A B = ((category_theory.limits.cofork.is_colimit.hom_iso (category_theory.limits.colimit.is_colimit (category_theory.limits.parallel_pair ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A)))) B).trans (((category_theory.adjunction.of_right_adjoint G).hom_equiv A.A B).subtype_equiv _)).trans {to_fun := λ (g : {g // G.map ((category_theory.left_adjoint G).map g) ≫ G.map ((category_theory.adjunction.of_right_adjoint G).counit.app B) = A.a ≫ g}), {f := ↑g, h' := _}, inv_fun := λ (f : A ⟶ (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint G)).obj B), ⟨f.f, _⟩, left_inv := _, right_inv := _}

source

noncomputable def category_theory.monad.monadicity_internal.left_adjoint_comparison {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] [∀ (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra), category_theory.limits.has_coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))] :

(category_theory.adjunction.of_right_adjoint G).to_monad.algebra ⥤ D

Construct the adjunction to the comparison functor.

Equations

category_theory.monad.monadicity_internal.left_adjoint_comparison = category_theory.adjunction.left_adjoint_of_equiv (λ (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra) (B : D), category_theory.monad.monadicity_internal.comparison_left_adjoint_hom_equiv A B) category_theory.monad.monadicity_internal.left_adjoint_comparison._proof_1

source

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

Equations

category_theory.monad.monadicity_internal.comparison_adjunction = category_theory.adjunction.adjunction_of_equiv_left (λ (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra) (B : D), category_theory.monad.monadicity_internal.comparison_left_adjoint_hom_equiv A B) category_theory.monad.monadicity_internal.comparison_adjunction._proof_4

source

@[simp]

theorem category_theory.monad.monadicity_internal.comparison_adjunction_counit {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] [∀ (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra), category_theory.limits.has_coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))] :

category_theory.monad.monadicity_internal.comparison_adjunction.counit = {app := λ (Y : D), ↑(category_theory.limits.cofork.is_colimit.desc' (category_theory.limits.colimit.is_colimit (category_theory.limits.parallel_pair ((category_theory.left_adjoint G).map (G.map ((category_theory.adjunction.of_right_adjoint G).counit.app Y))) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj (G.obj Y))))) (⇑(((category_theory.adjunction.of_right_adjoint G).hom_equiv (G.obj Y) Y).symm) (𝟙 (G.obj Y))) _), naturality' := _}

source

theorem category_theory.monad.monadicity_internal.comparison_adjunction_unit_f_aux {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] [∀ (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra), category_theory.limits.has_coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))] (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra) :

source

@[simp]

theorem category_theory.monad.monadicity_internal.unit_cofork_X {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra) [category_theory.limits.has_coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))] :

(category_theory.monad.monadicity_internal.unit_cofork A).X = G.obj (category_theory.limits.coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A)))

source

noncomputable def category_theory.monad.monadicity_internal.unit_cofork {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra) [category_theory.limits.has_coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))] :

category_theory.limits.cofork (G.map ((category_theory.left_adjoint G).map A.a)) (G.map ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).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

category_theory.monad.monadicity_internal.unit_cofork A = category_theory.limits.cofork.of_π (G.map (category_theory.limits.coequalizer.π ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A)))) _

source

@[simp]

theorem category_theory.monad.monadicity_internal.unit_cofork_π {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra) [category_theory.limits.has_coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))] :

(category_theory.monad.monadicity_internal.unit_cofork A).π = G.map (category_theory.limits.coequalizer.π ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A)))

source

@[simp]

theorem category_theory.monad.monadicity_internal.counit_cofork_ι_app {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] (B : D) (X : category_theory.limits.walking_parallel_pair) :

(category_theory.monad.monadicity_internal.counit_cofork B).ι.app X = category_theory.limits.walking_parallel_pair.rec ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj (G.obj B)) ≫ (category_theory.adjunction.of_right_adjoint G).counit.app B) ((category_theory.adjunction.of_right_adjoint G).counit.app B) X

source

def category_theory.monad.monadicity_internal.counit_cofork {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] (B : D) :

category_theory.limits.cofork ((category_theory.left_adjoint G).map (G.map ((category_theory.adjunction.of_right_adjoint G).counit.app B))) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj (G.obj B)))

The cofork which describes the counit of the adjunction: the morphism from the coequalizer of this pair to this morphism is the counit.

Equations

category_theory.monad.monadicity_internal.counit_cofork B = category_theory.limits.cofork.of_π ((category_theory.adjunction.of_right_adjoint G).counit.app B) _

source

@[simp]

theorem category_theory.monad.monadicity_internal.counit_cofork_X {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] (B : D) :

(category_theory.monad.monadicity_internal.counit_cofork B).X = B

source

noncomputable def category_theory.monad.monadicity_internal.unit_colimit_of_preserves_coequalizer {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra) [category_theory.limits.has_coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))] [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))) G] :

category_theory.limits.is_colimit (category_theory.monad.monadicity_internal.unit_cofork A)

The unit cofork is a colimit provided G preserves it.

Equations

category_theory.monad.monadicity_internal.unit_colimit_of_preserves_coequalizer A = category_theory.limits.is_colimit_of_has_coequalizer_of_preserves_colimit G ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))

source

The counit cofork is a colimit provided G reflects it.

Equations

category_theory.monad.monadicity_internal.counit_coequalizer_of_reflects_coequalizer B = category_theory.limits.is_colimit_of_is_colimit_cofork_map G _ (category_theory.monad.beck_coequalizer ((category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint G)).obj B))

source

theorem category_theory.monad.monadicity_internal.comparison_adjunction_counit_app {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] [∀ (A : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra), category_theory.limits.has_coequalizer ((category_theory.left_adjoint G).map A.a) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj A.A))] (B : D) :

category_theory.monad.monadicity_internal.comparison_adjunction.counit.app B = category_theory.limits.colimit.desc (category_theory.limits.parallel_pair ((category_theory.left_adjoint G).map (G.map ((category_theory.adjunction.of_right_adjoint G).counit.app B))) ((category_theory.adjunction.of_right_adjoint G).counit.app ((category_theory.left_adjoint G).obj (G.obj B)))) (category_theory.monad.monadicity_internal.counit_cofork B)

source

noncomputable def category_theory.monad.creates_G_split_coequalizers_of_monadic {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [category_theory.monadic_right_adjoint G] ⦃A B : D⦄ (f g : A ⟶ B) [G.is_split_pair f g] :

category_theory.creates_colimit (category_theory.limits.parallel_pair 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 monadic_of_creates_G_split_coequalizers.

Equations

category_theory.monad.creates_G_split_coequalizers_of_monadic G f g = category_theory.monadic_creates_colimit_of_preserves_colimit G (category_theory.limits.parallel_pair f g)

source

noncomputable def category_theory.monad.monadic_of_has_preserves_reflects_G_split_coequalizers {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [category_theory.is_right_adjoint G] [∀ ⦃A B : D⦄ (f g : A ⟶ B) [_inst_5 : G.is_split_pair f g], category_theory.limits.has_coequalizer f g] [Π ⦃A B : D⦄ (f g : A ⟶ B) [_inst_7 : G.is_split_pair f g], category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] [Π ⦃A B : D⦄ (f g : A ⟶ B) [_inst_9 : G.is_split_pair f g], category_theory.limits.reflects_colimit (category_theory.limits.parallel_pair f g) G] :

category_theory.monadic_right_adjoint G

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

Equations

category_theory.monad.monadic_of_has_preserves_reflects_G_split_coequalizers G = let L : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra ⥤ D := category_theory.monad.monadicity_internal.left_adjoint_comparison, i : category_theory.is_right_adjoint (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint G)) := {left := category_theory.monad.monadicity_internal.left_adjoint_comparison _, adj := category_theory.monad.monadicity_internal.comparison_adjunction _} in {to_is_right_adjoint := _inst_3, eqv := let this : ∀ (X : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint G))).unit.app X) := _, this : ∀ (Y : D), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint G))).counit.app Y) := _ in category_theory.adjunction.is_right_adjoint_to_is_equivalence}

source

noncomputable def category_theory.monad.monadic_of_creates_G_split_coequalizers {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [category_theory.is_right_adjoint G] [Π ⦃A B : D⦄ (f g : A ⟶ B) [_inst_5 : G.is_split_pair f g], category_theory.creates_colimit (category_theory.limits.parallel_pair f g) G] :

category_theory.monadic_right_adjoint 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

category_theory.monad.monadic_of_creates_G_split_coequalizers G = let _inst : ∀ ⦃A B : D⦄ (f g : A ⟶ B) [_inst_6 : G.is_split_pair f g], category_theory.limits.has_colimit (category_theory.limits.parallel_pair f g ⋙ G) := _ in category_theory.monad.monadic_of_has_preserves_reflects_G_split_coequalizers G

source

noncomputable def category_theory.monad.monadic_of_has_preserves_G_split_coequalizers_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [category_theory.is_right_adjoint G] [category_theory.reflects_isomorphisms G] [∀ ⦃A B : D⦄ (f g : A ⟶ B) [_inst_6 : G.is_split_pair f g], category_theory.limits.has_coequalizer f g] [Π ⦃A B : D⦄ (f g : A ⟶ B) [_inst_8 : G.is_split_pair f g], category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] :

category_theory.monadic_right_adjoint 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

category_theory.monad.monadic_of_has_preserves_G_split_coequalizers_of_reflects_isomorphisms G = category_theory.monad.monadic_of_has_preserves_reflects_G_split_coequalizers G

source

noncomputable def category_theory.monad.monadic_of_has_preserves_reflexive_coequalizers_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [category_theory.is_right_adjoint G] [category_theory.limits.has_reflexive_coequalizers D] [category_theory.reflects_isomorphisms G] [Π ⦃A B : D⦄ (f g : A ⟶ B) [_inst_7 : category_theory.is_reflexive_pair f g], category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) G] :

category_theory.monadic_right_adjoint 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.

Equations

category_theory.monad.monadic_of_has_preserves_reflexive_coequalizers_of_reflects_isomorphisms G = let L : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra ⥤ D := category_theory.monad.monadicity_internal.left_adjoint_comparison, i : category_theory.is_right_adjoint (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint G)) := {left := category_theory.monad.monadicity_internal.left_adjoint_comparison _, adj := category_theory.monad.monadicity_internal.comparison_adjunction _} in {to_is_right_adjoint := _inst_3, eqv := let this : ∀ (X : (category_theory.adjunction.of_right_adjoint G).to_monad.algebra), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint G))).unit.app X) := _, this : ∀ (Y : D), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint G))).counit.app Y) := _ in category_theory.adjunction.is_right_adjoint_to_is_equivalence}