mono_of_injective' — Mathlib

English

Variant stating mono of a desc map in a Sigma-like construction with coproducts.

Русский

Вариант утверждает моно отображения desc в сигма-конструкции с копроодуктами.

LaTeX

$$$Mono\\ (Cofan.IsColimit.desc\\ hc_1\\ (\\lambda i. c.inj (ι i))).$$$

Lean4

theorem mono_of_injective' [HasCoproduct (X ∘ ι)] [HasCoproduct X]
    [HasCoproduct (fun (k : ((Set.range ι)ᶜ : Set I)) => X k.1)] :
    Mono (Sigma.desc (f := X ∘ ι) (fun j => Sigma.ι X (ι j))) :=
  mono_of_injective X ι hι _ _ (colimit.isColimit _) (colimit.isColimit _)

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