English
A graded embedding ι into TensorAlgebra lands M into the degree-1 component, and the full ι is given by summing over degrees with the appropriate embedding.
Русский
Градуированное включение ι в тензорную алгебру помещает M в компоненту степени 1; полное ι задаётся через суммирование по степеням с нужным вложением.
LaTeX
$$$ ι_R M m = DirectSum.of (fun i => ⨂[R]^i M) 1 \langle ι_R m, \text{...} \rangle $$$
Lean4
/-- A version of `TensorAlgebra.ι` that maps directly into the graded structure. This is
primarily an auxiliary construction used to provide `TensorAlgebra.gradedAlgebra`. -/
nonrec def ι : M →ₗ[R] ⨁ i : ℕ, ↥(LinearMap.range (ι R : M →ₗ[_] _) ^ i) :=
DirectSum.lof R ℕ (fun i => ↥(LinearMap.range (ι R : M →ₗ[_] _) ^ i)) 1 ∘ₗ
(ι R).codRestrict _ fun m => by simpa only [pow_one] using LinearMap.mem_range_self _ m
