biprodIsoProd_inv_comp_fst — Mathlib

English

The inverse of the biprod isomorphism, composed with the biproduct fst, yields the left projection map given by fst on the underlying product.

Русский

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

LaTeX

$$$(biprodIsoProd\ M\ N)^{-1} \circ_{}\; biprod.fst = \mathrm{ofHom}(\mathrm{LinearMap.fst}\; R\; M\; N)$$$

Lean4

@[simp, elementwise]
theorem biprodIsoProd_inv_comp_fst (M N : ModuleCat.{v} R) :
    (biprodIsoProd M N).inv ≫ biprod.fst = ofHom (LinearMap.fst R M N) :=
  IsLimit.conePointUniqueUpToIso_inv_comp _ _ (Discrete.mk WalkingPair.left)

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