Admissible locally bounded categories

This is the manuscript's covering-theoretic admissibility package: local representation-finiteness, directedness of the finite-support module category, and containment of every finite object set in a finite convex full subcategory. Object deletion preserves all three clauses.

structure MagnitudeConjecture.CoveringHom.IsLocallyBounded {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : Prop

The locally bounded structure used throughout the covering argument. Besides skeletality and local endomorphism rings, it records finite support and finite-dimensionality of both covariant representables and coefficient- dual corepresentables.

• skeletal : CategoryTheory.Skeletal C
• finiteCovariantRepresentables (X : C) : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)
• finiteDualCorepresentables (X : C) : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)
• localEndomorphismRings (X : C) : IsLocalRing (CategoryTheory.End X)

def MagnitudeConjecture.CoveringHom.BaseNonzeroNonisomorphism {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Y : C) : Prop

A nonzero nonisomorphism in the base linear category.

def MagnitudeConjecture.CoveringHom.IsConvexObjectSet {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (U : Set C) : Prop

A set of objects is convex when every vertex on a path of nonzero nonisomorphisms between two of its vertices also belongs to it.

def MagnitudeConjecture.CoveringHom.HasFiniteConvexObjectNeighborhoods {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Prop

Every finite object set is contained in a finite convex full subcategory, recorded by its object set.

structure MagnitudeConjecture.CoveringHom.IsAdmissible {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : Prop

The exact admissibility package used in the local-deletion and finite-covering arguments.

• locallyBounded : IsLocallyBounded
• locallyRepresentationFinite : IsLocallyRepresentationFinite
• directed : HasAcyclicFiniteModuleNonzeroNonisomorphisms
• finiteConvexNeighborhoods : HasFiniteConvexObjectNeighborhoods

theorem MagnitudeConjecture.ObjectDeletion.isLocallyBounded_deletion {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (H : CoveringHom.IsLocallyBounded) : CoveringHom.IsLocallyBounded

Locally bounded structure descends to every literal object-deletion quotient.

theorem MagnitudeConjecture.ObjectDeletion.hasFiniteConvexObjectNeighborhoods_deletion {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (H : CoveringHom.HasFiniteConvexObjectNeighborhoods) : CoveringHom.HasFiniteConvexObjectNeighborhoods

Finite convex object neighborhoods descend to an object-deletion category.

theorem MagnitudeConjecture.ObjectDeletion.isAdmissible_deletion {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (H : CoveringHom.IsAdmissible) : CoveringHom.IsAdmissible

Every literal object-deletion quotient of an admissible category is again admissible.