The product algebra of translated principal-projective blocks

@[reducible, inline]

abbrev MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalTuple {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) (r : ℕ) : CategoryTheory.Mat_ (PrincipalDegreeCategory R ⋯ e he0)

A single interval as a tuple in the whole principal degree category.

def MagnitudeConjecture.Graded.FiniteGradedModule.principalBlockFamily {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) (r h j : ℕ) (p : ι × Fin (r + 1)) : PrincipalDegreeCategory R ⋯ e he0

The principal projective at one point of the j-th translated block.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalBlockFamily_inBlock {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) (r h j : ℕ) (p : ι × Fin (r + 1)) : GradedInterval.InBlock r h j (principalBlockFamily R ⋯ e he0 r h j p).2

Block labels have the required degree support.

@[reducible, inline]

abbrev MagnitudeConjecture.Graded.FiniteGradedModule.principalSeparatedBlockTuple {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) (r h q : ℕ) : CategoryTheory.Mat_ (PrincipalDegreeCategory R ⋯ e he0)

The tuple of all retained translated blocks.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalBlockEndAlgEquiv {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) (r h q : ℕ) (j : Fin q) : CategoryTheory.End (principalIntervalTuple R ⋯ e he0 r) ≃ₐ[k] CategoryTheory.End (CategoryTheory.blockMatrixTupleAt (fun (l : Fin q) => principalBlockFamily R ⋯ e he0 r h ↑l) j)

Common degree translation identifies each block's endomorphism algebra with the original interval tuple's algebra.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalSeparatedBlockEndAlgEquiv {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) (hneg : ∀ d < 0, R.component d = ⊥) (h : ℕ) (hupper : ∀ (d : ℤ), ↑h < d → R.component d = ⊥) (r q : ℕ) : CategoryTheory.End (principalSeparatedBlockTuple R ⋯ e he0 r h q) ≃ₐ[k] Fin q → CategoryTheory.End (principalIntervalTuple R ⋯ e he0 r)

The algebra of q separated blocks is the product of q copies of the small interval tuple's algebra.