Surplus counts for the actual separated principal intervals #
@[instance_reducible]
def
MagnitudeConjecture.Graded.FiniteGradedModule.packedSurplusIntervalFintype
{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)
(m : ℕ)
:
Fintype (PrincipalIntervalCategory R ⋯ e he0 m)
Instances For
@[instance_reducible]
def
MagnitudeConjecture.Graded.FiniteGradedModule.packedSurplusIntervalOpFintype
{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)
(m : ℕ)
:
Fintype (PrincipalIntervalCategory R ⋯ e he0 m)ᵒᵖ
Instances For
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedFiniteRepresentables
{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 : ℕ)
(X : PrincipalRetainedCategory R ⋯ e he0 r h q)
:
Representables on the literal retained category are finite dimensional.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.principalRetained_surplus_eq_q_mul_interval
{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 : ℕ)
(hrep : CoveringHom.IsLocallyRepresentationFinite)
(hsmall : CoveringHom.IsLocallyRepresentationFinite)
:
CoveringHom.finiteCategorySurplus ⋯ hrep = ↑q * CoveringHom.finiteCategorySurplus ⋯ hsmall
The literal retained category has q times the small interval's surplus.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.principalPackedDeletion_surplus_eq_q_mul_interval
{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 : ℕ)
(hambient : CoveringHom.IsLocallyRepresentationFinite)
(hsmall : CoveringHom.IsLocallyRepresentationFinite)
:
ObjectDeletion.finiteDeletionSurplus ⋯ hambient
(principalIntervalSeparatedDeleted R ⋯ e he0 h (GradedInterval.packingEnd r h q) r q) = ↑q * CoveringHom.finiteCategorySurplus ⋯ hsmall
The literal gap-deletion category has q times the small interval's surplus.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.principalInterval_surplus_packing
{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)
[IsAlgClosed k]
(hdiag : ∀ (i : ι), Module.finrank k ↥(cornerComponent R (e i) (e i) 0) = 1)
(hneg : ∀ d < 0, R.component d = ⊥)
(hoff : ∀ (i j : ι), i ≠ j → cornerComponent R (e i) (e j) 0 = ⊥)
(h : ℕ)
(hupper : ∀ (d : ℤ), ↑h < d → R.component d = ⊥)
(r q : ℕ)
(hambient : CoveringHom.IsLocallyRepresentationFinite)
(hsmall : CoveringHom.IsLocallyRepresentationFinite)
(H : CoveringHom.HasAcyclicFiniteModuleNonzeroNonisomorphisms)
:
↑q * CoveringHom.finiteCategorySurplus ⋯ hsmall ≤ CoveringHom.finiteCategorySurplus ⋯ hambient
Finite directed deletion gives the actual separated-interval packing inequality.