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 #

@[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.mem_grade_iff {M : Type u_1} (R : Type u_3) [decidable_eq M] [comm_semiring R] (m : M) (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) :
theorem add_monoid_algebra.single_mem_grade {M : Type u_1} [decidable_eq M] {R : Type u_2} [comm_semiring R] (i : M) (r : R) :
@[protected, instance]
def add_monoid_algebra.grade_by.graded_monoid {M : Type u_1} {ι : Type u_2} {R : Type u_3} [decidable_eq M] [add_monoid M] [add_monoid ι] [comm_semiring R] (f : M →+ ι) :
@[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) :
theorem add_monoid_algebra.decompose_aux_coe {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 →+ ι) {i : ι} (x : (add_monoid_algebra.grade_by R f i)) :
@[protected, instance]
noncomputable def add_monoid_algebra.grade_by.decomposition {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 →+ ι) :
Equations
@[simp]
theorem add_monoid_algebra.grades_by.decompose_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) :
@[simp]
theorem add_monoid_algebra.grade.decompose_single {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] (i : ι) (r : R) :
theorem add_monoid_algebra.grade_by.is_internal {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 →+ ι) :

add_monoid_algebra.gradesby describe an internally graded algebra

add_monoid_algebra.grades describe an internally graded algebra