Interval representations and supported graded representations

Contravariant finite-dimensional representations of a finite degree interval are equivalent to contravariant representations of the full degree category vanishing outside that interval. The latter are the categorical form of supported graded modules. Their identification with modules over the original graded algebra is a separate step.

theorem MagnitudeConjecture.GradedCategory.HomGrading.intervalOpDeletion_obj_bijective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (h : ℕ) (hbound : ∀ (X Y : C) (d : ℤ), d < 0 ∨ ↑h < d → G.component X Y d = ⊥) (m : ℕ) : Function.Bijective (G.intervalOpDeletionEquivalence h hbound m).functor.obj

The interval/deletion comparison is literally bijective on objects, not merely essentially surjective. Thus finite literal support is preserved.

noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.intervalSupportedModuleEquivalence {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (h : ℕ) (hbound : ∀ (X Y : C) (d : ℤ), d < 0 ∨ ↑h < d → G.component X Y d = ⊥) (m : ℕ) : CoveringHom.FiniteDimensionalModuleCategory k ≌ ObjectDeletion.VanishingFiniteModuleCategory (DegreeObject G)ᵒᵖ (G.outsideIntervalOp m)

Finite-dimensional contravariant interval representations are precisely the ambient contravariant degree representations supported on the interval.

@[instance_reducible]

def MagnitudeConjecture.GradedCategory.HomGrading.intervalOppositeFintype {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) [Fintype C] (m : ℕ) : Fintype (G.Interval m)ᵒᵖ

theorem MagnitudeConjecture.GradedCategory.HomGrading.intervalFiniteRepresentables {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) [Fintype C] (hfinite : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) (m : ℕ) (X : (G.Interval m)ᵒᵖ) : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)

All contravariant interval representables have finite dimension and finite object support.

@[reducible, inline]

abbrev MagnitudeConjecture.GradedCategory.HomGrading.intervalAlgebra {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) [Fintype C] (hfinite : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) (m : ℕ) : Type (max u v)

The endomorphism algebra of the sum of the interval representables. Its finitely generated right modules have the required contravariant variance.

theorem MagnitudeConjecture.GradedCategory.HomGrading.intervalAlgebra_finiteDimensional {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) [Fintype C] (hfinite : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) (m : ℕ) : FiniteDimensional k (G.intervalAlgebra hfinite m)

noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.intervalAlgebraSupportedModuleEquivalence {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (h : ℕ) (hbound : ∀ (X Y : C) (d : ℤ), d < 0 ∨ ↑h < d → G.component X Y d = ⊥) [Fintype C] (hfinite : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) (m : ℕ) : FGModuleCat (G.intervalAlgebra hfinite m)ᵐᵒᵖ ≌ ObjectDeletion.VanishingFiniteModuleCategory (DegreeObject G)ᵒᵖ (G.outsideIntervalOp m)

Finitely generated right modules over the interval algebra are precisely finite-dimensional contravariant degree representations supported there.