The category of graded modules

Let 𝒜 : ℤ → Submodule k A be a family of k-submodules of a k-algebra A, typically the pieces of a GradedAlgebra. A graded 𝒜-module is an A-module M with an internal ℤ-grading M = ⨁ₚ Mₚ by k-submodules, in the sense of TauCeti.InternalGrading, on which 𝒜 acts compatibly: 𝒜ᵢ • Mₚ ⊆ M_{i+p}. A morphism of graded modules is an A-linear map of degree zero, sending Mₚ into Nₚ for every p.

This file makes graded 𝒜-modules into a k-linear category TauCeti.GradedModuleCat 𝒜, with a faithful additive forgetful functor to ModuleCat A, and constructs its grading shift TauCeti.GradedModuleCat.shift 𝒜, the k-linear autoequivalence M ↦ M{1} of the category with (M{1})ₚ = M_{p-1}. This is the convention under which the class of M{1} in a graded Grothendieck group is q times the class of M, and it agrees with the shift of TauCeti.GradedVectorSpace. Graded Grothendieck groups, graded Ext and graded Cartan maps of graded algebras are formed in this category with this shift.

Main definitions

• TauCeti.GradedModuleCat 𝒜: the category of graded 𝒜-modules.
• TauCeti.GradedModuleCat.ofHom: the morphism given by an A-linear map of degree zero.
• TauCeti.GradedModuleCat.isoMk: the isomorphism given by an A-linear equivalence which preserves and reflects degrees.
• TauCeti.GradedModuleCat.toModuleCat: the forgetful functor to ModuleCat A.
• TauCeti.GradedModuleCat.shiftFunctor: the shift M ↦ M{n}, with (M{n})ₚ = M_{p-n}.
• TauCeti.GradedModuleCat.shift: the grading shift M ↦ M{1}, as an autoequivalence.

Main results

• TauCeti.GradedModuleCat.mem_shift_functor_obj_piece_iff and TauCeti.GradedModuleCat.mem_shift_inverse_obj_piece_iff: (M{1})ₚ = M_{p-1} and (M{-1})ₚ = M_{p+1}.

structure TauCeti.GradedModuleCat {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : Type (max (max uA uk) (v + 1))

The category of graded 𝒜-modules: A-modules with an internal ℤ-grading by k-submodules on which 𝒜ᵢ raises degrees by i.

• carrier : Type v

  The underlying type of the module.

• isAddCommGroup : AddCommGroup self.carrier
• isModule : Module A self.carrier
• isModuleBase : Module k self.carrier
• isScalarTower : IsScalarTower k A self.carrier
• grading : InternalGrading k self.carrier

  The internal grading of the module.

• gradedSMul : SetLike.GradedSMul 𝒜 self.grading.piece

@[instance_reducible]

instance TauCeti.GradedModuleCat.instCoeSortType {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : CoeSort (GradedModuleCat 𝒜) (Type v)

Equations

• TauCeti.GradedModuleCat.instCoeSortType = { coe := TauCeti.GradedModuleCat.carrier }

@[reducible, inline]

noncomputable abbrev TauCeti.GradedModuleCat.regular {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] [SetLike.GradedMul 𝒜] : GradedModuleCat 𝒜

The regular graded module of a graded algebra, with its given homogeneous pieces.

Equations

• One or more equations did not get rendered due to their size.

structure TauCeti.GradedModuleCat.Hom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M N : GradedModuleCat 𝒜) : Type v

A morphism of graded 𝒜-modules: an A-linear map of degree zero.

• hom : M.carrier →ₗ[A] N.carrier

  The underlying A-linear map.

• isHomogeneous : LinearMap.IsHomogeneous self.hom M.grading.piece N.grading.piece 0

  The underlying map sends Mₚ into Nₚ.

@[instance_reducible]

instance TauCeti.GradedModuleCat.instCategory {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : CategoryTheory.Category.{v, max (max (v + 1) uA) uk} (GradedModuleCat 𝒜)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev TauCeti.GradedModuleCat.ofHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M.carrier →ₗ[A] N.carrier) (hf : LinearMap.IsHomogeneous f M.grading.piece N.grading.piece 0) : M ⟶ N

The morphism of graded modules given by an A-linear map of degree zero.

Equations

• TauCeti.GradedModuleCat.ofHom f hf = { hom := f, isHomogeneous := hf }

@[simp]

theorem TauCeti.GradedModuleCat.hom_ofHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M.carrier →ₗ[A] N.carrier) (hf : LinearMap.IsHomogeneous f M.grading.piece N.grading.piece 0) : (ofHom f hf).hom = f

@[simp]

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

@[simp]

theorem TauCeti.GradedModuleCat.hom_comp {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N P : GradedModuleCat 𝒜} (f : M ⟶ N) (g : N ⟶ P) : (CategoryTheory.CategoryStruct.comp f g).hom = g.hom ∘ₗ f.hom

theorem TauCeti.GradedModuleCat.hom_ext {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} {f g : M ⟶ N} (h : f.hom = g.hom) : f = g

Two morphisms of graded modules are equal when their underlying linear maps are.

