Matrix algebras of deletions with no surviving factorization relation

theorem MagnitudeConjecture.ObjectDeletion.deletionFunctor_obj_bijective {k : Type v} [Field k] (C : Type) [CategoryTheory.Category.{v, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : Function.Bijective (functor C S).obj

Deletion changes morphisms but keeps exactly the surviving object set.

noncomputable def MagnitudeConjecture.ObjectDeletion.deletionObjectEquiv {k : Type v} [Field k] (C : Type) [CategoryTheory.Category.{v, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : SurvivingCategory C S ≃ DeletionCategory C S

The surviving and deleted categories have the same object coordinates.

@[instance_reducible]

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

noncomputable def MagnitudeConjecture.ObjectDeletion.survivingDeletionMatrixAlgEquiv {k : Type v} [Field k] (C : Type) [CategoryTheory.Category.{v, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) [Fintype (SurvivingCategory C S)] (hS : NoDeletedFactorization C S) : CategoryTheory.End CoveringHom.categoryAlgebraTuple ≃ₐ[k] CategoryTheory.End CoveringHom.categoryAlgebraTuple

If no nonzero composite between survivors passes through a deleted object, the finite deletion algebra equals the surviving full-category algebra.