coe_toModule_eq_coe_toAddMonoid — Mathlib

English

Any linear map ψ from the direct sum to N is determined by its compositions with each inclusion lof i; i.e., ψ = toModule R ι N (λ i, ψ ∘ lof i).

Русский

Любое линейное отображение ψ из прямой суммы в N определяется по его композициям с включениями lof_i: ψ = toModule R ι N (λ i, ψ ∘ lof i).

LaTeX

$$$\\psi = toModule\\; R\\; ι\\; N\\; (\\lambda i, \\psi \\circ \\mathrm{lof}\\; i).$$$

Lean4

/-- Coproducts in the categories of modules and additive monoids commute with the forgetful functor
from modules to additive monoids. -/
theorem coe_toModule_eq_coe_toAddMonoid :
    (toModule R ι N φ : (⨁ i, M i) → N) = toAddMonoid fun i ↦ (φ i).toAddMonoidHom :=
  rfl

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