# 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} {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} {t : } (ht : ) :

Monomorphisms are stable under pullback in the first argument.

theorem CategoryTheory.Limits.PullbackCone.mono_fst_of_is_pullback_of_mono {C : Type u} {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} {t : } (ht : ) :

Monomorphisms are stable under pullback in the second argument.

def CategoryTheory.Limits.PullbackCone.isLimitMkIdId {C : Type u} {X : C} {Y : C} (f : X Y) :

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
Instances For
theorem CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId {C : Type u} {X : C} {Y : C} (f : X Y) :

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} {W : C} {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) (h : W Z) (x : X W) (y : Y W) (hxh : ) (hyh : ) (s : ) (hs : ) :

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.
Instances For
def CategoryTheory.Limits.PullbackCone.isLimitOfCompMono {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : X W) (g : Y W) (i : W Z) (s : ) :

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.
Instances For
instance CategoryTheory.Limits.pullback.fst_of_mono {C : Type u} {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} :

The pullback of a monomorphism is a monomorphism

Equations
• =
instance CategoryTheory.Limits.pullback.snd_of_mono {C : Type u} {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} :

The pullback of a monomorphism is a monomorphism

Equations
• =
instance CategoryTheory.Limits.mono_pullback_to_prod {C : Type u_1} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) :

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

Equations
• =
noncomputable def CategoryTheory.Limits.pullbackIsPullbackOfCompMono {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : X W) (g : Y W) (i : W Z) :

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.
Instances For
instance CategoryTheory.Limits.hasPullback_of_comp_mono {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : X W) (g : Y W) (i : W Z) :
Equations
• =
instance CategoryTheory.Limits.hasPullback_of_right_factors_mono {C : Type u} {W : C} {X : C} {Z : C} (f : X Z) (i : Z W) :
Equations
• =
instance CategoryTheory.Limits.pullback_snd_iso_of_right_factors_mono {C : Type u} {W : C} {X : C} {Z : C} (f : X Z) (i : Z W) :
Equations
• =
instance CategoryTheory.Limits.hasPullback_of_left_factors_mono {C : Type u} {W : C} {X : C} {Z : C} (f : X Z) (i : Z W) :
Equations
• =
instance CategoryTheory.Limits.pullback_snd_iso_of_left_factors_mono {C : Type u} {W : C} {X : C} {Z : C} (f : X Z) (i : Z W) :
Equations
• =
instance CategoryTheory.Limits.has_kernel_pair_of_mono {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• =
theorem CategoryTheory.Limits.fst_eq_snd_of_mono_eq {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.Limits.pullbackSymmetry_hom_of_mono_eq {C : Type u} {X : C} {Y : C} (f : X Y) :
instance CategoryTheory.Limits.fst_iso_of_mono_eq {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• =
instance CategoryTheory.Limits.snd_iso_of_mono_eq {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• =
theorem CategoryTheory.Limits.PushoutCocone.epi_inr_of_is_pushout_of_epi {C : Type u} {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} {t : } (ht : ) :
theorem CategoryTheory.Limits.PushoutCocone.epi_inl_of_is_pushout_of_epi {C : Type u} {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} {t : } (ht : ) :
def CategoryTheory.Limits.PushoutCocone.isColimitMkIdId {C : Type u} {X : C} {Y : C} (f : X 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
Instances For
theorem CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId {C : Type u} {X : C} {Y : C} (f : X Y) :

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} {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) (h : X W) (x : W Y) (y : W Z) (hhx : ) (hhy : ) (s : ) (hs : ) :
let_fun reassoc₁ := ; let_fun reassoc₂ := ;

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.
Instances For
def CategoryTheory.Limits.PushoutCocone.isColimitOfEpiComp {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) (h : W X) (s : ) :

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.
Instances For
instance CategoryTheory.Limits.pushout.inl_of_epi {C : Type u} {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} :

The pushout of an epimorphism is an epimorphism

Equations
• =
instance CategoryTheory.Limits.pushout.inr_of_epi {C : Type u} {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} :

The pushout of an epimorphism is an epimorphism

Equations
• =
instance CategoryTheory.Limits.epi_coprod_to_pushout {C : Type u_1} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) :

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

Equations
• =
noncomputable def CategoryTheory.Limits.pushoutIsPushoutOfEpiComp {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) (h : W X) :

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.
Instances For
instance CategoryTheory.Limits.hasPushout_of_epi_comp {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) (h : W X) :
Equations
• =
instance CategoryTheory.Limits.hasPushout_of_right_factors_epi {C : Type u} {W : C} {X : C} {Z : C} (f : X Z) (h : W X) :
Equations
• =
instance CategoryTheory.Limits.pushout_inr_iso_of_right_factors_epi {C : Type u} {W : C} {X : C} {Z : C} (f : X Z) (h : W X) :
Equations
• =
instance CategoryTheory.Limits.hasPushout_of_left_factors_epi {C : Type u} {W : C} {X : C} {Y : C} (h : W X) (f : X Y) :
Equations
• =
instance CategoryTheory.Limits.pushout_inl_iso_of_left_factors_epi {C : Type u} {W : C} {X : C} {Y : C} (h : W X) (f : X Y) :
Equations
• =
instance CategoryTheory.Limits.has_cokernel_pair_of_epi {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• =
theorem CategoryTheory.Limits.inl_eq_inr_of_epi_eq {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.Limits.pullback_symmetry_hom_of_epi_eq {C : Type u} {X : C} {Y : C} (f : X Y) :
instance CategoryTheory.Limits.inl_iso_of_epi_eq {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• =
instance CategoryTheory.Limits.inr_iso_of_epi_eq {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• =