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.coeff.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] : gradeBy R id = 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 ∈ gradeBy R f i ↔ ↑a.coeff.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 ∈ grade R m ↔ a.coeff.support ⊆ {m}

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

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

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

theorem AddMonoidAlgebra.single_mem_grade {M : Type u_1} {R : Type u_4} [CommSemiring R] (i : M) (r : R) : single i r ∈ 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 (gradeBy R ⇑f)

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

noncomputable 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 : ι) => ↥(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) : (decomposeAux f) (single m r) = (DirectSum.of (fun (i : ι) => ↥(gradeBy R (⇑f) i)) (f m)) ⟨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 : ↥(gradeBy R (⇑f) i)) : (decomposeAux f) ↑x = (DirectSum.of (fun (i : ι) => ↥(gradeBy R (⇑f) i)) i) x

@[instance_reducible]

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

Equations

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

@[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 →+ ι) : ⇑(decomposeAux f) = ⇑(DirectSum.decompose (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 (gradeBy R ⇑f)) (single m r) = (DirectSum.of (fun (i : ι) => ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m r, ⋯⟩

@[instance_reducible]

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

Equations

• AddMonoidAlgebra.grade.gradedAlgebra = { toGradedMonoid := ⋯, decompose' := AddMonoidAlgebra.grade.gradedAlgebra._aux_2, left_inv := ⋯, right_inv := ⋯ }

theorem AddMonoidAlgebra.grade.decompose_single {ι : Type u_2} {R : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (i : ι) (r : R) : (DirectSum.decompose (grade R)) (single i r) = (DirectSum.of (fun (i : ι) => ↥(grade R i)) i) ⟨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 (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 (grade R)

AddMonoidAlgebra.grade describe an internally graded algebra.