English
Let R be a commutative ring and M an R-module. There exists a linear map ι from M into the graded exterior algebra ⊕i≥0 ∧^i_R M which lands the degree-1 part at ∧^1_R M via the usual injection; explicitly, ι(m) has only a nonzero component in degree 1 equal to the standard ι_R(m).
Русский
Пусть R – коммутативное кольцо и M – R-модуль. Существует линейное отображение ι: M → ⊕_{i≥0} ∧^i_R M, такое что единственный ненулевой компонент модуля ι(m) находится в степени 1 и равен обычному инъекту товара ι_R(m).
LaTeX
$$$\iota: M \to \bigoplus_{i\ge 0} \bigwedge^i_R M, \quad (\iota(m))_i = \begin{cases} \iota_R(m), & i=1 \\ 0, & i\neq 1 \end{cases}$$$
Lean4
/-- A version of `ExteriorAlgebra.ι` that maps directly into the graded structure. This is
primarily an auxiliary construction used to provide `ExteriorAlgebra.gradedAlgebra`. -/
protected def ι : M →ₗ[R] ⨁ i : ℕ, ⋀[R]^i M :=
DirectSum.lof R ℕ (fun i => ⋀[R]^i M) 1 ∘ₗ
(ι R).codRestrict _ fun m => by simpa only [pow_one] using LinearMap.mem_range_self _ m
