The block support of actual retained interval modules #
noncomputable def
MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlock
{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 : ℕ)
(X : PrincipalRetainedCategory R ⋯ e he0 r h q)
:
Fin q
The unique block number of a literal retained object.
Instances For
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlock_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 q : ℕ)
(X : PrincipalRetainedCategory R ⋯ e he0 r h q)
:
GradedInterval.InBlock r h ↑(principalRetainedBlock R ⋯ e he0 r h q X) ↑↑(Opposite.unop X.obj).2
The degree of a retained object lies in the block specified by its coordinates.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.principalRetained_hom_eq_zero_of_block_ne
{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 : ℕ)
(X Y : PrincipalRetainedCategory R ⋯ e he0 r h q)
(hXY : principalRetainedBlock R ⋯ e he0 r h q X ≠ principalRetainedBlock R ⋯ e he0 r h q Y)
(f : X ⟶ Y)
:
f = 0
The literal retained category has zero Hom spaces between different blocks.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.principalRetained_indecomposable_unique_block
{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 : ℕ)
(M : CoveringHom.FiniteDimensionalModuleCategory k)
(hM : CategoryTheory.Indecomposable M)
:
∃! j : Fin q, ∀ (X : PrincipalRetainedCategory R ⋯ e he0 r h q),
principalRetainedBlock R ⋯ e he0 r h q X ≠ j → CategoryTheory.Limits.IsZero (M.obj.obj.obj X)
Every indecomposable module on the actual retained category belongs to exactly one of its separated blocks.