isSplitEpi_prod_fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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