Finite object counts under deletion

theorem MagnitudeConjecture.ObjectDeletion.deletionUnderlying_injective {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : Function.Injective fun (X : DeletionCategory C S) => X.obj.as

Distinct surviving quotient objects have distinct original labels.

@[instance_reducible]

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

theorem MagnitudeConjecture.ObjectDeletion.deletion_card_lt {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (S : Set C) {x : C} (hx : x ∈ S) : Fintype.card (DeletionCategory C S) < Fintype.card C

Deleting any specified object strictly reduces the finite object count.