coproductIso_ι_comp_hom — Mathlib

English

Sigma.inl maps into the coproduct then through the coproduct iso gives the standard inl embedding into the Sigma type.

Русский

Sigma.inl затем через копроизоморфизм даёт стандартное вложение в сумму Σ.

LaTeX

$$$$ \\Sigma\\mathord{.}\\iota F j \\;\\circ\\; (coproductIso F).hom = \\lambda x: F j.\\; \\langle j, x \\rangle $$$$

Lean4

@[elementwise (attr := simp)]
theorem coproductIso_ι_comp_hom {J : Type v} (F : J → Type max v u) (j : J) :
    Sigma.ι F j ≫ (coproductIso F).hom = fun x : F j => (⟨j, x⟩ : Σ j, F j) :=
  colimit.isoColimitCocone_ι_hom (coproductColimitCocone F) ⟨j⟩

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