Translation of the degree-labelled principal-projective category

def MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeShiftMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (t : ℤ) {p q : PrincipalDegreeCategory R ⋯ e he0} (f : p ⟶ q) : (have this := (p.1, p.2 + t); this) ⟶ have this := (q.1, q.2 + t); this

Simultaneous degree translation leaves the corner coefficient unchanged.

@[simp]

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeShiftMap_coeff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (t : ℤ) {p q : PrincipalDegreeCategory R ⋯ e he0} (f : p ⟶ q) : ↑((principalDegreeHomEquiv R ⋯ e he0 he (have this := (p.1, p.2 + t); this) (have this := (q.1, q.2 + t); this)) (principalDegreeShiftMap R ⋯ e he0 he t f)) = ↑((principalDegreeHomEquiv R ⋯ e he0 he p q) f)

def MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeShift {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (t : ℤ) : CategoryTheory.Functor (PrincipalDegreeCategory R ⋯ e he0) (PrincipalDegreeCategory R ⋯ e he0)

Translation is a functor on degree-labelled principal projectives.

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeShift_faithful {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (t : ℤ) : (principalDegreeShift R ⋯ e he0 he t).Faithful

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeShift_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (t : ℤ) : (principalDegreeShift R ⋯ e he0 he t).Full

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeShift_essSurj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (t : ℤ) : (principalDegreeShift R ⋯ e he0 he t).EssSurj

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeShift_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (t : ℤ) : (principalDegreeShift R ⋯ e he0 he t).Additive

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeShift_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (t : ℤ) : CategoryTheory.Functor.Linear k (principalDegreeShift R ⋯ e he0 he t)

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeShiftEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (t : ℤ) : PrincipalDegreeCategory R ⋯ e he0 ≌ PrincipalDegreeCategory R ⋯ e he0

Every common degree translation is an equivalence.