English
For any m in M, the graded injection ι followed by the degree-1 projection yields the standard exterior product map ι_R: M → ∧^1_R M; i.e., the degree-1 component of ι(m) is ι_R(m).
Русский
Для каждого элемента m из M соответствующее включение в градацию ι(m) имеет в компоненте степени 1 элемент ι_R(m).
LaTeX
$$$\pi_1(\iota_R(m)) = ι_R(m) \quad\text{and}\quad \pi_i(\iota_R(m))=0 \text{ for } i\neq 1$$$
Lean4
theorem ι_apply (m : M) :
GradedAlgebra.ι R M m =
DirectSum.of (fun i : ℕ => ⋀[R]^i M) 1 ⟨ι R m, by simpa only [pow_one] using LinearMap.mem_range_self _ m⟩ :=
rfl