Integer powers of the grading shift

The integer powers of the grading-shift autoequivalence agree, up to natural isomorphism, with the explicit internal shifts M{d}. This comparison lets graded Hom computations made using the pieces (M{d})ₚ = M_{p-d} enter graded Ext and Euler characteristics, which use powers of an autoequivalence. No finiteness or projectivity assumptions are required.

References

• Năstăsescu--Van Oystaeyen, Methods of Graded Rings, Section 2.3.

def TauCeti.GradedModuleCat.shiftFunctorZeroIso {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : shiftFunctor 0 ≅ CategoryTheory.Functor.id (GradedModuleCat 𝒜)

The internal shift by zero is naturally isomorphic to the identity functor.

Equations

• TauCeti.GradedModuleCat.shiftFunctorZeroIso 𝒜 = CategoryTheory.NatIso.ofComponents (fun (M : TauCeti.GradedModuleCat 𝒜) => TauCeti.GradedModuleCat.isoMk (LinearEquiv.refl A M.carrier) ⋯) ⋯

@[simp]

theorem TauCeti.GradedModuleCat.hom_shiftFunctorZeroIso_hom_app {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) (M : GradedModuleCat 𝒜) : ((shiftFunctorZeroIso 𝒜).hom.app M).hom = LinearMap.id

@[simp]

theorem TauCeti.GradedModuleCat.hom_shiftFunctorZeroIso_inv_app {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) (M : GradedModuleCat 𝒜) : ((shiftFunctorZeroIso 𝒜).inv.app M).hom = LinearMap.id

def TauCeti.GradedModuleCat.shiftFunctorAddIso {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) (a b : ℤ) : (shiftFunctor a).comp (shiftFunctor b) ≅ shiftFunctor (a + b)

Successive internal shifts add their amounts; the comparison preserves the underlying linear maps.

Equations

• TauCeti.GradedModuleCat.shiftFunctorAddIso 𝒜 a b = CategoryTheory.NatIso.ofComponents (fun (M : TauCeti.GradedModuleCat 𝒜) => TauCeti.GradedModuleCat.isoMk (LinearEquiv.refl A M.carrier) ⋯) ⋯

@[simp]

theorem TauCeti.GradedModuleCat.hom_shiftFunctorAddIso_hom_app {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) (a b : ℤ) (M : GradedModuleCat 𝒜) : ((shiftFunctorAddIso 𝒜 a b).hom.app M).hom = LinearMap.id

@[simp]

theorem TauCeti.GradedModuleCat.hom_shiftFunctorAddIso_inv_app {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) (a b : ℤ) (M : GradedModuleCat 𝒜) : ((shiftFunctorAddIso 𝒜 a b).inv.app M).hom = LinearMap.id

def TauCeti.GradedModuleCat.shiftPowIso {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) (d : ℤ) : (shift 𝒜 ^ d).functor ≅ shiftFunctor d

The d-th integer power of the grading-shift autoequivalence is the explicit internal shift by d. Its components compare the same graded module with two presentations of its shifted grading.

Equations

• TauCeti.GradedModuleCat.shiftPowIso 𝒜 (Int.ofNat n) = TauCeti.GradedModuleCat.shiftPowNatIso✝ 𝒜 n
• TauCeti.GradedModuleCat.shiftPowIso 𝒜 (Int.negSucc n) = TauCeti.GradedModuleCat.shiftInversePowNatIso✝ 𝒜 (n + 1)