ι_comp_coproductIsoSelf_hom — Mathlib

English

For the i-th component, the injection through the Sigma i followed by the coproductIsoSelf hom equals the fromIncl i with identity on the i-th component.

Русский

Для i-го компонента: инъекция через Sigma i затем гомоморфизм coproductIsoSelf равна fromIncl i с единицей на i-м компоненте.

LaTeX

$$$\\Sigma.\\iota\\ X.toFun i \\;\\circ\\; (coproductIsoSelf X).hom = \\mathrm{Hom.fromIncl}\\ i\\ (1_{X.obj i})$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_comp_coproductIsoSelf_hom (i : X.I) : Sigma.ι _ i ≫ (coproductIsoSelf X).hom = .fromIncl i (𝟙 (X.obj i)) := by
  simp [coproductIsoSelf]

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