isSplitEpi_prod_snd — Mathlib

English

In a category with zero morphisms, projections into a product are split epimorphisms. Specifically snd: X × Y → Y has a section s: Y → X × Y given by prod.lift 0 (id_Y), so snd ∘ s = id_Y.

Русский

В категории с нулевыми морфизмами проекции на произведение являются разделимыми эпиморфизмами. snd: X × Y → Y имеет секцию s: Y → X × Y, заданную prod.lift 0 (id_Y), тогда snd ∘ s = id_Y.

LaTeX

$$$\exists s: Y \to X \times Y\quad\text{such that}\quad \mathrm{snd} \;\circ\; s = \mathrm{id}_Y.$$$

Lean4

/-- In the presence of zero morphisms, projections into a product are (split) epimorphisms. -/
instance isSplitEpi_prod_snd [HasZeroMorphisms C] {X Y : C} [HasLimit (pair X Y)] : IsSplitEpi (prod.snd : X ⨯ Y ⟶ Y) :=
  IsSplitEpi.mk' { section_ := prod.lift 0 (𝟙 Y) }

Похожие утверждения