theorem TauCeti.GradedModuleCat.hom_ext_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} {f g : M ⟶ N} : f = g ↔ f.hom = g.hom

theorem TauCeti.GradedModuleCat.hom_injective {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} : Function.Injective fun (f : M ⟶ N) => f.hom

theorem TauCeti.GradedModuleCat.map_mem {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) {p : ℤ} {x : M.carrier} (hx : x ∈ M.grading.piece p) : f.hom x ∈ N.grading.piece p

A morphism of graded modules sends elements of degree p to elements of degree p.

@[instance_reducible]

instance TauCeti.GradedModuleCat.instZeroHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} : Zero (M ⟶ N)

Equations

• TauCeti.GradedModuleCat.instZeroHom = { zero := { hom := 0, isHomogeneous := ⋯ } }

@[instance_reducible]

instance TauCeti.GradedModuleCat.instAddHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} : Add (M ⟶ N)

Equations

• TauCeti.GradedModuleCat.instAddHom = { add := fun (f g : M ⟶ N) => { hom := f.hom + g.hom, isHomogeneous := ⋯ } }

@[instance_reducible]

instance TauCeti.GradedModuleCat.instNegHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} : Neg (M ⟶ N)

Equations

• TauCeti.GradedModuleCat.instNegHom = { neg := fun (f : M ⟶ N) => { hom := -f.hom, isHomogeneous := ⋯ } }

@[instance_reducible]

instance TauCeti.GradedModuleCat.instSubHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} : Sub (M ⟶ N)

Equations

• TauCeti.GradedModuleCat.instSubHom = { sub := fun (f g : M ⟶ N) => { hom := f.hom - g.hom, isHomogeneous := ⋯ } }

@[instance_reducible]

instance TauCeti.GradedModuleCat.instSMulNatHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} : SMul ℕ (M ⟶ N)

Equations

• TauCeti.GradedModuleCat.instSMulNatHom = { smul := fun (n : ℕ) (f : M ⟶ N) => { hom := n • f.hom, isHomogeneous := ⋯ } }

@[instance_reducible]

instance TauCeti.GradedModuleCat.instSMulIntHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} : SMul ℤ (M ⟶ N)

Equations

• TauCeti.GradedModuleCat.instSMulIntHom = { smul := fun (n : ℤ) (f : M ⟶ N) => { hom := n • f.hom, isHomogeneous := ⋯ } }

@[instance_reducible]

instance TauCeti.GradedModuleCat.instSMulHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} : SMul k (M ⟶ N)

Equations

• TauCeti.GradedModuleCat.instSMulHom = { smul := fun (c : k) (f : M ⟶ N) => { hom := c • f.hom, isHomogeneous := ⋯ } }

@[simp]

theorem TauCeti.GradedModuleCat.hom_zero {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} : Hom.hom 0 = 0

@[simp]

theorem TauCeti.GradedModuleCat.hom_add {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f g : M ⟶ N) : (f + g).hom = f.hom + g.hom

@[simp]

