mono_map'_of_injective — Mathlib

English

The map Sigma.map' ι (λ j, 𝟙 ((X ∘ ι) j)) is mono when ι is injective and coproducts exist.

Русский

Отображение Sigma.map' ι ... моно при инъективности ι и существовании копроодуктов.

LaTeX

$$$Mono\\ (Sigma.map'\\ ι\\ (\\lambda j. 𝟙 ((X \\circ ι) j))).$$$

Lean4

theorem mono_map'_of_injective [HasCoproduct (X ∘ ι)] [HasCoproduct X]
    [HasCoproduct (fun (k : ((Set.range ι)ᶜ : Set I)) => X k.1)] : Mono (Sigma.map' ι (fun j => 𝟙 ((X ∘ ι) j))) :=
  by
  convert mono_of_injective' X ι hι
  apply Sigma.hom_ext
  intro j
  rw [Sigma.ι_comp_map', id_comp, colimit.ι_desc]
  simp

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