Pullbacks and monomorphisms

This file provides some results about interactions between pullbacks and monomorphisms, as well as the dual statements between pushouts and epimorphisms.

Main results

• Monomorphisms are stable under pullback. This is available using the PullbackCone API as mono_fst_of_is_pullback_of_mono and mono_snd_of_is_pullback_of_mono, and using the pullback API as pullback.fst_of_mono and pullback.snd_of_mono.

• A pullback cone is a limit iff its composition with a monomorphism is a limit. This is available as IsLimitOfCompMono and pullbackIsPullbackOfCompMono respectively.

• Monomorphisms admit kernel pairs, this is has_kernel_pair_of_mono.

The dual notions for pushouts are also available.

theorem CategoryTheory.Limits.PullbackCone.mono_snd_of_is_pullback_of_mono {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsLimit t) [Mono f] : Mono t.snd

Monomorphisms are stable under pullback in the first argument.

theorem CategoryTheory.Limits.PullbackCone.mono_fst_of_is_pullback_of_mono {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsLimit t) [Mono g] : Mono t.fst

Monomorphisms are stable under pullback in the second argument.

def CategoryTheory.Limits.PullbackCone.isLimitMkIdId {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : IsLimit (mk (CategoryStruct.id X) (CategoryStruct.id X) ⋯)

The pullback cone (𝟙 X, 𝟙 X) for the pair (f, f) is a limit if f is a mono. The converse is shown in mono_of_pullback_is_id.

theorem CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (t : IsLimit (mk (CategoryStruct.id X) (CategoryStruct.id X) ⋯)) : Mono f

f is a mono if the pullback cone (𝟙 X, 𝟙 X) is a limit for the pair (f, f). The converse is given in PullbackCone.is_id_of_mono.

def CategoryTheory.Limits.PullbackCone.isLimitOfFactors {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ Z) [Mono h] (x : X ⟶ W) (y : Y ⟶ W) (hxh : CategoryStruct.comp x h = f) (hyh : CategoryStruct.comp y h = g) (s : PullbackCone f g) (hs : IsLimit s) : IsLimit (mk s.fst s.snd ⋯)

Suppose f and g are two morphisms with a common codomain and s is a limit cone over the diagram formed by f and g. Suppose f and g both factor through a monomorphism h via x and y, respectively. Then s is also a limit cone over the diagram formed by x and y.

def CategoryTheory.Limits.PullbackCone.isLimitOfCompMono {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ W) (g : Y ⟶ W) (i : W ⟶ Z) [Mono i] (s : PullbackCone f g) (H : IsLimit s) : IsLimit (mk s.fst s.snd ⋯)

If W is the pullback of f, g, it is also the pullback of f ≫ i, g ≫ i for any mono i.

instance CategoryTheory.Limits.pullback.fst_of_mono {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] [Mono g] : Mono (fst f g)

The pullback of a monomorphism is a monomorphism

instance CategoryTheory.Limits.pullback.snd_of_mono {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] [Mono f] : Mono (snd f g)

The pullback of a monomorphism is a monomorphism

instance CategoryTheory.Limits.mono_pullback_to_prod {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasBinaryProduct X Y] : Mono (prod.lift (pullback.fst f g) (pullback.snd f g))

The map X ×[Z] Y ⟶ X × Y is mono.

noncomputable def CategoryTheory.Limits.pullbackIsPullbackOfCompMono {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ W) (g : Y ⟶ W) (i : W ⟶ Z) [Mono i] [HasPullback f g] : IsLimit (PullbackCone.mk (pullback.fst f g) (pullback.snd f g) ⋯)

The pullback of f, g is also the pullback of f ≫ i, g ≫ i for any mono i.

instance CategoryTheory.Limits.hasPullback_of_comp_mono {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ W) (g : Y ⟶ W) (i : W ⟶ Z) [Mono i] [HasPullback f g] : HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)

