Basic results on graded algebras

For a ℤ-graded algebra concentrated in nonnegative degrees, the degree-zero component of a product is the product of the degree-zero components, as for gradings by a canonically ordered monoid (GradedRing.projZeroRingHom). Consequently an idempotent with no degree-zero component vanishes: its powers have no components below any given degree.

In any graded ring, multiplication by a homogeneous element a of degree i shifts every homogeneous component by i. If a is moreover left regular, then the components of b can be read off from those of a * b; in particular, if a * b is homogeneous of degree i + j, then b is homogeneous of degree j. For instance, dividing a homogeneous polynomial by a linear form that divides it produces a homogeneous polynomial of one degree less.

Main results

• TauCeti.GradedAlgebra.mul_le_grade_add: the product of two homogeneous components is contained in the component indexed by the sum of their degrees.
• TauCeti.GradedAlgebra.coe_decompose_mul_zero_of_nonneg: in nonnegative degrees, the degree-zero component is multiplicative.
• TauCeti.GradedAlgebra.eq_zero_of_isIdempotentElem_of_decompose_zero: in nonnegative degrees, an idempotent with zero degree-zero component is zero.
• TauCeti.GradedAlgebra.mem_of_mul_mem_add_of_isLeftRegular: if a ∈ 𝒜 i is left regular and a * b ∈ 𝒜 (i + j), then b ∈ 𝒜 j.
• TauCeti.GradedAlgebra.isScalarTower_gradeZero: the scalars act on a graded algebra through its degree-zero part.

theorem TauCeti.GradedAlgebra.mul_le_grade_add {R : Type u_1} {A : Type u_2} {ι : Type u_3} [Add ι] [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [SetLike.GradedMul 𝒜] (i j : ι) : 𝒜 i * 𝒜 j ≤ 𝒜 (i + j)

The product of two homogeneous components lies in the component of the sum of the degrees.

theorem TauCeti.GradedAlgebra.coe_decompose_mul_zero_of_nonneg {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) (x y : A) : ↑(((DirectSum.decompose 𝒜) (x * y)) 0) = ↑(((DirectSum.decompose 𝒜) x) 0) * ↑(((DirectSum.decompose 𝒜) y) 0)

The degree-zero component is multiplicative in nonnegative degrees. This is the ℤ-graded counterpart of GradedRing.projZeroRingHom, which needs a canonically ordered grading monoid.

theorem TauCeti.GradedAlgebra.eq_zero_of_isIdempotentElem_of_decompose_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) {f : A} (hf : IsIdempotentElem f) (h0 : ↑(((DirectSum.decompose 𝒜) f) 0) = 0) : f = 0

An idempotent with no degree-zero component vanishes in nonnegative degrees.

theorem TauCeti.GradedAlgebra.mem_of_mul_mem_add_of_isLeftRegular {A : Type u_1} {ι : Type u_2} {σ : Type u_3} [AddLeftCancelMonoid ι] [DecidableEq ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a b : A} {i j : ι} (ha : a ∈ 𝒜 i) (hreg : IsLeftRegular a) (hab : a * b ∈ 𝒜 (i + j)) : b ∈ 𝒜 j

Cancelling a homogeneous regular factor. If a is homogeneous of degree i and left regular, and a * b is homogeneous of degree i + j, then b is homogeneous of degree j.

instance TauCeti.GradedAlgebra.isScalarTower_gradeZero {R : Type u_1} {A : Type u_2} {ι : Type u_3} [AddMonoid ι] [CommSemiring R] [CommSemiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [SetLike.GradedMonoid 𝒜] : IsScalarTower R (↥(𝒜 0)) A

The scalars of an algebra with a graded monoid of submodules act on it through its degree-zero part. Only the multiplicative structure of the grading is used, not a decomposition.