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
PullbackConeAPI asmono_fst_of_is_pullback_of_monoandmono_snd_of_is_pullback_of_mono, and using thepullbackAPI aspullback.fst_of_monoandpullback.snd_of_mono.A pullback cone is a limit iff its composition with a monomorphism is a limit. This is available as
IsLimitOfCompMonoandpullbackIsPullbackOfCompMonorespectively.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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
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) ⋯ ⋯ ⋯
Instances For
theorem
CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(t : CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X) ⋯))
:
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 : C}
{X : C}
{Y : C}
{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.
Instances For
def
CategoryTheory.Limits.PullbackCone.isLimitOfCompMono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{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.
Instances For
instance
CategoryTheory.Limits.pullback.fst_of_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Mono g]
:
CategoryTheory.Mono CategoryTheory.Limits.pullback.fst
The pullback of a monomorphism is a monomorphism
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.pullback.snd_of_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Mono f]
:
CategoryTheory.Mono CategoryTheory.Limits.pullback.snd
The pullback of a monomorphism is a monomorphism
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.mono_pullback_to_prod
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{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 CategoryTheory.Limits.pullback.snd)
The map X ×[Z] Y ⟶ X × Y is mono.
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.Limits.pullbackIsPullbackOfCompMono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{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 CategoryTheory.Limits.pullback.snd ⋯)
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}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ W)
(g : Y ⟶ W)
(i : W ⟶ Z)
[CategoryTheory.Mono i]
[CategoryTheory.Limits.HasPullback f g]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasPullback_of_right_factors_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Z : C}
(f : X ⟶ Z)
(i : Z ⟶ W)
[CategoryTheory.Mono i]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.pullback_snd_iso_of_right_factors_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Z : C}
(f : X ⟶ Z)
(i : Z ⟶ W)
[CategoryTheory.Mono i]
:
CategoryTheory.IsIso CategoryTheory.Limits.pullback.snd
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasPullback_of_left_factors_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Z : C}
(f : X ⟶ Z)
(i : Z ⟶ W)
[CategoryTheory.Mono i]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.pullback_snd_iso_of_left_factors_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Z : C}
(f : X ⟶ Z)
(i : Z ⟶ W)
[CategoryTheory.Mono i]
:
CategoryTheory.IsIso CategoryTheory.Limits.pullback.fst
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.has_kernel_pair_of_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.fst_eq_snd_of_mono_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_hom_of_mono_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
instance
CategoryTheory.Limits.fst_iso_of_mono_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
CategoryTheory.IsIso CategoryTheory.Limits.pullback.fst
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.snd_iso_of_mono_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
CategoryTheory.IsIso CategoryTheory.Limits.pullback.snd
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.PushoutCocone.epi_inr_of_is_pushout_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
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) ⋯ ⋯ ⋯
Instances For
theorem
CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(t : CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id 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}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{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.
Instances For
def
CategoryTheory.Limits.PushoutCocone.isColimitOfEpiComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{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)
:
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}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Epi g]
:
CategoryTheory.Epi CategoryTheory.Limits.pushout.inl
The pushout of an epimorphism is an epimorphism
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.pushout.inr_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Epi f]
:
CategoryTheory.Epi CategoryTheory.Limits.pushout.inr
The pushout of an epimorphism is an epimorphism
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.epi_coprod_to_pushout
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{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 CategoryTheory.Limits.pushout.inr)
The map X ⨿ Y ⟶ X ⨿[Z] Y is epi.
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.Limits.pushoutIsPushoutOfEpiComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{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 CategoryTheory.Limits.pushout.inr ⋯)
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}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(h : W ⟶ X)
[CategoryTheory.Epi h]
[CategoryTheory.Limits.HasPushout f g]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasPushout_of_right_factors_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Z : C}
(f : X ⟶ Z)
(h : W ⟶ X)
[CategoryTheory.Epi h]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.pushout_inr_iso_of_right_factors_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Z : C}
(f : X ⟶ Z)
(h : W ⟶ X)
[CategoryTheory.Epi h]
:
CategoryTheory.IsIso CategoryTheory.Limits.pushout.inr
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasPushout_of_left_factors_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
(h : W ⟶ X)
[CategoryTheory.Epi h]
(f : X ⟶ Y)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.pushout_inl_iso_of_left_factors_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
(h : W ⟶ X)
[CategoryTheory.Epi h]
(f : X ⟶ Y)
:
CategoryTheory.IsIso CategoryTheory.Limits.pushout.inl
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.has_cokernel_pair_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.inl_eq_inr_of_epi_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
CategoryTheory.Limits.pushout.inl = CategoryTheory.Limits.pushout.inr
@[simp]
theorem
CategoryTheory.Limits.pullback_symmetry_hom_of_epi_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
instance
CategoryTheory.Limits.inl_iso_of_epi_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
CategoryTheory.IsIso CategoryTheory.Limits.pushout.inl
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.inr_iso_of_epi_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
CategoryTheory.IsIso CategoryTheory.Limits.pushout.inr
Equations
- ⋯ = ⋯