English
For m ∈ M, the graded embedding ι_R M m equals the corresponding degree-1 component in DirectSum via ι_R.
Русский
Для элемента m ∈ M градуированное вложение ι_R M m равняется соответствующему компоненту степени 1 в DirectSum через ι_R.
LaTeX
$$$ GradedAlgebra.ι R M m = DirectSum.of (fun i => ⨂[R]^i M) 1 ⟨TensorAlgebra.ι R m, _⟩ $$$
Lean4
theorem ι_apply (m : M) :
GradedAlgebra.ι R M m =
DirectSum.of (fun (i : ℕ) => ↥(LinearMap.range (TensorAlgebra.ι R : M →ₗ[_] _) ^ i)) 1
⟨TensorAlgebra.ι R m, by simpa only [pow_one] using LinearMap.mem_range_self _ m⟩ :=
rfl