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}
[Category.{u_2, u_1} C]
{X Y : C}
{f : X ⟶ Y}
{c : Limits.PullbackCone f f}
(hc : Limits.IsLimit c)
:
theorem
CategoryTheory.mono_iff_isIso_fst
{C : Type u_1}
[Category.{u_2, u_1} C]
{X Y : C}
{f : X ⟶ Y}
{c : Limits.PullbackCone f f}
(hc : Limits.IsLimit c)
:
theorem
CategoryTheory.mono_iff_isIso_snd
{C : Type u_1}
[Category.{u_2, u_1} C]
{X Y : C}
{f : X ⟶ Y}
{c : Limits.PullbackCone f f}
(hc : Limits.IsLimit c)
:
theorem
CategoryTheory.mono_iff_isPullback
{C : Type u_1}
[Category.{u_2, u_1} C]
{X Y : C}
(f : X ⟶ Y)
:
Mono f ↔ IsPullback (CategoryStruct.id X) (CategoryStruct.id X) f f
theorem
CategoryTheory.epi_iff_inl_eq_inr
{C : Type u_1}
[Category.{u_2, u_1} C]
{X Y : C}
{f : X ⟶ Y}
{c : Limits.PushoutCocone f f}
(hc : Limits.IsColimit c)
:
theorem
CategoryTheory.epi_iff_isIso_inl
{C : Type u_1}
[Category.{u_2, u_1} C]
{X Y : C}
{f : X ⟶ Y}
{c : Limits.PushoutCocone f f}
(hc : Limits.IsColimit c)
:
theorem
CategoryTheory.epi_iff_isIso_inr
{C : Type u_1}
[Category.{u_2, u_1} C]
{X Y : C}
{f : X ⟶ Y}
{c : Limits.PushoutCocone f f}
(hc : Limits.IsColimit c)
:
theorem
CategoryTheory.epi_iff_isPushout
{C : Type u_1}
[Category.{u_2, u_1} C]
{X Y : C}
(f : X ⟶ Y)
:
Epi f ↔ IsPushout f f (CategoryStruct.id Y) (CategoryStruct.id Y)