binaryCoproductIso_inr_comp_hom — Mathlib

English

The map Sigma.ι F j composed with the coproduct isomorphism sends x ∈ F j to the pair ⟨j, x⟩ in Σ j, F j, matching the right injection.

Русский

Отображение Sigma.ι F j, композиция с копроизоморфизмом отправляет x ∈ F j в пару ⟨j, x⟩ в Σ j, F j, соответствуя правому вложению.

LaTeX

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

Lean4

@[elementwise (attr := simp)]
theorem binaryCoproductIso_inr_comp_hom (X Y : Type u) : Limits.coprod.inr ≫ (binaryCoproductIso X Y).hom = Sum.inr :=
  colimit.isoColimitCocone_ι_hom (binaryCoproductColimitCocone X Y) ⟨WalkingPair.right⟩

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