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} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsLimit t) [CategoryTheory.Mono f] : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsLimit t) [CategoryTheory.Mono g] : CategoryTheory.Mono t.fst

Monomorphisms are stable under pullback in the second argument.

def CategoryTheory.Limits.PullbackCone.isLimitMkIdId {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.id X) (CategoryTheory.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.

Equations

• CategoryTheory.Limits.PullbackCone.isLimitMkIdId f = CategoryTheory.Limits.PullbackCone.IsLimit.mk ⋯ (fun (s : CategoryTheory.Limits.PullbackCone f f) => s.fst) ⋯ ⋯ ⋯

theorem CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X) ⋯)) : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ Z) [CategoryTheory.Mono h] (x : X ⟶ W) (y : Y ⟶ W) (hxh : CategoryTheory.CategoryStruct.comp x h = f) (hyh : CategoryTheory.CategoryStruct.comp y h = g) (s : CategoryTheory.Limits.PullbackCone f g) (hs : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.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.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.PullbackCone.isLimitOfCompMono {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ W) (g : Y ⟶ W) (i : W ⟶ Z) [CategoryTheory.Mono i] (s : CategoryTheory.Limits.PullbackCone f g) (H : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.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.

Equations

• One or more equations did not get rendered due to their size.

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

The pullback of a monomorphism is a monomorphism

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

The pullback of a monomorphism is a monomorphism

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

def CategoryTheory.Limits.PushoutCocone.isColimitMkIdId {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.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.

Equations

• CategoryTheory.Limits.PushoutCocone.isColimitMkIdId f = CategoryTheory.Limits.PushoutCocone.IsColimit.mk ⋯ (fun (s : CategoryTheory.Limits.PushoutCocone f f) => s.inl) ⋯ ⋯ ⋯

theorem CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (t : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y) ⋯)) : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) [CategoryTheory.Epi h] (x : W ⟶ Y) (y : W ⟶ Z) (hhx : CategoryTheory.CategoryStruct.comp h x = f) (hhy : CategoryTheory.CategoryStruct.comp h y = g) (s : CategoryTheory.Limits.PushoutCocone f g) (hs : CategoryTheory.Limits.IsColimit s) : let_fun reassoc₁ := ⋯; let_fun reassoc₂ := ⋯; CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.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.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.PushoutCocone.isColimitOfEpiComp {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : W ⟶ X) [CategoryTheory.Epi h] (s : CategoryTheory.Limits.PushoutCocone f g) (H : CategoryTheory.Limits.IsColimit s) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.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.

Equations

• One or more equations did not get rendered due to their size.

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

The pushout of an epimorphism is an epimorphism

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

The pushout of an epimorphism is an epimorphism

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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