biproductIsoPi_inv_comp_π — Mathlib

English

The inverse component of the isomorphism interacts with the projection π_j to yield the standard basis projection.

Русский

Обратный компонент изоморфизма взаимодействует с проекцией π_j и даёт стандартную базовую проекцию.

LaTeX

$$$(\mathrm{biproductIsoPi}(f))^{-1} \circ \pi_j = \mathrm{ofHom}(\mathrm{proj}_j)$$$

Lean4

@[simp, elementwise]
theorem biproductIsoPi_inv_comp_π [Finite J] (f : J → ModuleCat.{v} R) (j : J) :
    (biproductIsoPi f).inv ≫ biproduct.π f j = ofHom (LinearMap.proj j : (∀ j, f j) →ₗ[R] f j) :=
  IsLimit.conePointUniqueUpToIso_inv_comp _ _ (Discrete.mk j)

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