unique — Mathlib

English

If ι is finite, there is an R-linear equivalence between the direct sum ⨁ i, M_i and the function type ∀ i, M_i.

Русский

При конечности индексов ι существует линейное эквивалентное отображение между прямой суммой ⨁ i, M_i и функциональным типом ∀ i, M_i.

LaTeX

$$$ (\\bigoplus_{i} M_i) \\simeq_{R} \\forall i, M_i \\quad\\text{provided } [Fintype\\; ι].$$$

Lean4

/-- Every linear map from a direct sum agrees with the one obtained by applying
the universal property to each of its components. -/
theorem unique (f : ⨁ i, M i) : ψ f = toModule R ι N (fun i ↦ ψ.comp <| lof R ι M i) f :=
  toAddMonoid.unique ψ.toAddMonoidHom f

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