directSum_injective — Mathlib

English

The map that sends a family of additive characters to their direct-sum character on the direct sum is injective.

Русский

Отображение, устанавливающее из семейства добавочно-определённых отображений характеристику на прямой сумме, инъективно.

LaTeX

$$$\\text{Injective}\\;\\big(\\,\\mathrm{directSum} : (\\forall i, AddChar(G_i,R)) \\to AddChar(\\bigoplus_i G_i,R)\\big)$$$

Lean4

theorem directSum_injective : Injective (directSum : (∀ i, AddChar (G i) R) → AddChar (⨁ i, G i) R) :=
  by
  refine toAddMonoidHomEquiv.symm.injective.comp <| DirectSum.toAddMonoid_injective.comp ?_
  rintro ψ χ h
  simpa [funext_iff] using h

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