biproductIsoPi_inv_comp_π — Mathlib

English

For a finite index set J and a family f:J→AddCommGrpCat, the inverse of biproductIsoPi composed with the j-th projection equals the canonical projection to the j-th component.

Русский

Для конечного множества индексов J и семейства f:J→AddCommGrpCat обратное изоморфизма biproductIsoPi композитной π_j равно канонической проекции на j-компоненту.

LaTeX

$$(biproductIsoPi f)^{-1} \circ \pi f j = ofHom (Pi.evalAddMonoidHom (fun j => (f j).carrier) j)$$

Lean4

@[simp, elementwise]
theorem biproductIsoPi_inv_comp_π (f : J → AddCommGrpCat.{u}) (j : J) :
    (biproductIsoPi f).inv ≫ biproduct.π f j = ofHom (Pi.evalAddMonoidHom (fun j => f j) j) :=
  IsLimit.conePointUniqueUpToIso_inv_comp _ _ (Discrete.mk j)

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