Universe-independent finite category deletion

The category algebra used by the primitive-deletion theorem is formed after reindexing a finite object type by Fin n. This keeps its objects small without changing any Hom space. The induced base equivalence transports finite-dimensional module skeletons and their Auslander--Reiten surplus, so the checked finite deletion theorem applies to a finite category in an arbitrary object universe.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.FiniteObjectModel {C : Type u} [Fintype C] : Type

A finite category reindexed by a small Fin object type.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.CoveringHom.finiteObjectModel_fintype {C : Type u} [Fintype C] : Fintype FiniteObjectModel

noncomputable def MagnitudeConjecture.CoveringHom.finiteObjectEquiv {C : Type u} [Fintype C] : FiniteObjectModel ≃ C

The literal object equivalence from the small model to the original finite category.

noncomputable def MagnitudeConjecture.CoveringHom.finiteObjectModelEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [Fintype C] : FiniteObjectModel ≌ C

Reindexing by Fin is a linear equivalence of base categories.

instance MagnitudeConjecture.CoveringHom.finiteObjectModelEquivalence_functor_additive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [Fintype C] : finiteObjectModelEquivalence.functor.Additive

instance MagnitudeConjecture.CoveringHom.finiteObjectModelEquivalence_functor_linear {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] : CategoryTheory.Functor.Linear k finiteObjectModelEquivalence.functor

@[simp]

theorem MagnitudeConjecture.CoveringHom.finiteObjectModelEquivalence_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [Fintype C] (X : FiniteObjectModel) : finiteObjectModelEquivalence.functor.obj X = finiteObjectEquiv X

noncomputable def MagnitudeConjecture.CoveringHom.finiteObjectModelModuleEquivalence {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] : FiniteDimensionalModuleCategory k ≌ FiniteDimensionalModuleCategory k

The induced equivalence gives the corresponding equivalence of finite-dimensional module categories.

instance MagnitudeConjecture.CoveringHom.finiteObjectModelModuleEquivalence_functor_additive {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] : finiteObjectModelModuleEquivalence.functor.Additive

instance MagnitudeConjecture.CoveringHom.ObjectDeletion.deletionCategory_finite {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Finite C] (S : Set C) : Finite (ObjectDeletion.DeletionCategory C S)

A deletion category of a finite object type again has finitely many objects.

theorem MagnitudeConjecture.CoveringHom.finiteObjectModel_finiteCovariantRepresentables {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (X : FiniteObjectModel) : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)

Reindexing preserves finite-dimensional covariant representables.

noncomputable def MagnitudeConjecture.CoveringHom.finiteObjectModelEndRingEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [Fintype C] (X : FiniteObjectModel) : CategoryTheory.End X ≃+* CategoryTheory.End (finiteObjectEquiv X)

Endomorphism rings are unchanged by the induced finite reindexing.

theorem MagnitudeConjecture.CoveringHom.finiteObjectModel_localEndomorphismRings {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [Fintype C] (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (X : FiniteObjectModel) : IsLocalRing (CategoryTheory.End X)

Local vertex endomorphism rings pass to the finite object model.

theorem MagnitudeConjecture.CoveringHom.finiteObjectModel_skeletal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [Fintype C] (hC : CategoryTheory.Skeletal C) : CategoryTheory.Skeletal FiniteObjectModel

Skeletality passes to the finite object model.

theorem MagnitudeConjecture.CoveringHom.isLocallyRepresentationFinite_of_finiteSkeleton {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (S : FiniteDimensionalModuleIndecomposableSkeleton) : IsLocallyRepresentationFinite

A complete finite skeleton supplies the pointwise form of local representation-finiteness.

theorem MagnitudeConjecture.CoveringHom.finiteObjectModel_isLocallyRepresentationFinite {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hrep : IsLocallyRepresentationFinite) : IsLocallyRepresentationFinite

Local representation-finiteness passes to the finite object model.

theorem MagnitudeConjecture.CoveringHom.finiteObjectModel_hasAcyclicFiniteModuleNonzeroNonisomorphisms {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (H : HasAcyclicFiniteModuleNonzeroNonisomorphisms) : HasAcyclicFiniteModuleNonzeroNonisomorphisms

Directedness of the finite module category passes to the finite object model.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.singletonDeletion_surplus_le_of_fintype {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] [IsAlgClosed k] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hskel : CategoryTheory.Skeletal C) (hrep : IsLocallyRepresentationFinite) (H : HasAcyclicFiniteModuleNonzeroNonisomorphisms) (X : C) (T : FiniteDimensionalModuleIndecomposableSkeleton) (Tdeleted : FiniteDimensionalModuleIndecomposableSkeleton) : ARCount.surplus (FiniteTauMatrix.arrowMultiplicity Tdeleted.toFiniteRightTauCategoryData) Tdeleted.toFiniteRightTauCategoryData.IsProjective ≤ ARCount.surplus (FiniteTauMatrix.arrowMultiplicity T.toFiniteRightTauCategoryData) T.toFiniteRightTauCategoryData.IsProjective

Literal singleton deletion cannot increase surplus for a finite representation-directed category in an arbitrary object universe.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.finrank_obj_eq_one_of_singletonDeletion_surplus_eq_of_fintype {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] [IsAlgClosed k] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hskel : CategoryTheory.Skeletal C) (hrep : IsLocallyRepresentationFinite) (H : HasAcyclicFiniteModuleNonzeroNonisomorphisms) (X : C) (T : FiniteDimensionalModuleIndecomposableSkeleton) (Tdeleted : FiniteDimensionalModuleIndecomposableSkeleton) (hEquality : ARCount.surplus (FiniteTauMatrix.arrowMultiplicity Tdeleted.toFiniteRightTauCategoryData) Tdeleted.toFiniteRightTauCategoryData.IsProjective = ARCount.surplus (FiniteTauMatrix.arrowMultiplicity T.toFiniteRightTauCategoryData) T.toFiniteRightTauCategoryData.IsProjective) (M : FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) (hMX : ¬CategoryTheory.Limits.IsZero (M.obj.obj.obj X)) : Module.finrank k ↑(M.obj.obj.obj X) = 1

Equality in literal singleton deletion forces one-dimensional fiber at the deleted object for a finite representation-directed category in an arbitrary object universe.