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 #

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.equiv_grade_by: the equivalence between an add_monoid_algebra and the direct sum of its grades.
add_monoid_algebra.equiv_grade: the equivalence between an add_monoid_algebra and the direct sum of its grades when the degree function is the identity.
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.

noncomputable 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 : ι) :

submodule R (add_monoid_algebra R M)

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

source

noncomputable def add_monoid_algebra.grade {M : Type u_1} (R : Type u_3) [decidable_eq M] [comm_semiring R] (m : M) :

submodule R (add_monoid_algebra R M)

The submodule corresponding to each grade.

source

theorem add_monoid_algebra.grade_by_id {M : Type u_1} (R : Type u_3) [decidable_eq M] [comm_semiring R] :

add_monoid_algebra.grade_by R id = add_monoid_algebra.grade R

source

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) :

a ∈ add_monoid_algebra.grade_by R f i ↔ ↑(a.support) ⊆ f ⁻¹' {i}

source

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) :

a ∈ add_monoid_algebra.grade R m ↔ a.support ⊆ {m}

source

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) :

a ∈ add_monoid_algebra.grade R m ↔ a ∈ (finsupp.lsingle m).range

source

theorem add_monoid_algebra.grade_eq_lsingle_range {M : Type u_1} (R : Type u_3) [decidable_eq M] [comm_semiring R] (m : M) :

add_monoid_algebra.grade R m = (finsupp.lsingle m).range

source

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 → ι) (i : ι) (m : M) (h : f m = i) (r : R) :

finsupp.single m r ∈ add_monoid_algebra.grade_by R f i

source

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) :

finsupp.single i r ∈ add_monoid_algebra.grade R i

source

@[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 →+ ι) :

set_like.graded_monoid (add_monoid_algebra.grade_by R ⇑f)

source

@[protected, instance]

def add_monoid_algebra.grade.graded_monoid {M : Type u_1} {R : Type u_3} [decidable_eq M] [add_monoid M] [comm_semiring R] :

set_like.graded_monoid (add_monoid_algebra.grade R)

source

noncomputable def add_monoid_algebra.to_grades_by {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 R M →ₐ[R] ⨁ (i : ι), ↥(add_monoid_algebra.grade_by R ⇑f i)

The canonical grade decomposition.

Equations

add_monoid_algebra.to_grades_by f = ⇑(add_monoid_algebra.lift R M (⨁ (i : ι), (λ (i : ι), ↥(add_monoid_algebra.grade_by R ⇑f i)) i)) {to_fun := λ (m : multiplicative M), ⇑(direct_sum.of (λ (i : ι), ↥(add_monoid_algebra.grade_by R ⇑f i)) (⇑f (⇑multiplicative.to_add m))) ⟨finsupp.single (⇑multiplicative.to_add m) 1, _⟩, map_one' := _, map_mul' := _}

source

noncomputable def add_monoid_algebra.to_grades {M : Type u_1} {R : Type u_3} [decidable_eq M] [add_monoid M] [comm_semiring R] :

add_monoid_algebra R M →ₐ[R] ⨁ (i : M), ↥(add_monoid_algebra.grade R i)

The canonical grade decomposition.

Equations

add_monoid_algebra.to_grades = add_monoid_algebra.to_grades_by (add_monoid_hom.id M)

source

theorem add_monoid_algebra.to_grades_by_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 →+ ι) (i : ι) (m : M) (h : ⇑f m = i) (r : R) :

⇑(add_monoid_algebra.to_grades_by f) (finsupp.single m r) = ⇑(direct_sum.of (λ (i : ι), ↥(add_monoid_algebra.grade_by R ⇑f i)) i) ⟨finsupp.single m r, _⟩

source

@[simp]

theorem add_monoid_algebra.to_grades_by_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) :

⇑(add_monoid_algebra.to_grades_by f) (finsupp.single m r) = ⇑(direct_sum.of (λ (i : ι), ↥(add_monoid_algebra.grade_by R ⇑f i)) (⇑f m)) ⟨finsupp.single m r, _⟩

source

@[simp]

theorem add_monoid_algebra.to_grades_single {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] (i : ι) (r : R) :

⇑add_monoid_algebra.to_grades (finsupp.single i r) = ⇑(direct_sum.of (λ (i : ι), ↥(add_monoid_algebra.grade R i)) i) ⟨finsupp.single i r, _⟩

source

@[simp]

theorem add_monoid_algebra.to_grades_by_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)) :

⇑(add_monoid_algebra.to_grades_by f) ↑x = ⇑(direct_sum.of (λ (i : ι), ↥(add_monoid_algebra.grade_by R ⇑f i)) i) x

source

@[simp]

theorem add_monoid_algebra.to_grades_coe {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] {i : ι} (x : ↥(add_monoid_algebra.grade R i)) :

⇑add_monoid_algebra.to_grades ↑x = ⇑(direct_sum.of (λ (i : ι), ↥(add_monoid_algebra.grade R i)) i) x

source

noncomputable def add_monoid_algebra.of_grades_by {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 : ι), ↥(add_monoid_algebra.grade_by R ⇑f i)) →ₐ[R] add_monoid_algebra R M

The canonical recombination of grades.

Equations

add_monoid_algebra.of_grades_by f = direct_sum.submodule_coe_alg_hom (add_monoid_algebra.grade_by R ⇑f)

source

noncomputable def add_monoid_algebra.of_grades {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] :

(⨁ (i : ι), ↥(add_monoid_algebra.grade R i)) →ₐ[R] add_monoid_algebra R ι

The canonical recombination of grades.

