Shifting an internal grading

An internal grading may be regraded by a fixed shift c, so that the degree-p piece of the shifted grading is the degree-(p + c) piece of the original one. The underlying module is unchanged, and the shifted family is again an internal direct sum: reindexing the homogeneous pieces along an equivalence of degrees only permutes the summands of ⨁ p, G.piece p.

This is the suspension sA of the A∞ conventions of the DGAInfinity roadmap, seen on the internal presentation of a graded module. The suspension leaves the underlying module unchanged and reindexes its homogeneous pieces.

Main definitions

• TauCeti.InternalGrading.shift: the shift of an internal grading.

Main results

• TauCeti.LinearMap.isHomogeneous_shift_piece_iff: shifting both gradings preserves degrees.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 3.6.

def TauCeti.InternalGrading.shift {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (c : ℤ) : InternalGrading R M

The shift of an internal grading by c: its degree-p piece is the degree-(p + c) piece of the original grading. The underlying module is unchanged.

Equations

• G.shift c = { piece := fun (p : ℤ) => G.piece (p + c), isInternal := ⋯ }

@[simp]

theorem TauCeti.InternalGrading.shift_piece {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (c p : ℤ) : (G.shift c).piece p = G.piece (p + c)

@[simp]

theorem TauCeti.InternalGrading.shift_zero {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : G.shift 0 = G

@[simp]

theorem TauCeti.InternalGrading.shift_shift {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (c d : ℤ) : (G.shift c).shift d = G.shift (d + c)

Shifting twice shifts by the sum of the two amounts.

theorem TauCeti.InternalGrading.koszulTwist_shift {R : Type u} {M : Type v} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (c q : ℤ) : (G.shift c).koszulTwist q = ↑↑(q * c).negOnePow • G.koszulTwist q

The Koszul twist of parameter q for a grading shifted by c differs from the unshifted twist by the constant sign (-1)^(q * c): a homogeneous element of degree p has degree p - c after the shift.

theorem TauCeti.InternalGrading.koszulTwist_one_shift_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) : (G.shift 1).koszulTwist 1 = -G.koszulTwist 1

The degree-one Koszul twist of the suspended grading is the negative of the unsuspended one.

theorem TauCeti.LinearMap.isHomogeneous_shift_piece_iff {R : Type u} {M : Type u_1} {N : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {H : InternalGrading R N} {f : M →ₗ[R] N} {c q : ℤ} : IsHomogeneous f (G.shift c).piece (H.shift c).piece q ↔ IsHomogeneous f G.piece H.piece q

Shifting the source and the target internal grading by the same amount leaves the degree of a homogeneous linear map unchanged.