mathlib3documentation

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 #

• add_monoid_algebra.grade_by R f i: the ith grade of an add_monoid_algebra R M given by the degree function f.
• add_monoid_algebra.grade R i: the ith grade of an add_monoid_algebra R M when the degree function is the identity.
• add_monoid_algebra.grade_by.graded_algebra: add_monoid_algebra is an algebra graded by add_monoid_algebra.grade_by.
• add_monoid_algebra.grade.graded_algebra: add_monoid_algebra is an algebra graded by add_monoid_algebra.grade.
• add_monoid_algebra.grade_by.is_internal: propositionally, the statement that add_monoid_algebra.grade_by defines an internal graded structure.
• add_monoid_algebra.grade.is_internal: propositionally, the statement that add_monoid_algebra.grade defines an internal graded structure when the degree function is the identity.
@[reducible]
def add_monoid_algebra.grade_by {M : Type u_1} {ι : Type u_2} (R : Type u_3) [decidable_eq M] (f : M ι) (i : ι) :
M)

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] (m : M) :
M)

The submodule corresponding to each grade.

theorem add_monoid_algebra.grade_by_id {M : Type u_1} (R : Type u_3) [decidable_eq M]  :
theorem add_monoid_algebra.mem_grade_by_iff {M : Type u_1} {ι : Type u_2} (R : Type u_3) [decidable_eq M] (f : M ι) (i : ι) (a : M) :
theorem add_monoid_algebra.mem_grade_iff {M : Type u_1} (R : Type u_3) [decidable_eq M] (m : M) (a : M) :
a.support {m}
theorem add_monoid_algebra.mem_grade_iff' {M : Type u_1} (R : Type u_3) [decidable_eq M] (m : M) (a : M) :
theorem add_monoid_algebra.grade_eq_lsingle_range {M : Type u_1} (R : Type u_3) [decidable_eq M] (m : M) :
theorem add_monoid_algebra.single_mem_grade_by {M : Type u_1} {ι : Type u_2} [decidable_eq M] {R : Type u_3} (f : M ι) (m : M) (r : R) :
(f m)
theorem add_monoid_algebra.single_mem_grade {M : Type u_1} [decidable_eq M] {R : Type u_2} (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 ι] (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 ι] (f : M →+ ι) :
→ₐ[R] (λ (i : ι), i))

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 ι] (f : M →+ ι) (m : M) (r : R) :
= (direct_sum.of (λ (i : ι), i)) (f m)) , _⟩
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 ι] (f : M →+ ι) {i : ι} (x : i)) :
= (direct_sum.of (λ (i : ι), i)) i) x
@[protected, instance]
noncomputable def add_monoid_algebra.grade_by.graded_algebra {M : Type u_1} {ι : Type u_2} {R : Type u_3} [decidable_eq M] [add_monoid M] [decidable_eq ι] [add_monoid ι] (f : M →+ ι) :
Equations
@[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 ι] (f : M →+ ι) :
Equations
@[simp]
theorem add_monoid_algebra.decompose_aux_eq_decompose {M : Type u_1} {ι : Type u_2} {R : Type u_3} [decidable_eq M] [add_monoid M] [decidable_eq ι] [add_monoid ι] (f : M →+ ι) :
@[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 ι] (f : M →+ ι) (m : M) (r : R) :
= (direct_sum.of (λ (i : ι), i)) (f m)) , _⟩
@[protected, instance]
noncomputable def add_monoid_algebra.grade.graded_algebra {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι]  :
Equations
@[protected, instance]
noncomputable def add_monoid_algebra.grade.decomposition {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι]  :
Equations
@[simp]
theorem add_monoid_algebra.grade.decompose_single {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] (i : ι) (r : R) :
= (direct_sum.of (λ (i : ι), i)) i) , _⟩
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 ι] (f : M →+ ι) :

add_monoid_algebra.gradesby describe an internally graded algebra

theorem add_monoid_algebra.grade.is_internal {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι]  :

add_monoid_algebra.grades describe an internally graded algebra