fromIncl_comp_coproductIsoSelf_inv

English

Inverse compatibility: the inclusion into the i-th summand composed with the inverse of coproductIsoSelf recovers the i-th cofan injection.

Русский

Обратная совместимость: включение в i-ую сумму, затем обратная сторона coproductIsoSelf, восстанавливают инъекцию i-ого кофана.

LaTeX

$$$\\mathrm{Hom.fromIncl}\\; i\\; (1_{X.obj i}) \\; \\circ \\; (\\mathrm{coproductIsoSelf}\\ X)^{-1} = (\\mathrm{cofan}\\ X.I\\ X.toFun).inj i$$$

Lean4

@[reassoc (attr := simp)]
theorem fromIncl_comp_coproductIsoSelf_inv (i : X.I) :
    Hom.fromIncl i (𝟙 (X.obj i)) ≫ (coproductIsoSelf X).inv = Sigma.ι X.toFun i :=
  (Iso.comp_inv_eq _).2 (ι_comp_coproductIsoSelf_hom _ _).symm

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