Theorems · Theorem · ring theory

DirectSum.toModule_lof

∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] {N : Type u₁} [inst_4 : AddCommMonoid N]
  [inst_5 : Module R N] {φ : (i : ι) → M i →ₗ[R] N} (i : ι) (x : M i),
  (DirectSum.toModule R ι N φ) ((DirectSum.lof R ι M i) x) = (φ i) x

The map constructed using the universal property gives back the original maps when restricted to each component.

Defined in

Mathlib.Algebra.DirectSum.Module

Cited by

8 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleDecidableEqAddCommMonoidModule