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.

@[reducible, inline]

abbrev AddMonoidAlgebra.gradeBy {M : Type u_1} {ι : Type u_2} (R : Type u_3) [CommSemiring R] (f : M → ι) (i : ι) : Submodule R (AddMonoidAlgebra R M)

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

Equations

• AddMonoidAlgebra.gradeBy R f i = { carrier := {a : AddMonoidAlgebra R M | ∀ m ∈ a.support, f m = i}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[reducible, inline]

abbrev AddMonoidAlgebra.grade {M : Type u_1} (R : Type u_3) [CommSemiring R] (m : M) : Submodule R (AddMonoidAlgebra R M)

The submodule corresponding to each grade.

Equations

• AddMonoidAlgebra.grade R m = AddMonoidAlgebra.gradeBy R id m

theorem AddMonoidAlgebra.gradeBy_id {M : Type u_1} (R : Type u_3) [CommSemiring R] : AddMonoidAlgebra.gradeBy R id = AddMonoidAlgebra.grade R

theorem AddMonoidAlgebra.mem_gradeBy_iff {M : Type u_1} {ι : Type u_2} (R : Type u_3) [CommSemiring R] (f : M → ι) (i : ι) (a : AddMonoidAlgebra R M) : a ∈ AddMonoidAlgebra.gradeBy R f i ↔ ↑a.support ⊆ f ⁻¹' {i}

theorem AddMonoidAlgebra.mem_grade_iff {M : Type u_1} (R : Type u_3) [CommSemiring R] (m : M) (a : AddMonoidAlgebra R M) : a ∈ AddMonoidAlgebra.grade R m ↔ a.support ⊆ {m}

theorem AddMonoidAlgebra.mem_grade_iff' {M : Type u_1} (R : Type u_3) [CommSemiring R] (m : M) (a : AddMonoidAlgebra R M) : a ∈ AddMonoidAlgebra.grade R m ↔ a ∈ LinearMap.range (Finsupp.lsingle m)

theorem AddMonoidAlgebra.grade_eq_lsingle_range {M : Type u_1} (R : Type u_3) [CommSemiring R] (m : M) : AddMonoidAlgebra.grade R m = LinearMap.range (Finsupp.lsingle m)

theorem AddMonoidAlgebra.single_mem_gradeBy {M : Type u_1} {ι : Type u_2} {R : Type u_4} [CommSemiring R] (f : M → ι) (m : M) (r : R) : Finsupp.single m r ∈ AddMonoidAlgebra.gradeBy R f (f m)

theorem AddMonoidAlgebra.single_mem_grade {M : Type u_1} {R : Type u_4} [CommSemiring R] (i : M) (r : R) : Finsupp.single i r ∈ AddMonoidAlgebra.grade R i

instance AddMonoidAlgebra.gradeBy.gradedMonoid {M : Type u_1} {ι : Type u_2} {R : Type u_3} [AddMonoid M] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) : SetLike.GradedMonoid (AddMonoidAlgebra.gradeBy R ⇑f)

instance AddMonoidAlgebra.grade.gradedMonoid {M : Type u_1} {R : Type u_3} [AddMonoid M] [CommSemiring R] : SetLike.GradedMonoid (AddMonoidAlgebra.grade R)

def AddMonoidAlgebra.decomposeAux {M : Type u_1} {ι : Type u_2} {R : Type u_3} [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) : AddMonoidAlgebra R 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.

theorem AddMonoidAlgebra.decomposeAux_single {M : Type u_1} {ι : Type u_2} {R : Type u_3} [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) (m : M) (r : R) : (AddMonoidAlgebra.decomposeAux f) (Finsupp.single m r) = (DirectSum.of (fun (i : ι) => ↥(AddMonoidAlgebra.gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m r, ⋯⟩

theorem AddMonoidAlgebra.decomposeAux_coe {M : Type u_1} {ι : Type u_2} {R : Type u_3} [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) {i : ι} (x : ↥(AddMonoidAlgebra.gradeBy R (⇑f) i)) : (AddMonoidAlgebra.decomposeAux f) ↑x = (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} [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) : GradedAlgebra (AddMonoidAlgebra.gradeBy R ⇑f)

Equations

• AddMonoidAlgebra.gradeBy.gradedAlgebra f = GradedAlgebra.ofAlgHom (AddMonoidAlgebra.gradeBy R ⇑f) (AddMonoidAlgebra.decomposeAux f) ⋯ ⋯

instance AddMonoidAlgebra.gradeBy.decomposition {M : Type u_1} {ι : Type u_2} {R : Type u_3} [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) : DirectSum.Decomposition (AddMonoidAlgebra.gradeBy R ⇑f)

Equations

• AddMonoidAlgebra.gradeBy.decomposition f = inferInstance

@[simp]

theorem AddMonoidAlgebra.decomposeAux_eq_decompose {M : Type u_1} {ι : Type u_2} {R : Type u_3} [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) : ⇑(AddMonoidAlgebra.decomposeAux f) = ⇑(DirectSum.decompose (AddMonoidAlgebra.gradeBy R ⇑f))

theorem AddMonoidAlgebra.GradesBy.decompose_single {M : Type u_1} {ι : Type u_2} {R : Type u_3} [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) (m : M) (r : R) : (DirectSum.decompose (AddMonoidAlgebra.gradeBy R ⇑f)) (Finsupp.single m r) = (DirectSum.of (fun (i : ι) => ↥(AddMonoidAlgebra.gradeBy R (⇑f) i)) (f m)) ⟨Finsupp.single m r, ⋯⟩

instance AddMonoidAlgebra.grade.gradedAlgebra {ι : Type u_2} {R : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] : GradedAlgebra (AddMonoidAlgebra.grade R)

Equations

• AddMonoidAlgebra.grade.gradedAlgebra = AddMonoidAlgebra.gradeBy.gradedAlgebra (AddMonoidHom.id ι)

instance AddMonoidAlgebra.grade.decomposition {ι : Type u_2} {R : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] : DirectSum.Decomposition (AddMonoidAlgebra.grade R)

Equations

• AddMonoidAlgebra.grade.decomposition = inferInstance

theorem AddMonoidAlgebra.grade.decompose_single {ι : Type u_2} {R : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (i : ι) (r : R) : (DirectSum.decompose (AddMonoidAlgebra.grade R)) (Finsupp.single i r) = (DirectSum.of (fun (i : ι) => ↥(AddMonoidAlgebra.grade R i)) i) ⟨Finsupp.single i r, ⋯⟩

theorem AddMonoidAlgebra.gradeBy.isInternal {M : Type u_1} {ι : Type u_2} {R : Type u_3} [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) : DirectSum.IsInternal (AddMonoidAlgebra.gradeBy R ⇑f)

AddMonoidAlgebra.gradeBy describe an internally graded algebra.

theorem AddMonoidAlgebra.grade.isInternal {ι : Type u_2} {R : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] : DirectSum.IsInternal (AddMonoidAlgebra.grade R)

AddMonoidAlgebra.grade describe an internally graded algebra.