# Internal grading of an AddMonoidAlgebra#

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

## Main results #

• AddMonoidAlgebra.gradeBy R f i: the ith grade of an R[M] given by the degree function f.
• AddMonoidAlgebra.grade R i: the ith grade of an R[M] when the degree function is the identity.
• AddMonoidAlgebra.gradeBy.gradedAlgebra: AddMonoidAlgebra is an algebra graded by AddMonoidAlgebra.gradeBy.
• AddMonoidAlgebra.grade.gradedAlgebra: AddMonoidAlgebra is an algebra graded by AddMonoidAlgebra.grade.
• AddMonoidAlgebra.gradeBy.isInternal: propositionally, the statement that AddMonoidAlgebra.gradeBy defines an internal graded structure.
• AddMonoidAlgebra.grade.isInternal: propositionally, the statement that AddMonoidAlgebra.grade defines an internal graded structure when the degree function is the identity.
@[inline, reducible]
abbrev AddMonoidAlgebra.gradeBy {M : Type u_1} {ι : Type u_2} (R : Type u_3) [] (f : Mι) (i : ι) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline, reducible]
abbrev AddMonoidAlgebra.grade {M : Type u_1} (R : Type u_3) [] (m : M) :

The submodule corresponding to each grade.

Equations
Instances For
theorem AddMonoidAlgebra.gradeBy_id {M : Type u_1} (R : Type u_3) [] :
theorem AddMonoidAlgebra.mem_gradeBy_iff {M : Type u_1} {ι : Type u_2} (R : Type u_3) [] (f : Mι) (i : ι) (a : ) :
a a.support f ⁻¹' {i}
theorem AddMonoidAlgebra.mem_grade_iff {M : Type u_1} (R : Type u_3) [] (m : M) (a : ) :
a.support {m}
theorem AddMonoidAlgebra.mem_grade_iff' {M : Type u_1} (R : Type u_3) [] (m : M) (a : ) :
theorem AddMonoidAlgebra.grade_eq_lsingle_range {M : Type u_1} (R : Type u_3) [] (m : M) :
theorem AddMonoidAlgebra.single_mem_gradeBy {M : Type u_1} {ι : Type u_2} {R : Type u_4} [] (f : Mι) (m : M) (r : R) :
theorem AddMonoidAlgebra.single_mem_grade {M : Type u_1} {R : Type u_4} [] (i : M) (r : R) :
instance AddMonoidAlgebra.gradeBy.gradedMonoid {M : Type u_1} {ι : Type u_2} {R : Type u_3} [] [] [] (f : M →+ ι) :
Equations
• (_ : ) = (_ : )
Equations
• = (_ : )
def AddMonoidAlgebra.decomposeAux {M : Type u_1} {ι : Type u_2} {R : Type u_3} [] [] [] [] (f : M →+ ι) :
→ₐ[R] DirectSum ι fun (i : ι) => (AddMonoidAlgebra.gradeBy R (f) i)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddMonoidAlgebra.decomposeAux_single {M : Type u_1} {ι : Type u_2} {R : Type u_3} [] [] [] [] (f : M →+ ι) (m : M) (r : R) :
= (DirectSum.of (fun (i : ι) => (AddMonoidAlgebra.gradeBy R (f) i)) (f m)) { val := , property := (_ : AddMonoidAlgebra.gradeBy R (f) (f m)) }
theorem AddMonoidAlgebra.decomposeAux_coe {M : Type u_1} {ι : Type u_2} {R : Type u_3} [] [] [] [] (f : M →+ ι) {i : ι} (x : (AddMonoidAlgebra.gradeBy R (f) i)) :
= (DirectSum.of (fun (i : ι) => (AddMonoidAlgebra.gradeBy R (f) i)) i) x
instance AddMonoidAlgebra.gradeBy.gradedAlgebra {M : Type u_1} {ι : Type u_2} {R : Type u_3} [] [] [] [] (f : M →+ ι) :
Equations
• One or more equations did not get rendered due to their size.
instance AddMonoidAlgebra.gradeBy.decomposition {M : Type u_1} {ι : Type u_2} {R : Type u_3} [] [] [] [] (f : M →+ ι) :
Equations
• = inferInstance
@[simp]
theorem AddMonoidAlgebra.decomposeAux_eq_decompose {M : Type u_1} {ι : Type u_2} {R : Type u_3} [] [] [] [] (f : M →+ ι) :
@[simp]
theorem AddMonoidAlgebra.GradesBy.decompose_single {M : Type u_1} {ι : Type u_2} {R : Type u_3} [] [] [] [] (f : M →+ ι) (m : M) (r : R) :
() = (DirectSum.of (fun (i : ι) => (AddMonoidAlgebra.gradeBy R (f) i)) (f m)) { val := , property := (_ : AddMonoidAlgebra.gradeBy R (f) (f m)) }
Equations
AddMonoidAlgebra.gradeBy describe an internally graded algebra.
AddMonoidAlgebra.grade describe an internally graded algebra.