Bases and ranks of the graded pieces of a monoid algebra

A function f : M → ι grades the additive monoid algebra R[M] by the submodules AddMonoidAlgebra.gradeBy R f i of elements supported on the fibre f ⁻¹' {i}. This file shows that the basis elements single m 1 with f m = i form a basis of the piece of grade i, so that its rank is the number of elements of M of grade i.

For the semigroup algebra k[S] of an additive monoid S graded by a degree deg : S →+ ℕ, the Hilbert function of k[S] is n ↦ Module.finrank k (gradeBy k deg n), the rank of its homogeneous component of degree n. By AddMonoidAlgebra.finrank_gradeBy it is the function counting the elements of S of degree n. The count is taken with Nat.card, which is 0 for an infinite fibre, as is the rank of a free module of infinite rank.

Main declarations

• AddMonoidAlgebra.gradeBy_eq_supported: the piece of grade i consists of the elements supported on f ⁻¹' {i}.
• AddMonoidAlgebra.basisGradeBy: the basis of the piece of grade i given by the elements single m 1 with f m = i.
• AddMonoidAlgebra.finrank_gradeBy: the rank of the piece of grade i is the number of elements of M of grade i.
• TauCeti.homogeneousUnitDegrees_gradeBy: for the group algebra R[G] graded by an additive homomorphism f : G →+ ι, the homogeneous unit degrees are the range of f.

theorem AddMonoidAlgebra.gradeBy_eq_supported {M : Type u_1} {ι : Type u_2} (R : Type u_3) [CommSemiring R] (f : M → ι) (i : ι) : gradeBy R f i = supported R R (f ⁻¹' {i})

The piece of grade i of R[M] for the grading by f consists of the elements supported on the fibre f ⁻¹' {i}.

noncomputable def AddMonoidAlgebra.basisGradeBy {M : Type u_1} {ι : Type u_2} (R : Type u_3) [CommSemiring R] (f : M → ι) (i : ι) : Module.Basis (↑(f ⁻¹' {i})) R ↥(gradeBy R f i)

The piece of grade i of R[M] for the grading by f has a basis indexed by the fibre f ⁻¹' {i}, consisting of the elements single m 1 with f m = i.

@[simp]

theorem AddMonoidAlgebra.coe_basisGradeBy {M : Type u_1} {ι : Type u_2} (R : Type u_3) [CommSemiring R] (f : M → ι) (i : ι) (m : ↑(f ⁻¹' {i})) : ↑((basisGradeBy R f i) m) = single (↑m) 1

instance AddMonoidAlgebra.instFreeSubtypeMemSubmoduleGradeBy_tauCeti {M : Type u_1} {ι : Type u_2} (R : Type u_3) [CommSemiring R] (f : M → ι) (i : ι) : Module.Free R ↥(gradeBy R f i)

theorem AddMonoidAlgebra.finrank_gradeBy {M : Type u_1} {ι : Type u_2} (R : Type u_3) [CommSemiring R] [StrongRankCondition R] (f : M → ι) (i : ι) : Module.finrank R ↥(gradeBy R f i) = Nat.card ↑(f ⁻¹' {i})

The Hilbert function of a graded monoid algebra. The rank of the piece of grade i of R[M] for the grading by f is the number of elements of M of grade i.

@[simp]

theorem TauCeti.homogeneousUnitDegrees_gradeBy {ι : Type u_1} {G : Type u_2} [AddGroup ι] [AddGroup G] (R : Type u_3) [CommSemiring R] [Nontrivial R] (f : G →+ ι) : homogeneousUnitDegrees (AddMonoidAlgebra.gradeBy R ⇑f) = f.range

For the group algebra R[G] over a nontrivial commutative semiring, graded by an additive homomorphism f : G →+ ι (so that single g r has degree f g), the degrees of the homogeneous units are the range of f: each single g 1 is a homogeneous unit of degree f g, and a nonzero element of degree d has a monomial of degree d.