Equations

add_monoid_algebra.of_grades = add_monoid_algebra.of_grades_by (add_monoid_hom.id ι)

source

@[simp]

theorem add_monoid_algebra.of_grades_by_of {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)) :

⇑(add_monoid_algebra.of_grades_by f) (⇑(direct_sum.of (λ (i : ι), ↥(add_monoid_algebra.grade_by R ⇑f i)) i) x) = ↑x

source

@[simp]

theorem add_monoid_algebra.of_grades_of {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] (i : ι) (x : ↥(add_monoid_algebra.grade R i)) :

⇑add_monoid_algebra.of_grades (⇑(direct_sum.of (λ (i : ι), ↥(add_monoid_algebra.grade R i)) i) x) = ↑x

source

@[simp]

theorem add_monoid_algebra.of_grades_by_comp_to_grades_by {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.of_grades_by f).comp (add_monoid_algebra.to_grades_by f) = alg_hom.id R (add_monoid_algebra R M)

source

@[simp]

theorem add_monoid_algebra.of_grades_comp_to_grades {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] :

add_monoid_algebra.of_grades.comp add_monoid_algebra.to_grades = alg_hom.id R (add_monoid_algebra R ι)

source

@[simp]

theorem add_monoid_algebra.of_grades_by_to_grades_by {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 →+ ι) (x : add_monoid_algebra R M) :

⇑(add_monoid_algebra.of_grades_by f) (⇑(add_monoid_algebra.to_grades_by f) x) = x

source

@[simp]

theorem add_monoid_algebra.of_grades_to_grades {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] (x : add_monoid_algebra R ι) :

⇑add_monoid_algebra.of_grades (⇑add_monoid_algebra.to_grades x) = x

source

@[simp]

theorem add_monoid_algebra.to_grades_by_comp_of_grades_by {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.to_grades_by f).comp (add_monoid_algebra.of_grades_by f) = alg_hom.id R (⨁ (i : ι), ↥(add_monoid_algebra.grade_by R ⇑f i))

source

@[simp]

theorem add_monoid_algebra.to_grades_comp_of_grades {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] :

add_monoid_algebra.to_grades.comp add_monoid_algebra.of_grades = alg_hom.id R (⨁ (i : ι), ↥(add_monoid_algebra.grade R i))

source

@[simp]

theorem add_monoid_algebra.to_grades_by_of_grades_by {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 →+ ι) (g : ⨁ (i : ι), ↥(add_monoid_algebra.grade_by R ⇑f i)) :

⇑(add_monoid_algebra.to_grades_by f) (⇑(add_monoid_algebra.of_grades_by f) g) = g

source

@[simp]

theorem add_monoid_algebra.to_grades_of_grades {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] (g : ⨁ (i : ι), ↥(add_monoid_algebra.grade R i)) :

⇑add_monoid_algebra.to_grades (⇑add_monoid_algebra.of_grades g) = g

source

@[simp]

theorem add_monoid_algebra.equiv_grades_by_apply {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 R M) :

⇑(add_monoid_algebra.equiv_grades_by f) ᾰ = ⇑(add_monoid_algebra.to_grades_by f) ᾰ

source

@[simp]

theorem add_monoid_algebra.equiv_grades_by_symm_apply {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 : ι), ↥(add_monoid_algebra.grade_by R ⇑f i)) :

⇑((add_monoid_algebra.equiv_grades_by f).symm) ᾰ = ⇑(add_monoid_algebra.of_grades_by f) ᾰ

source

noncomputable def add_monoid_algebra.equiv_grades_by {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 R M ≃ₐ[R] ⨁ (i : ι), ↥(add_monoid_algebra.grade_by R ⇑f i)

An add_monoid_algebra R M is equivalent as an algebra to the direct sum of its grades.

Equations

add_monoid_algebra.equiv_grades_by f = alg_equiv.of_alg_hom (add_monoid_algebra.to_grades_by f) (add_monoid_algebra.of_grades_by f) _ _

source

@[simp]

theorem add_monoid_algebra.equiv_grades_apply {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] (ᾰ : add_monoid_algebra R ι) :

⇑add_monoid_algebra.equiv_grades ᾰ = ⇑(add_monoid_algebra.to_grades_by (add_monoid_hom.id ι)) ᾰ

source

noncomputable def add_monoid_algebra.equiv_grades {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] :

add_monoid_algebra R ι ≃ₐ[R] ⨁ (i : ι), ↥(add_monoid_algebra.grade R i)

An add_monoid_algebra R ι is equivalent as an algebra to the direct sum of its grades.

Equations

add_monoid_algebra.equiv_grades = add_monoid_algebra.equiv_grades_by (add_monoid_hom.id ι)

source

@[simp]

theorem add_monoid_algebra.equiv_grades_symm_apply {ι : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring R] (ᾰ : ⨁ (i : ι), ↥(add_monoid_algebra.grade_by R ⇑(add_monoid_hom.id ι) i)) :

⇑(add_monoid_algebra.equiv_grades.symm) ᾰ = ⇑(add_monoid_algebra.of_grades_by (add_monoid_hom.id ι)) ᾰ

source

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 →+ ι) :

direct_sum.submodule_is_internal (add_monoid_algebra.grade_by R ⇑f)

add_monoid_algebra.gradesby describe an internally graded algebra

source

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

direct_sum.submodule_is_internal (add_monoid_algebra.grade R)

add_monoid_algebra.grades describe an internally graded algebra

Internal grading of an add_monoid_algebra #

Main results #

Internal grading of an `add_monoid_algebra` #