Relation between mono/epi and pullback/pushout squares #
In this file, monomorphisms and epimorphisms are characterized in terms
of pullback and pushout squares. For example, we obtain mono_iff_isPullback
which asserts that a morphism f : X ⟶ Y is a monomorphism iff the obvious
square
X ⟶ X
| |
v v
X ⟶ Y
is a pullback square.
theorem
CategoryTheory.mono_iff_fst_eq_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{c : CategoryTheory.Limits.PullbackCone f f}
(hc : CategoryTheory.Limits.IsLimit c)
:
CategoryTheory.Mono f ↔ c.fst = c.snd
theorem
CategoryTheory.mono_iff_isIso_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{c : CategoryTheory.Limits.PullbackCone f f}
(hc : CategoryTheory.Limits.IsLimit c)
:
CategoryTheory.Mono f ↔ CategoryTheory.IsIso c.fst
theorem
CategoryTheory.mono_iff_isIso_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{c : CategoryTheory.Limits.PullbackCone f f}
(hc : CategoryTheory.Limits.IsLimit c)
:
CategoryTheory.Mono f ↔ CategoryTheory.IsIso c.snd
theorem
CategoryTheory.mono_iff_isPullback
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.epi_iff_inl_eq_inr
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{c : CategoryTheory.Limits.PushoutCocone f f}
(hc : CategoryTheory.Limits.IsColimit c)
:
CategoryTheory.Epi f ↔ c.inl = c.inr
theorem
CategoryTheory.epi_iff_isIso_inl
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{c : CategoryTheory.Limits.PushoutCocone f f}
(hc : CategoryTheory.Limits.IsColimit c)
:
CategoryTheory.Epi f ↔ CategoryTheory.IsIso c.inl
theorem
CategoryTheory.epi_iff_isIso_inr
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{c : CategoryTheory.Limits.PushoutCocone f f}
(hc : CategoryTheory.Limits.IsColimit c)
:
CategoryTheory.Epi f ↔ CategoryTheory.IsIso c.inr
theorem
CategoryTheory.epi_iff_isPushout
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
: