toModule_lof — Mathlib

English

On each component, applying toModule to the inclusion map recovers the original component map: toModule R ι N φ (lof i x) = φ_i x.

Русский

На каждом компоненте применение toModule к включению восстанавливает исходную компоненту: toModule R ι N φ (lof i x) = φ_i x.

LaTeX

$$$toModule\\; R\\; ι\\; N\\; φ\\; (\\mathrm{lof}\\; R\\; ι\\; M\\; i\\; x) = φ_i\\, x.$$$

Lean4

/-- The map constructed using the universal property gives back the original maps when
restricted to each component. -/
@[simp]
theorem toModule_lof (i) (x : M i) : toModule R ι N φ (lof R ι M i x) = φ i x :=
  toAddMonoid_of (fun i ↦ (φ i).toAddMonoidHom) i x

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