English
Let M and N be modules over a ring R. The biproduct M ⊕ N is canonically identified with the cartesian product M × N, and the inverse of the biproduct-to-product isomorphism sends the second projection to the natural linear map snd: M ⊕ N → N.
Русский
Пусть M и N — модули над кольцом R. Двупродукт M ⊕ N естественным образом идентифицируется с прямым произведением M × N; обратный к изоморфизму между двупродуктом и произведением отображает вторую проекцию на естественную линейную карту snd: M ⊕ N → N.
LaTeX
$$$$(biprodIsoProd(M,N))^{-1} \circ biprod.snd = \operatorname{ofHom}(\mathrm{LinearMap.snd}\ R\ M\ N).$$$$
Lean4
@[simp, elementwise]
theorem biprodIsoProd_inv_comp_snd (M N : ModuleCat.{v} R) :
(biprodIsoProd M N).inv ≫ biprod.snd = ofHom (LinearMap.snd R M N) :=
IsLimit.conePointUniqueUpToIso_inv_comp _ _ (Discrete.mk WalkingPair.right)
