The trivial grading of a module

Every module has an integer grading concentrated in degree zero: the whole module in degree 0 and the zero submodule in every other degree. This file packages that family of submodules, records its membership API, and proves that it is an internal direct-sum decomposition, computing its projections. Scalar multiplication by a trivially graded base ring preserves every homogeneous piece of any family closed under scalar multiplication. For an algebra, TauCeti.RingTheory.GradedAlgebra.Trivial makes it a GradedAlgebra.

Main definitions

• TauCeti.trivialGrading: the integer grading with the whole module in degree zero.
• TauCeti.toTrivialGradingZero: the module viewed as the degree-zero piece of that grading.

Main results

• TauCeti.mem_trivialGrading_iff: an element has degree p exactly when p = 0 or it is zero.
• TauCeti.instDecompositionTrivialGrading: the trivial grading is an internal grading.
• TauCeti.instGradedSMulTrivialGrading: the trivially graded base ring acts compatibly with any family of scalar-stable sets containing zero.
• TauCeti.proj_trivialGrading: its degree projection is the identity in degree zero and zero in every other degree.

def TauCeti.trivialGrading (R : Type u_1) (A : Type u_2) [Semiring R] [AddCommMonoid A] [Module R A] (p : ℤ) : Submodule R A

The trivial integer grading of an R-module: all elements have degree zero and every other homogeneous piece is zero.

@[simp]

theorem TauCeti.trivialGrading_zero (R : Type u_1) (A : Type u_2) [Semiring R] [AddCommMonoid A] [Module R A] : trivialGrading R A 0 = ⊤

The degree-zero piece of the trivial grading is the whole module.

theorem TauCeti.trivialGrading_eq_bot (R : Type u_1) (A : Type u_2) [Semiring R] [AddCommMonoid A] [Module R A] {p : ℤ} (hp : p ≠ 0) : trivialGrading R A p = ⊥

Every nonzero-degree piece of the trivial grading is zero.

@[simp]

theorem TauCeti.mem_trivialGrading_iff (R : Type u_1) (A : Type u_2) [Semiring R] [AddCommMonoid A] [Module R A] {p : ℤ} {a : A} : a ∈ trivialGrading R A p ↔ p = 0 ∨ a = 0

An element belongs to degree p of the trivial grading exactly when p = 0 or the element itself is zero.

def TauCeti.toTrivialGradingZero (R : Type u_1) (A : Type u_2) [Semiring R] [AddCommMonoid A] [Module R A] : A →+ ↥(trivialGrading R A 0)

Every element of the module, viewed as an element of the degree-zero piece of the trivial grading.

@[simp]

theorem TauCeti.coe_toTrivialGradingZero (R : Type u_1) (A : Type u_2) [Semiring R] [AddCommMonoid A] [Module R A] (a : A) : ↑((toTrivialGradingZero R A) a) = a

@[instance_reducible]

instance TauCeti.instDecompositionTrivialGrading (R : Type u_1) (A : Type u_2) [Semiring R] [AddCommMonoid A] [Module R A] : DirectSum.Decomposition (trivialGrading R A)

The trivial grading of a module is an internal grading: an element is its own degree-zero component, and all other components vanish.

@[simp]

theorem TauCeti.proj_trivialGrading (R : Type u_1) (A : Type u_2) [Semiring R] [AddCommMonoid A] [Module R A] (p : ℤ) (a : A) : ↑(((DirectSum.decompose (trivialGrading R A)) a) p) = if p = 0 then a else 0

The homogeneous projection for the trivial grading is the identity in degree zero and the zero map in every other degree.

instance TauCeti.instGradedSMulTrivialGrading (R : Type u_1) [Semiring R] {M : Type u_3} {σ : Type u_4} [Zero M] [SMulWithZero R M] [SetLike σ M] [ZeroMemClass σ M] [SMulMemClass σ R M] (ℳ : ℤ → σ) : SetLike.GradedSMul (trivialGrading R R) ℳ

Scalar multiplication by the trivially graded base ring preserves every piece of any family closed under scalar multiplication and containing zero.