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] [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

@[reducible]

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 ∈ linear_map.range (finsupp.lsingle m)

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 = linear_map.range (finsupp.lsingle m)

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

finsupp.single m r ∈ add_monoid_algebra.grade_by R f (f m)

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.decompose_aux {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] direct_sum ι (λ (i : ι), ↥(add_monoid_algebra.grade_by R ⇑f i))

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

Equations

add_monoid_algebra.decompose_aux f = ⇑(add_monoid_algebra.lift R M (direct_sum ι (λ (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

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 ι] [comm_semiring R] (f : M →+ ι) (m : M) (r : R) :

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

source

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 ι] [comm_semiring R] (f : M →+ ι) {i : ι} (x : ↥(add_monoid_algebra.grade_by R ⇑f i)) :

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

source

@[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 ι] [comm_semiring R] (f : M →+ ι) :

graded_algebra (add_monoid_algebra.grade_by R ⇑f)

Equations

add_monoid_algebra.grade_by.graded_algebra f = graded_algebra.of_alg_hom (add_monoid_algebra.grade_by R ⇑f) (add_monoid_algebra.decompose_aux f) _ _

source

@[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 ι] [comm_semiring R] (f : M →+ ι) :

direct_sum.decomposition (add_monoid_algebra.grade_by R ⇑f)

Equations

add_monoid_algebra.grade_by.decomposition f = graded_ring.to_decomposition

source

@[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 ι] [comm_semiring R] (f : M →+ ι) :

⇑(add_monoid_algebra.decompose_aux f) = ⇑(direct_sum.decompose (add_monoid_algebra.grade_by R ⇑f))

source

@[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 ι] [comm_semiring R] (f : M →+ ι) (m : M) (r : R) :

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

source

@[protected, instance]

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

graded_algebra (add_monoid_algebra.grade R)

Equations

add_monoid_algebra.grade.graded_algebra = add_monoid_algebra.grade_by.graded_algebra (add_monoid_hom.id ι)

source

@[protected, instance]

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

direct_sum.decomposition (add_monoid_algebra.grade R)

Equations

add_monoid_algebra.grade.decomposition = graded_ring.to_decomposition

source

@[simp]

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

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

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.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.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` #