mathlib documentation

algebra.monoid_algebra.grading

Internal grading of an add_monoid_algebra #

In this file, we show that an add_monoid_algebra has an internal direct sum structure.

Main results #

noncomputable def add_monoid_algebra.grade {ι : Type u_1} (R : Type u_2) [comm_semiring R] (i : ι) :

The submodule corresponding to each grade.

@[protected, instance]
noncomputable def add_monoid_algebra.to_grades {ι : Type u_1} {R : Type u_2} [decidable_eq ι] [add_monoid ι] [comm_semiring R] :

The canonical grade decomposition.

Equations
@[simp]
theorem add_monoid_algebra.to_grades_single {ι : Type u_1} {R : Type u_2} [decidable_eq ι] [add_monoid ι] [comm_semiring R] (i : ι) (r : R) :
@[simp]
theorem add_monoid_algebra.to_grades_coe {ι : Type u_1} {R : Type u_2} [decidable_eq ι] [add_monoid ι] [comm_semiring R] {i : ι} (x : (add_monoid_algebra.grade R i)) :
noncomputable def add_monoid_algebra.of_grades {ι : Type u_1} {R : Type u_2} [decidable_eq ι] [add_monoid ι] [comm_semiring R] :

The canonical recombination of grades.

Equations
@[simp]
theorem add_monoid_algebra.of_grades_of {ι : Type u_1} {R : Type u_2} [decidable_eq ι] [add_monoid ι] [comm_semiring R] (i : ι) (x : (add_monoid_algebra.grade R i)) :
noncomputable def add_monoid_algebra.equiv_grades {ι : Type u_1} {R : Type u_2} [decidable_eq ι] [add_monoid ι] [comm_semiring R] :

An add_monoid_algebra R ι is equivalent as an algebra to the direct sum of its grades.

Equations

add_monoid_algebra.grades describe an internally graded algebra