coeLinearMap — Mathlib

English

The canonical linear map from the direct sum ⨁ i, A_i to M, where A_i are submodules of M, is given by the inclusion of each component and summing over i.

Русский

Каноническое линейное отображение от прямой суммы ⨁_i A_i к M, где A_i подмодули M, задаётся инклузией каждой компоненты и суммой по i.

LaTeX

$$$\mathrm{coeLinearMap} A : (\bigoplus_i A_i) \to_{} M,\quad x \mapsto \sum_i x_i.$$$

Lean4

/-- The canonical linear map from `⨁ i, A i` to `M` where `A` is a collection of `Submodule R M`
indexed by `ι`. This is `DirectSum.coeAddMonoidHom` as a `LinearMap`. -/
def coeLinearMap : (⨁ i, A i) →ₗ[R] M :=
  toModule R ι M fun i ↦ (A i).subtype

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