English
The exterior algebra ExteriorAlgebra_R(M) is naturally graded by the powers ∧^i_R M, forming a graded algebra whose multiplication respects the total degree addition.
Русский
Внешняя алгебра ExteriorAlgebra_R(M) естественным образом градуирована степенями ∧^i_R M, образуя градуированную алгебру, где умножение суммирует степени.
LaTeX
$$$ExteriorAlgebra_R(M) \text{ is graded by } i \mapsto \bigwedge^i_R M, \quad (\bigwedge^i_R M) \cdot (\bigwedge^j_R M) \subseteq \bigwedge^{i+j}_R M$$$
Lean4
/-- The exterior algebra is graded by the powers of the submodule `(ExteriorAlgebra.ι R).range`. -/
instance gradedAlgebra : GradedAlgebra (fun i : ℕ ↦ ⋀[R]^i M) :=
GradedAlgebra.ofAlgHom _
(by apply GradedAlgebra.liftι R M)
-- the proof from here onward is identical to the `TensorAlgebra` case
(by
ext m
dsimp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply, AlgHom.id_apply,
GradedAlgebra.liftι]
rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk])
(by apply GradedAlgebra.liftι_eq R M)
