ι_mono — Mathlib

English

In a finite biproduct, each injection ι_f j is a split monomorphism; there exists a retraction given by biproduct.desc (Pi.single j id).

Русский

В конечном биопродукте каждый инъектор ι_f j является разложимым моно; существует отрезок-обратное, заданное biproduct.desc (Pi.single j id).

LaTeX

$$$ \\text{IsSplitMono}( \\text{biproduct.ι } f j ) $$$

Lean4

instance ι_mono (f : J → C) [HasBiproduct f] (b : J) : IsSplitMono (biproduct.ι f b) := by
  classical exact IsSplitMono.mk' { retraction := biproduct.desc <| Pi.single b (𝟙 (f b)) }

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