instance CategoryTheory.Limits.hasPullback_of_right_factors_mono {C : Type u} [Category.{v, u} C] {W X Z : C} (f : X ⟶ Z) (i : Z ⟶ W) [Mono i] : HasPullback i (CategoryStruct.comp f i)

instance CategoryTheory.Limits.pullback_snd_iso_of_right_factors_mono {C : Type u} [Category.{v, u} C] {W X Z : C} (f : X ⟶ Z) (i : Z ⟶ W) [Mono i] : IsIso (pullback.snd i (CategoryStruct.comp f i))

instance CategoryTheory.Limits.hasPullback_of_left_factors_mono {C : Type u} [Category.{v, u} C] {W X Z : C} (f : X ⟶ Z) (i : Z ⟶ W) [Mono i] : HasPullback (CategoryStruct.comp f i) i

instance CategoryTheory.Limits.pullback_snd_iso_of_left_factors_mono {C : Type u} [Category.{v, u} C] {W X Z : C} (f : X ⟶ Z) (i : Z ⟶ W) [Mono i] : IsIso (pullback.fst (CategoryStruct.comp f i) i)

instance CategoryTheory.Limits.has_kernel_pair_of_mono {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : HasPullback f f

theorem CategoryTheory.Limits.PullbackCone.fst_eq_snd_of_mono_eq {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [Mono f] (t : PullbackCone f f) : t.fst = t.snd

theorem CategoryTheory.Limits.fst_eq_snd_of_mono_eq {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : pullback.fst f f = pullback.snd f f

@[simp]

theorem CategoryTheory.Limits.pullbackSymmetry_hom_of_mono_eq {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : (pullbackSymmetry f f).hom = CategoryStruct.id (pullback f f)

theorem CategoryTheory.Limits.PullbackCone.isIso_fst_of_mono_of_isLimit {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [Mono f] {t : PullbackCone f f} (ht : IsLimit t) : IsIso t.fst

theorem CategoryTheory.Limits.PullbackCone.isIso_snd_of_mono_of_isLimit {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [Mono f] {t : PullbackCone f f} (ht : IsLimit t) : IsIso t.snd

instance CategoryTheory.Limits.isIso_fst_of_mono {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : IsIso (pullback.fst f f)

instance CategoryTheory.Limits.isIso_snd_of_mono {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : IsIso (pullback.snd f f)

theorem CategoryTheory.Limits.PushoutCocone.epi_inr_of_is_pushout_of_epi {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : PushoutCocone f g} (ht : IsColimit t) [Epi f] : Epi t.inr

theorem CategoryTheory.Limits.PushoutCocone.epi_inl_of_is_pushout_of_epi {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : PushoutCocone f g} (ht : IsColimit t) [Epi g] : Epi t.inl

def CategoryTheory.Limits.PushoutCocone.isColimitMkIdId {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Epi f] : IsColimit (mk (CategoryStruct.id Y) (CategoryStruct.id Y) ⋯)

The pushout cocone (𝟙 X, 𝟙 X) for the pair (f, f) is a colimit if f is an epi. The converse is shown in epi_of_isColimit_mk_id_id.

theorem CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (t : IsColimit (mk (CategoryStruct.id Y) (CategoryStruct.id Y) ⋯)) : Epi f

f is an epi if the pushout cocone (𝟙 X, 𝟙 X) is a colimit for the pair (f, f). The converse is given in PushoutCocone.isColimitMkIdId.

def CategoryTheory.Limits.PushoutCocone.isColimitOfFactors {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) [Epi h] (x : W ⟶ Y) (y : W ⟶ Z) (hhx : CategoryStruct.comp h x = f) (hhy : CategoryStruct.comp h y = g) (s : PushoutCocone f g) (hs : IsColimit s) : have reassoc₁ := ⋯; have reassoc₂ := ⋯; IsColimit (mk s.inl s.inr ⋯)

Suppose f and g are two morphisms with a common domain and s is a colimit cocone over the diagram formed by f and g. Suppose f and g both factor through an epimorphism h via x and y, respectively. Then s is also a colimit cocone over the diagram formed by x and y.

def CategoryTheory.Limits.PushoutCocone.isColimitOfEpiComp {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : W ⟶ X) [Epi h] (s : PushoutCocone f g) (H : IsColimit s) : IsColimit (mk s.inl s.inr ⋯)

If W is the pushout of f, g, it is also the pushout of h ≫ f, h ≫ g for any epi h.

instance CategoryTheory.Limits.pushout.inl_of_epi {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] [Epi g] : Epi (inl f g)

The pushout of an epimorphism is an epimorphism

instance CategoryTheory.Limits.pushout.inr_of_epi {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] [Epi f] : Epi (inr f g)

The pushout of an epimorphism is an epimorphism

instance CategoryTheory.Limits.epi_coprod_to_pushout {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] [HasBinaryCoproduct Y Z] : Epi (coprod.desc (pushout.inl f g) (pushout.inr f g))

The map X ⨿ Y ⟶ X ⨿[Z] Y is epi.

noncomputable def CategoryTheory.Limits.pushoutIsPushoutOfEpiComp {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : W ⟶ X) [Epi h] [HasPushout f g] : IsColimit (PushoutCocone.mk (pushout.inl f g) (pushout.inr f g) ⋯)

The pushout of f, g is also the pullback of h ≫ f, h ≫ g for any epi h.

instance CategoryTheory.Limits.hasPushout_of_epi_comp {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : W ⟶ X) [Epi h] [HasPushout f g] : HasPushout (CategoryStruct.comp h f) (CategoryStruct.comp h g)

instance CategoryTheory.Limits.hasPushout_of_right_factors_epi {C : Type u} [Category.{v, u} C] {W X Z : C} (f : X ⟶ Z) (h : W ⟶ X) [Epi h] : HasPushout h (CategoryStruct.comp h f)

instance CategoryTheory.Limits.pushout_inr_iso_of_right_factors_epi {C : Type u} [Category.{v, u} C] {W X Z : C} (f : X ⟶ Z) (h : W ⟶ X) [Epi h] : IsIso (pushout.inr h (CategoryStruct.comp h f))

instance CategoryTheory.Limits.hasPushout_of_left_factors_epi {C : Type u} [Category.{v, u} C] {W X Y : C} (h : W ⟶ X) [Epi h] (f : X ⟶ Y) : HasPushout (CategoryStruct.comp h f) h

instance CategoryTheory.Limits.pushout_inl_iso_of_left_factors_epi {C : Type u} [Category.{v, u} C] {W X Y : C} (h : W ⟶ X) [Epi h] (f : X ⟶ Y) : IsIso (pushout.inl (CategoryStruct.comp h f) h)

instance CategoryTheory.Limits.has_cokernel_pair_of_epi {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Epi f] : HasPushout f f

theorem CategoryTheory.Limits.PushoutCocone.inl_eq_inr_of_epi_eq {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [Epi f] (t : PushoutCocone f f) : t.inl = t.inr

theorem CategoryTheory.Limits.inl_eq_inr_of_epi_eq {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Epi f] : pushout.inl f f = pushout.inr f f

@[simp]

theorem CategoryTheory.Limits.pullback_symmetry_hom_of_epi_eq {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Epi f] : (pushoutSymmetry f f).hom = CategoryStruct.id (pushout f f)

theorem CategoryTheory.Limits.PushoutCocone.isIso_inl_of_epi_of_isColimit {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [Epi f] {t : PushoutCocone f f} (ht : IsColimit t) : IsIso t.inl

theorem CategoryTheory.Limits.PushoutCocone.isIso_inr_of_epi_of_isColimit {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [Epi f] {t : PushoutCocone f f} (ht : IsColimit t) : IsIso t.inr

instance CategoryTheory.Limits.isIso_inl_of_epi {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Epi f] : IsIso (pushout.inl f f)

instance CategoryTheory.Limits.isIso_inr_of_epi {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Epi f] : IsIso (pushout.inr f f)