Finite structural data inherited by object deletion

The finite-cover push-down theorem needs finite representables, finite dual corepresentables, and local vertex endomorphism rings at every intermediate deletion stage. These properties descend from the ambient locally bounded skeletal category. Hom spaces downstairs are quotients of ambient Hom spaces, while the deletion ideal at a surviving object lies in its categorical radical and hence cannot kill the identity.

theorem MagnitudeConjecture.ObjectDeletion.deletion_linearCoyoneda_isFiniteDimensional {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)) (S : Set C) (X : DeletionCategory C S) : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)

Finite-dimensionality and finite support of covariant representables pass to an object-deletion quotient.

theorem MagnitudeConjecture.ObjectDeletion.deletion_dualLinearYoneda_isFiniteDimensional {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.dualLinearYonedaLinearModule X)) (S : Set C) (X : DeletionCategory C S) : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.dualLinearYonedaLinearModule X)

Finite-dimensionality and finite support of coefficient-dual corepresentables pass to an object-deletion quotient.

theorem MagnitudeConjecture.ObjectDeletion.deletionIdeal_end_isRadical {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hC : CategoryTheory.Skeletal C) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (S : Set C) (X : C) (hX : X ∉ S) {f : X ⟶ X} (hf : f ∈ (ideal C S).hom X X) : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f

At a surviving object, every endomorphism in the deletion ideal is radical. Each spanning term factors through a deleted object, which cannot be isomorphic to the surviving source in a skeletal category.

theorem MagnitudeConjecture.ObjectDeletion.deletion_skeletal {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hC : CategoryTheory.Skeletal C) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (S : Set C) : CategoryTheory.Skeletal (DeletionCategory C S)

Deleting objects from a skeletal category with local endomorphism rings does not identify two surviving objects up to isomorphism.

theorem MagnitudeConjecture.ObjectDeletion.deletion_end_isLocalRing {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hC : CategoryTheory.Skeletal C) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (S : Set C) (X : DeletionCategory C S) : IsLocalRing (CategoryTheory.End X)

Local endomorphism rings descend to every surviving vertex of an object-deletion quotient of a skeletal category.