Convex full subcategories and object deletion

If no morphism between surviving objects factors nontrivially through a deleted object, the deletion ideal vanishes on surviving Hom spaces. The canonical full functor from the surviving full subcategory to the deletion quotient is then an equivalence. Convexity for nonzero nonisomorphisms gives this factorization condition in a skeletal category.

@[reducible, inline]

abbrev MagnitudeConjecture.ObjectDeletion.FullSubcategoryOn (C : Type u) [CategoryTheory.Category.{v, u} C] (U : Set C) : Type u

The literal full subcategory on a set of ambient objects.

def MagnitudeConjecture.ObjectDeletion.fullSubcategoryOnToSurvivingComplFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] (U : Set C) : CategoryTheory.Functor (FullSubcategoryOn C U) (SurvivingCategory C Uᶜ)

The identity-on-underlying-objects functor from the literal full subcategory on U to the surviving subcategory for deletion by Uᶜ.

instance MagnitudeConjecture.ObjectDeletion.fullSubcategoryOnToSurvivingComplFunctor_full (C : Type u) [CategoryTheory.Category.{v, u} C] (U : Set C) : (fullSubcategoryOnToSurvivingComplFunctor C U).Full

instance MagnitudeConjecture.ObjectDeletion.fullSubcategoryOnToSurvivingComplFunctor_faithful (C : Type u) [CategoryTheory.Category.{v, u} C] (U : Set C) : (fullSubcategoryOnToSurvivingComplFunctor C U).Faithful

instance MagnitudeConjecture.ObjectDeletion.fullSubcategoryOnToSurvivingComplFunctor_essSurj (C : Type u) [CategoryTheory.Category.{v, u} C] (U : Set C) : (fullSubcategoryOnToSurvivingComplFunctor C U).EssSurj

noncomputable def MagnitudeConjecture.ObjectDeletion.fullSubcategoryOnSurvivingComplEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] (U : Set C) : FullSubcategoryOn C U ≌ SurvivingCategory C Uᶜ

The literal full subcategory on U is the surviving subcategory for deletion by the complement of U.

instance MagnitudeConjecture.ObjectDeletion.fullSubcategoryOnSurvivingComplEquivalence_functor_additive (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (U : Set C) : (fullSubcategoryOnSurvivingComplEquivalence C U).functor.Additive

instance MagnitudeConjecture.ObjectDeletion.fullSubcategoryOnSurvivingComplEquivalence_functor_linear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (U : Set C) : CategoryTheory.Functor.Linear k (fullSubcategoryOnSurvivingComplEquivalence C U).functor

def MagnitudeConjecture.ObjectDeletion.NoDeletedFactorization (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : Set C) : Prop

No morphism between surviving objects factors nontrivially through one deleted object.

theorem MagnitudeConjecture.ObjectDeletion.eq_zero_of_mem_ideal_of_noDeletedFactorization {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {S : Set C} (hS : NoDeletedFactorization C S) {X Y : C} (hX : X ∉ S) (hY : Y ∉ S) {f : X ⟶ Y} (hf : f ∈ (ideal C S).hom X Y) : f = 0

Under the no-factorization condition, every member of the deletion ideal between surviving objects is zero.

theorem MagnitudeConjecture.ObjectDeletion.functor_faithful_of_noDeletedFactorization {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (hS : NoDeletedFactorization C S) : (functor C S).Faithful

The surviving-to-deletion functor is faithful when deleted objects cannot carry a nonzero factorization between survivors.

theorem MagnitudeConjecture.ObjectDeletion.functor_essSurj {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : (functor C S).EssSurj

Every deletion-quotient object is represented by the corresponding surviving ambient object.

noncomputable def MagnitudeConjecture.ObjectDeletion.survivingDeletionEquivalence {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (hS : NoDeletedFactorization C S) : SurvivingCategory C S ≌ DeletionCategory C S

Under no deleted factorization, the retained full subcategory is equivalent to the deletion quotient.

instance MagnitudeConjecture.ObjectDeletion.survivingDeletionEquivalence_functor_additive {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (hS : NoDeletedFactorization C S) : (survivingDeletionEquivalence C S ⋯).functor.Additive

instance MagnitudeConjecture.ObjectDeletion.survivingDeletionEquivalence_functor_linear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (hS : NoDeletedFactorization C S) : CategoryTheory.Functor.Linear k (survivingDeletionEquivalence C S ⋯).functor

theorem MagnitudeConjecture.ObjectDeletion.noDeletedFactorization_compl_of_isConvexObjectSet (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (hC : CategoryTheory.Skeletal C) (U : Set C) (hU : CoveringHom.IsConvexObjectSet U) : NoDeletedFactorization C Uᶜ

In a skeletal category, convexity of the retained object set forbids a nonzero factorization between retained objects through an object outside the set.

noncomputable def MagnitudeConjecture.ObjectDeletion.convexSurvivingDeletionEquivalence {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hC : CategoryTheory.Skeletal C) (U : Set C) (hU : CoveringHom.IsConvexObjectSet U) : SurvivingCategory C Uᶜ ≌ DeletionCategory C Uᶜ

A convex retained full subcategory of a skeletal linear category is canonically equivalent to deletion by its complement.

instance MagnitudeConjecture.ObjectDeletion.convexSurvivingDeletionEquivalence_functor_additive {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hC : CategoryTheory.Skeletal C) (U : Set C) (hU : CoveringHom.IsConvexObjectSet U) : (convexSurvivingDeletionEquivalence C hC U ⋯).functor.Additive

instance MagnitudeConjecture.ObjectDeletion.convexSurvivingDeletionEquivalence_functor_linear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hC : CategoryTheory.Skeletal C) (U : Set C) (hU : CoveringHom.IsConvexObjectSet U) : CategoryTheory.Functor.Linear k (convexSurvivingDeletionEquivalence C hC U ⋯).functor

noncomputable def MagnitudeConjecture.ObjectDeletion.convexFullSubcategoryDeletionEquivalence {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hC : CategoryTheory.Skeletal C) (U : Set C) (hU : CoveringHom.IsConvexObjectSet U) : FullSubcategoryOn C U ≌ DeletionCategory C Uᶜ

The manuscript's finite convex full subcategory is linearly equivalent to the literal deletion quotient by the complementary objects.

instance MagnitudeConjecture.ObjectDeletion.convexFullSubcategoryDeletionEquivalence_functor_additive {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hC : CategoryTheory.Skeletal C) (U : Set C) (hU : CoveringHom.IsConvexObjectSet U) : (convexFullSubcategoryDeletionEquivalence C hC U ⋯).functor.Additive

instance MagnitudeConjecture.ObjectDeletion.convexFullSubcategoryDeletionEquivalence_functor_linear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hC : CategoryTheory.Skeletal C) (U : Set C) (hU : CoveringHom.IsConvexObjectSet U) : CategoryTheory.Functor.Linear k (convexFullSubcategoryDeletionEquivalence C hC U ⋯).functor