theorem TauCeti.GradedModuleCat.hom_neg {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : (-f).hom = -f.hom

@[simp]

theorem TauCeti.GradedModuleCat.hom_sub {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f g : M ⟶ N) : (f - g).hom = f.hom - g.hom

@[simp]

theorem TauCeti.GradedModuleCat.hom_nsmul {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (n : ℕ) (f : M ⟶ N) : (n • f).hom = n • f.hom

@[simp]

theorem TauCeti.GradedModuleCat.hom_zsmul {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (n : ℤ) (f : M ⟶ N) : (n • f).hom = n • f.hom

@[simp]

theorem TauCeti.GradedModuleCat.hom_smul {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (c : k) (f : M ⟶ N) : (c • f).hom = c • f.hom

@[instance_reducible]

instance TauCeti.GradedModuleCat.instAddCommGroupHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} : AddCommGroup (M ⟶ N)

Equations

• TauCeti.GradedModuleCat.instAddCommGroupHom = Function.Injective.addCommGroup (fun (f : M ⟶ N) => f.hom) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance TauCeti.GradedModuleCat.instModuleHom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} : Module k (M ⟶ N)

Equations

• TauCeti.GradedModuleCat.instModuleHom = Function.Injective.module k { toFun := fun (f : M ⟶ N) => f.hom, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[instance_reducible]

instance TauCeti.GradedModuleCat.instPreadditive {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : CategoryTheory.Preadditive (GradedModuleCat 𝒜)

Equations

• TauCeti.GradedModuleCat.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

@[instance_reducible]

instance TauCeti.GradedModuleCat.instLinear {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : CategoryTheory.Linear k (GradedModuleCat 𝒜)

Equations

• TauCeti.GradedModuleCat.instLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

def TauCeti.GradedModuleCat.isoMk {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (e : M.carrier ≃ₗ[A] N.carrier) (he : ∀ (p : ℤ) (x : M.carrier), x ∈ M.grading.piece p ↔ e x ∈ N.grading.piece p) : M ≅ N

The isomorphism of graded modules given by an A-linear equivalence which preserves and reflects degrees.

Equations

• TauCeti.GradedModuleCat.isoMk e he = { hom := TauCeti.GradedModuleCat.ofHom ↑e ⋯, inv := TauCeti.GradedModuleCat.ofHom ↑e.symm ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem TauCeti.GradedModuleCat.isoMk_hom_hom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (e : M.carrier ≃ₗ[A] N.carrier) (he : ∀ (p : ℤ) (x : M.carrier), x ∈ M.grading.piece p ↔ e x ∈ N.grading.piece p) : (isoMk e he).hom.hom = ↑e

@[simp]

theorem TauCeti.GradedModuleCat.isoMk_inv_hom {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (e : M.carrier ≃ₗ[A] N.carrier) (he : ∀ (p : ℤ) (x : M.carrier), x ∈ M.grading.piece p ↔ e x ∈ N.grading.piece p) : (isoMk e he).inv.hom = ↑e.symm

def TauCeti.GradedModuleCat.toModuleCat {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : CategoryTheory.Functor (GradedModuleCat 𝒜) (ModuleCat A)

The forgetful functor from graded 𝒜-modules to A-modules.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GradedModuleCat.toModuleCat_obj_carrier {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : GradedModuleCat 𝒜) : ↑(toModuleCat.obj M) = M.carrier

@[simp]

theorem TauCeti.GradedModuleCat.toModuleCat_map {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {X✝ Y✝ : GradedModuleCat 𝒜} (f : X✝ ⟶ Y✝) : toModuleCat.map f = ModuleCat.ofHom f.hom

instance TauCeti.GradedModuleCat.instFaithfulModuleCatToModuleCat {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : toModuleCat.Faithful

instance TauCeti.GradedModuleCat.instAdditiveModuleCatToModuleCat {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : toModuleCat.Additive

@[reducible, inline]

abbrev TauCeti.GradedModuleCat.shiftObj {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : GradedModuleCat 𝒜) (n : ℤ) : GradedModuleCat 𝒜

The graded module M{n}: the module M with (M{n})ₚ = M_{p-n}.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.GradedModuleCat.instFiniteCarrierShiftObj {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : GradedModuleCat 𝒜) [Module.Finite k M.carrier] (n : ℤ) : Module.Finite k (M.shiftObj n).carrier

A shift of a graded module has the same underlying k-module, so it is finite whenever the module is.

theorem TauCeti.GradedModuleCat.mem_shiftObj_piece_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : GradedModuleCat 𝒜) (n p : ℤ) (x : M.carrier) : x ∈ (M.shiftObj n).grading.piece p ↔ x ∈ M.grading.piece (p - n)

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

The shift M ↦ M{n} of graded modules, the identity on underlying linear maps.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GradedModuleCat.shiftFunctor_obj {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : GradedModuleCat 𝒜) (n : ℤ) : (shiftFunctor n).obj M = M.shiftObj n

@[simp]

theorem TauCeti.GradedModuleCat.hom_shiftFunctor_map {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (n : ℤ) (f : M ⟶ N) : ((shiftFunctor n).map f).hom = f.hom

def TauCeti.GradedModuleCat.shift {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : GradedModuleCat 𝒜 ≌ GradedModuleCat 𝒜

The grading shift M ↦ M{1} of graded 𝒜-modules, with (M{1})ₚ = M_{p-1}, as an autoequivalence; its inverse is M ↦ M{-1}.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GradedModuleCat.mem_shift_functor_obj_piece_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : GradedModuleCat 𝒜) (p : ℤ) (x : M.carrier) : x ∈ ((shift 𝒜).functor.obj M).grading.piece p ↔ x ∈ M.grading.piece (p - 1)

@[simp]

theorem TauCeti.GradedModuleCat.mem_shift_inverse_obj_piece_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : GradedModuleCat 𝒜) (p : ℤ) (x : M.carrier) : x ∈ ((shift 𝒜).inverse.obj M).grading.piece p ↔ x ∈ M.grading.piece (p + 1)

@[simp]

theorem TauCeti.GradedModuleCat.hom_shift_functor_map {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : ((shift 𝒜).functor.map f).hom = f.hom

@[simp]

theorem TauCeti.GradedModuleCat.hom_shift_inverse_map {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : ((shift 𝒜).inverse.map f).hom = f.hom

def TauCeti.GradedModuleCat.shiftFunctorCompToModuleCatIso {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (n : ℤ) : (shiftFunctor n).comp toModuleCat ≅ toModuleCat

Forgetting the internal grading identifies every grading shift with the identity functor on underlying modules.

Equations

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

@[simp]

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

@[simp]

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

instance TauCeti.GradedModuleCat.instAdditiveShiftFunctor {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (n : ℤ) : (shiftFunctor n).Additive

instance TauCeti.GradedModuleCat.instLinearShiftFunctor {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (n : ℤ) : CategoryTheory.Functor.Linear k (shiftFunctor n)

instance TauCeti.GradedModuleCat.instAdditiveFunctorShift {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : (shift 𝒜).functor.Additive

instance TauCeti.GradedModuleCat.instLinearFunctorShift {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : CategoryTheory.Functor.Linear k (shift 𝒜).functor