mathlib3 documentation

algebra.monoid_algebra.grading

Internal grading of an add_monoid_algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

@[reducible]
def add_monoid_algebra.grade_by {M : Type u_1} {ι : Type u_2} (R : Type u_3) [decidable_eq M] [comm_semiring R] (f : M ι) (i : ι) :

The submodule corresponding to each grade given by the degree function f.

@[reducible]
def add_monoid_algebra.grade {M : Type u_1} (R : Type u_3) [decidable_eq M] [comm_semiring R] (m : M) :

The submodule corresponding to each grade.

theorem add_monoid_algebra.mem_grade_by_iff {M : Type u_1} {ι : Type u_2} (R : Type u_3) [decidable_eq M] [comm_semiring R] (f : M ι) (i : ι) (a : add_monoid_algebra R M) :
theorem add_monoid_algebra.single_mem_grade_by {M : Type u_1} {ι : Type u_2} [decidable_eq M] {R : Type u_3} [comm_semiring R] (f : M ι) (m : M) (r : R) :
@[protected, instance]
noncomputable def add_monoid_algebra.decompose_aux {M : Type u_1} {ι : Type u_2} {R : Type u_3} [decidable_eq M] [add_monoid M] [decidable_eq ι] [add_monoid ι] [comm_semiring R] (f : M →+ ι) :

Auxiliary definition; the canonical grade decomposition, used to provide direct_sum.decompose.

Equations
theorem add_monoid_algebra.decompose_aux_single {M : Type u_1} {ι : Type u_2} {R : Type u_3} [decidable_eq M] [add_monoid M] [decidable_eq ι] [add_monoid ι] [comm_semiring R] (f : M →+ ι) (m : M) (r : R) :

add_monoid_algebra.gradesby describe an internally graded algebra

add_monoid_algebra.grades describe an internally graded algebra