Extending an ℕ-indexed grading by zero to ℤ

A grading indexed by the natural numbers, such as the path-length grading of a quiver algebra, is extended to the integers by putting ⊥ in every negative degree. Integer indexing is the one in which internal grading shifts M{d}_p = M_{p-d} are stated, so this is how a nonnegatively graded module enters the signed-degree API.

Main definitions

• TauCeti.Graded.extendByZero: the extension by ⊥ of an ℕ-indexed family to ℤ.

Main results

• TauCeti.Graded.isInternal_extendByZero: the extension of an internal direct sum of submodules is still an internal direct sum.
• TauCeti.Graded.mul_mem_extendByZero: if multiplication adds degrees in the ℕ-indexed family, it adds signed degrees in its extension.

def TauCeti.Graded.extendByZero {α : Type u_1} [Bot α] (𝒜 : ℕ → α) (d : ℤ) : α

The extension by zero of an ℕ-indexed family of graded pieces to ℤ: its degree-d piece is 𝒜 d in nonnegative degrees and ⊥ in negative degrees.

Equations

• TauCeti.Graded.extendByZero 𝒜 d = if 0 ≤ d then 𝒜 d.toNat else ⊥

@[simp]

theorem TauCeti.Graded.extendByZero_natCast {α : Type u_1} [Bot α] (𝒜 : ℕ → α) (n : ℕ) : extendByZero 𝒜 ↑n = 𝒜 n

theorem TauCeti.Graded.extendByZero_of_neg {α : Type u_1} [Bot α] (𝒜 : ℕ → α) {d : ℤ} (hd : d < 0) : extendByZero 𝒜 d = ⊥

The extension by zero vanishes in negative degrees.

theorem TauCeti.Graded.isInternal_extendByZero {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {𝒜 : ℕ → Submodule R M} (h : DirectSum.IsInternal 𝒜) : DirectSum.IsInternal (extendByZero 𝒜)

The extension by zero of an internal direct sum is an internal direct sum: its pieces in nonnegative degrees are those of 𝒜, and those in negative degrees vanish.

theorem TauCeti.Graded.mul_mem_extendByZero {R : Type u_2} {A : Type u_3} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] {𝒜 : ℕ → Submodule R A} (h𝒜 : ∀ {m n : ℕ} {x y : A}, x ∈ 𝒜 m → y ∈ 𝒜 n → x * y ∈ 𝒜 (m + n)) {m n : ℤ} {x y : A} (hx : x ∈ extendByZero 𝒜 m) (hy : y ∈ extendByZero 𝒜 n) : x * y ∈ extendByZero 𝒜 (m + n)

Multiplication adds signed degrees in the extension by zero of an ℕ-indexed family in which it adds degrees.