instGradedMonoidNatSubmoduleExteriorPower

English

The family i ↦ ∧^i_R M carries a natural graded monoid structure coming from exterior multiplication, and this induces a graded algebra structure on the direct sum ⊕i ∧^i_R M.

Русский

Семейство степеней i ↦ ∧^i_R M естественным образом образует градуированную моноиду из-за внешнего произведения; это задаёт градуированную алгебру на прямую сумму ⊕i ∧^i_R M.

LaTeX

$$$\bigoplus_{i\ge 0} \bigwedge^i_R M$ имеет градуированную умножение $\bigwedge^i_R M \times \bigwedge^j_R M \to \bigwedge^{i+j}_R M$ и, следовательно, естественную градуированную алгебру.$$

Lean4

instance : SetLike.GradedMonoid fun i : ℕ ↦ ⋀[R]^i M :=
  Submodule.nat_power_gradedMonoid (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M))

Похожие утверждения