isSplitEpi_pi_π — Mathlib

English

Projections into a product are split epimorphisms in presence of zero morphisms: Pi.π f b has a retraction given by Pi.lift(Pi.single b id).

Русский

Проекции в произведении являются разложимыми эпиморфизмами при наличии нулевых морфизмов: Pi.π f b имеет развёртку, задаваемую Pi.lift (Pi.single b id).

LaTeX

$$$$\\mathrm{IsSplitEpi}(\\mathrm{Pi.\\pi}\\ f\\ b).$$$$

Lean4

/-- In the presence of zero morphisms, projections into a product are (split) epimorphisms. -/
instance isSplitEpi_pi_π {β : Type u'} [HasZeroMorphisms C] (f : β → C) [HasLimit (Discrete.functor f)] (b : β) :
    IsSplitEpi (Pi.π f b) := by classical exact IsSplitEpi.mk' { section_ := Pi.lift <| Pi.single b (𝟙 _) }

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