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: theith grade of anR[M]given by the degree functionf.AddMonoidAlgebra.grade R i: theith grade of anR[M]when the degree function is the identity.AddMonoidAlgebra.gradeBy.gradedAlgebra:AddMonoidAlgebrais an algebra graded byAddMonoidAlgebra.gradeBy.AddMonoidAlgebra.grade.gradedAlgebra:AddMonoidAlgebrais an algebra graded byAddMonoidAlgebra.grade.AddMonoidAlgebra.gradeBy.isInternal: propositionally, the statement thatAddMonoidAlgebra.gradeBydefines an internal graded structure.AddMonoidAlgebra.grade.isInternal: propositionally, the statement thatAddMonoidAlgebra.gradedefines 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)
[DecidableEq M]
[CommSemiring R]
(f : M → ι)
(i : ι)
:
Submodule R (AddMonoidAlgebra R M)
The submodule corresponding to each grade given by the degree function f.
Instances For
@[inline, reducible]
abbrev
AddMonoidAlgebra.grade
{M : Type u_1}
(R : Type u_3)
[DecidableEq M]
[CommSemiring R]
(m : M)
:
Submodule R (AddMonoidAlgebra R M)
The submodule corresponding to each grade.
Instances For
theorem
AddMonoidAlgebra.gradeBy_id
{M : Type u_1}
(R : Type u_3)
[DecidableEq M]
[CommSemiring R]
:
theorem
AddMonoidAlgebra.mem_gradeBy_iff
{M : Type u_1}
{ι : Type u_2}
(R : Type u_3)
[DecidableEq M]
[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)
[DecidableEq M]
[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)
[DecidableEq M]
[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)
[DecidableEq M]
[CommSemiring R]
(m : M)
:
theorem
AddMonoidAlgebra.single_mem_gradeBy
{M : Type u_1}
{ι : Type u_2}
[DecidableEq M]
{R : Type u_4}
[CommSemiring R]
(f : M → ι)
(m : M)
(r : R)
:
(fun₀ | m => r) ∈ AddMonoidAlgebra.gradeBy R f (f m)
theorem
AddMonoidAlgebra.single_mem_grade
{M : Type u_1}
[DecidableEq M]
{R : Type u_4}
[CommSemiring R]
(i : M)
(r : R)
:
(fun₀ | i => r) ∈ AddMonoidAlgebra.grade R i
instance
AddMonoidAlgebra.gradeBy.gradedMonoid
{M : Type u_1}
{ι : Type u_2}
{R : Type u_3}
[DecidableEq M]
[AddMonoid M]
[AddMonoid ι]
[CommSemiring R]
(f : M →+ ι)
:
instance
AddMonoidAlgebra.grade.gradedMonoid
{M : Type u_1}
{R : Type u_3}
[DecidableEq M]
[AddMonoid M]
[CommSemiring R]
:
def
AddMonoidAlgebra.decomposeAux
{M : Type u_1}
{ι : Type u_2}
{R : Type u_3}
[DecidableEq M]
[AddMonoid M]
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring R]
(f : M →+ ι)
:
AddMonoidAlgebra R M →ₐ[R] ⨁ (i : ι), { x // x ∈ AddMonoidAlgebra.gradeBy R (↑f) i }
Auxiliary definition; the canonical grade decomposition, used to provide
DirectSum.decompose.
Instances For
theorem
AddMonoidAlgebra.decomposeAux_single
{M : Type u_1}
{ι : Type u_2}
{R : Type u_3}
[DecidableEq M]
[AddMonoid M]
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring R]
(f : M →+ ι)
(m : M)
(r : R)
:
(↑(AddMonoidAlgebra.decomposeAux f) fun₀ | m => r) = ↑(DirectSum.of (fun i => { x // x ∈ AddMonoidAlgebra.gradeBy R (↑f) i }) (↑f m))
{ val := fun₀ | m => r, property := (_ : (fun₀ | m => r) ∈ AddMonoidAlgebra.gradeBy R (↑f) (↑f m)) }
theorem
AddMonoidAlgebra.decomposeAux_coe
{M : Type u_1}
{ι : Type u_2}
{R : Type u_3}
[DecidableEq M]
[AddMonoid M]
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring R]
(f : M →+ ι)
{i : ι}
(x : { x // x ∈ AddMonoidAlgebra.gradeBy R (↑f) i })
:
↑(AddMonoidAlgebra.decomposeAux f) ↑x = ↑(DirectSum.of (fun i => { x // x ∈ AddMonoidAlgebra.gradeBy R (↑f) i }) i) x
instance
AddMonoidAlgebra.gradeBy.gradedAlgebra
{M : Type u_1}
{ι : Type u_2}
{R : Type u_3}
[DecidableEq M]
[AddMonoid M]
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring R]
(f : M →+ ι)
:
instance
AddMonoidAlgebra.gradeBy.decomposition
{M : Type u_1}
{ι : Type u_2}
{R : Type u_3}
[DecidableEq M]
[AddMonoid M]
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring R]
(f : M →+ ι)
:
@[simp]
theorem
AddMonoidAlgebra.decomposeAux_eq_decompose
{M : Type u_1}
{ι : Type u_2}
{R : Type u_3}
[DecidableEq M]
[AddMonoid M]
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring R]
(f : M →+ ι)
:
@[simp]
theorem
AddMonoidAlgebra.GradesBy.decompose_single
{M : Type u_1}
{ι : Type u_2}
{R : Type u_3}
[DecidableEq M]
[AddMonoid M]
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring R]
(f : M →+ ι)
(m : M)
(r : R)
:
(↑(DirectSum.decompose (AddMonoidAlgebra.gradeBy R ↑f)) fun₀ | m => r) = ↑(DirectSum.of (fun i => { x // x ∈ AddMonoidAlgebra.gradeBy R (↑f) i }) (↑f m))
{ val := fun₀ | m => r, property := (_ : (fun₀ | m => r) ∈ AddMonoidAlgebra.gradeBy R (↑f) (↑f m)) }
instance
AddMonoidAlgebra.grade.gradedAlgebra
{ι : Type u_2}
{R : Type u_3}
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring R]
:
instance
AddMonoidAlgebra.grade.decomposition
{ι : Type u_2}
{R : Type u_3}
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring R]
:
@[simp]
theorem
AddMonoidAlgebra.grade.decompose_single
{ι : Type u_2}
{R : Type u_3}
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring R]
(i : ι)
(r : R)
:
(↑(DirectSum.decompose (AddMonoidAlgebra.grade R)) fun₀ | i => r) = ↑(DirectSum.of (fun i => { x // x ∈ AddMonoidAlgebra.grade R i }) i)
{ val := fun₀ | i => r, property := (_ : (fun₀ | i => r) ∈ AddMonoidAlgebra.grade R i) }
theorem
AddMonoidAlgebra.gradeBy.isInternal
{M : Type u_1}
{ι : Type u_2}
{R : Type u_3}
[DecidableEq M]
[AddMonoid M]
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring R]
(f : M →+ ι)
:
AddMonoidAlgebra.gradeBy describe an internally graded algebra.
theorem
AddMonoidAlgebra.grade.isInternal
{ι : Type u_2}
{R : Type u_3}
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring R]
:
AddMonoidAlgebra.grade describe an internally graded algebra.