Comparing successive and union object deletions

For sets of objects S and T, the manuscript freely identifies deleting S and then the surviving objects represented by T with deleting S ∪ T at once. This file constructs the canonical linear functor between those categories. Its faithfulness is the substantive point: modulo the first deletion ideal, the extra kernel is generated exactly by the still-surviving objects in T.

theorem MagnitudeConjecture.ObjectDeletion.mem_ideal_empty_iff {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X Y : C} (f : X ⟶ Y) : f ∈ (ideal C ∅).hom X Y ↔ f = 0

The ideal generated by the empty set of objects contains only the zero morphism.

def MagnitudeConjecture.ObjectDeletion.emptyDeletionFunctor {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Functor C (DeletionCategory C ∅)

Deleting no objects gives a category equivalent to the original one.

instance MagnitudeConjecture.ObjectDeletion.emptyDeletionFunctor_additive {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : (emptyDeletionFunctor C).Additive

instance MagnitudeConjecture.ObjectDeletion.emptyDeletionFunctor_linear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Functor.Linear k (emptyDeletionFunctor C)

instance MagnitudeConjecture.ObjectDeletion.emptyDeletionFunctor_full {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : (emptyDeletionFunctor C).Full

instance MagnitudeConjecture.ObjectDeletion.emptyDeletionFunctor_faithful {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : (emptyDeletionFunctor C).Faithful

instance MagnitudeConjecture.ObjectDeletion.emptyDeletionFunctor_essSurj {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : (emptyDeletionFunctor C).EssSurj

noncomputable def MagnitudeConjecture.ObjectDeletion.emptyDeletionEquivalence {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : C ≌ DeletionCategory C ∅

Canonical equivalence between the ambient category and deletion by the empty object set.

noncomputable def MagnitudeConjecture.ObjectDeletion.deletionEquivalenceOfEq {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {S T : Set C} (h : S = T) : DeletionCategory C S ≌ DeletionCategory C T

Equal deleted-object sets give definitionally the same deletion category, after transporting along the equality.

instance MagnitudeConjecture.ObjectDeletion.deletionEquivalenceOfEq_functor_additive {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {S T : Set C} (h : S = T) : (deletionEquivalenceOfEq C h).functor.Additive

instance MagnitudeConjecture.ObjectDeletion.deletionEquivalenceOfEq_functor_linear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {S T : Set C} (h : S = T) : CategoryTheory.Functor.Linear k (deletionEquivalenceOfEq C h).functor

theorem MagnitudeConjecture.ObjectDeletion.deletionEquivalenceOfEq_functor_obj_bijective {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {S T : Set C} (h : S = T) : Function.Bijective (deletionEquivalenceOfEq C h).functor.obj

The equivalence attached to equality of deleted sets is literally bijective on objects.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.deletionEquivalenceOfEq_functor_obj_as {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {S T : Set C} (h : S = T) (X : DeletionCategory C S) : ((deletionEquivalenceOfEq C h).functor.obj X).obj.as = X.obj.as

theorem MagnitudeConjecture.ObjectDeletion.ideal_mono {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {S T : Set C} (hST : S ⊆ T) {X Y : C} {f : X ⟶ Y} (hf : f ∈ (ideal C S).hom X Y) : f ∈ (ideal C T).hom X Y

Inclusion of deleted object sets induces inclusion of deletion ideals.

theorem MagnitudeConjecture.ObjectDeletion.rawFunctorOfLE_isKilledBy {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {S T : Set C} (hST : S ⊆ T) : (ideal C S).IsKilledBy (rawFunctor C T)

The larger raw quotient kills the smaller deletion ideal.

noncomputable def MagnitudeConjecture.ObjectDeletion.rawFunctorOfLE {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {S T : Set C} (hST : S ⊆ T) : CategoryTheory.Functor (RawCategory C S) (RawCategory C T)

The canonical functor from a smaller raw deletion quotient to a larger one.

instance MagnitudeConjecture.ObjectDeletion.rawFunctorOfLE_additive {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {S T : Set C} (hST : S ⊆ T) : (rawFunctorOfLE C hST).Additive

instance MagnitudeConjecture.ObjectDeletion.rawFunctorOfLE_linear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {S T : Set C} (hST : S ⊆ T) : CategoryTheory.Functor.Linear k (rawFunctorOfLE C hST)

instance MagnitudeConjecture.ObjectDeletion.rawFunctorOfLE_full {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {S T : Set C} (hST : S ⊆ T) : (rawFunctorOfLE C hST).Full

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.rawFunctorOfLE_map_rawFunctor {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {S T : Set C} (hST : S ⊆ T) {X Y : C} (f : X ⟶ Y) : (rawFunctorOfLE C hST).map ((rawFunctor C S).map f) = (rawFunctor C T).map f

def MagnitudeConjecture.ObjectDeletion.AdditionalDeleted {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : Set (DeletionCategory C S)

After deleting S, these are the surviving objects represented by T. Objects lying in S ∩ T are already absent.

@[reducible, inline]

abbrev MagnitudeConjecture.ObjectDeletion.IteratedDeletionCategory {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : Type u

The result of deleting S and then the surviving representatives of T.

def MagnitudeConjecture.ObjectDeletion.survivingObj {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {X : C} (hX : X ∉ S) : DeletionCategory C S

A surviving ambient object, regarded as an object of C/(S).

def MagnitudeConjecture.ObjectDeletion.survivingMap {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {X Y : C} (hX : X ∉ S) (hY : Y ∉ S) (f : X ⟶ Y) : survivingObj C S hX ⟶ survivingObj C S hY

The image in C/(S) of an ambient map between surviving objects.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.survivingMap_zero {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {X Y : C} (hX : X ∉ S) (hY : Y ∉ S) : survivingMap C S hX hY 0 = 0

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.survivingMap_add {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {X Y : C} (hX : X ∉ S) (hY : Y ∉ S) (f g : X ⟶ Y) : survivingMap C S hX hY (f + g) = survivingMap C S hX hY f + survivingMap C S hX hY g

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.survivingMap_smul {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {X Y : C} (hX : X ∉ S) (hY : Y ∉ S) (c : k) (f : X ⟶ Y) : survivingMap C S hX hY (c • f) = c • survivingMap C S hX hY f

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.survivingMap_comp {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {X Y Z : C} (hX : X ∉ S) (hY : Y ∉ S) (hZ : Z ∉ S) (f : X ⟶ Y) (g : Y ⟶ Z) : survivingMap C S hX hZ (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (survivingMap C S hX hY f) (survivingMap C S hY hZ g)

theorem MagnitudeConjecture.ObjectDeletion.survivingMap_mem_additionalIdeal_of_mem_unionIdeal {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) {X Y : C} (hX : X ∉ S) (hY : Y ∉ S) {f : X ⟶ Y} (hf : f ∈ (ideal C (S ∪ T)).hom X Y) : survivingMap C S hX hY f ∈ (ideal (DeletionCategory C S) (AdditionalDeleted C S T)).hom (survivingObj C S hX) (survivingObj C S hY)

If an ambient map belongs to the union deletion ideal, its image after deleting S belongs to the ideal generated by the still-surviving objects represented by T.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.ObjectDeletion.firstDeletionToRawUnion {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : CategoryTheory.Functor (DeletionCategory C S) (RawCategory C (S ∪ T))

The first deletion category maps canonically to the raw quotient by S ∪ T.

theorem MagnitudeConjecture.ObjectDeletion.firstDeletionToRawUnion_isKilledBy {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : (ideal (DeletionCategory C S) (AdditionalDeleted C S T)).IsKilledBy (firstDeletionToRawUnion C S T)

The canonical map to the union quotient kills the objects represented by T after the first deletion.

theorem MagnitudeConjecture.ObjectDeletion.firstDeletionToRawUnion_kernel_le {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) {X Y : DeletionCategory C S} {f : X ⟶ Y} (hf : (firstDeletionToRawUnion C S T).map f = 0) : f ∈ (ideal (DeletionCategory C S) (AdditionalDeleted C S T)).hom X Y

No additional morphisms vanish in the union quotient: the kernel after the first deletion is contained in the ideal generated by surviving representatives of T.

noncomputable def MagnitudeConjecture.ObjectDeletion.iteratedRawToRawUnion {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : CategoryTheory.Functor (RawCategory (DeletionCategory C S) (AdditionalDeleted C S T)) (RawCategory C (S ∪ T))

The canonical functor from the raw iterated quotient to the raw quotient by the union.

instance MagnitudeConjecture.ObjectDeletion.iteratedRawToRawUnion_additive {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : (iteratedRawToRawUnion C S T).Additive

instance MagnitudeConjecture.ObjectDeletion.iteratedRawToRawUnion_linear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : CategoryTheory.Functor.Linear k (iteratedRawToRawUnion C S T)

instance MagnitudeConjecture.ObjectDeletion.iteratedRawToRawUnion_full {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : (iteratedRawToRawUnion C S T).Full

instance MagnitudeConjecture.ObjectDeletion.iteratedRawToRawUnion_faithful {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : (iteratedRawToRawUnion C S T).Faithful

noncomputable def MagnitudeConjecture.ObjectDeletion.iteratedToUnionFunctor {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : CategoryTheory.Functor (IteratedDeletionCategory C S T) (DeletionCategory C (S ∪ T))

The canonical linear functor from successive deletion to deletion by the union.

instance MagnitudeConjecture.ObjectDeletion.iteratedToUnionFunctor_additive {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : (iteratedToUnionFunctor C S T).Additive

instance MagnitudeConjecture.ObjectDeletion.iteratedToUnionFunctor_linear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : CategoryTheory.Functor.Linear k (iteratedToUnionFunctor C S T)

instance MagnitudeConjecture.ObjectDeletion.iteratedToUnionFunctor_full {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : (iteratedToUnionFunctor C S T).Full

instance MagnitudeConjecture.ObjectDeletion.iteratedToUnionFunctor_faithful {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : (iteratedToUnionFunctor C S T).Faithful

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.iteratedToUnionFunctor_obj_as {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) (X : IteratedDeletionCategory C S T) : ((iteratedToUnionFunctor C S T).obj X).obj.as = X.obj.as.obj.as

instance MagnitudeConjecture.ObjectDeletion.iteratedToUnionFunctor_essSurj {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : (iteratedToUnionFunctor C S T).EssSurj

noncomputable def MagnitudeConjecture.ObjectDeletion.iteratedDeletionEquivalence {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : IteratedDeletionCategory C S T ≌ DeletionCategory C (S ∪ T)

Successive object deletion is canonically equivalent to deletion by the union.

instance MagnitudeConjecture.ObjectDeletion.iteratedDeletionEquivalence_functor_additive {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : (iteratedDeletionEquivalence C S T).functor.Additive

instance MagnitudeConjecture.ObjectDeletion.iteratedDeletionEquivalence_functor_linear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : CategoryTheory.Functor.Linear k (iteratedDeletionEquivalence C S T).functor

theorem MagnitudeConjecture.ObjectDeletion.iteratedDeletionEquivalence_functor_obj_bijective {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : Function.Bijective (iteratedDeletionEquivalence C S T).functor.obj

The canonical equivalence from successive deletion to union deletion is literally bijective on objects, not merely essentially surjective.

noncomputable def MagnitudeConjecture.ObjectDeletion.iteratedDeletionObjectEquiv {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) : IteratedDeletionCategory C S T ≃ DeletionCategory C (S ∪ T)

The literal object bijection underlying successive deletion.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.iteratedDeletionObjectEquiv_apply {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) (X : IteratedDeletionCategory C S T) : (iteratedDeletionObjectEquiv C S T) X = (iteratedDeletionEquivalence C S T).functor.obj X

theorem MagnitudeConjecture.ObjectDeletion.map_mem_singleton_ideal {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (q : C) {X Y : C} {f : X ⟶ Y} (hf : f ∈ (ideal C {q}).hom X Y) : e.functor.map f ∈ (ideal D {e.functor.obj q}).hom (e.functor.obj X) (e.functor.obj Y)

A linear equivalence carries the ideal generated by one object into the ideal generated by its image.

theorem MagnitudeConjecture.ObjectDeletion.mem_singleton_ideal_of_map {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (q : C) {X Y : C} {f : X ⟶ Y} (hf : e.functor.map f ∈ (ideal D {e.functor.obj q}).hom (e.functor.obj X) (e.functor.obj Y)) : f ∈ (ideal C {q}).hom X Y

For an equivalence, membership in a singleton-generated deletion ideal is also reflected from the image category.

theorem MagnitudeConjecture.ObjectDeletion.singletonIdeal_isKilledBy {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (q : C) : (ideal C {q}).IsKilledBy (e.functor.comp (rawFunctor D {e.functor.obj q}))

The composite from the source category to the raw quotient by the image object kills the source singleton deletion ideal.

noncomputable def MagnitudeConjecture.ObjectDeletion.rawSingletonDeletionMapFunctor {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (q : C) : CategoryTheory.Functor (RawCategory C {q}) (RawCategory D {e.functor.obj q})

The induced functor between the two raw singleton-deletion quotients.

instance MagnitudeConjecture.ObjectDeletion.rawSingletonDeletionMapFunctor_additive {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (q : C) : (rawSingletonDeletionMapFunctor C e q).Additive

instance MagnitudeConjecture.ObjectDeletion.rawSingletonDeletionMapFunctor_linear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (q : C) : CategoryTheory.Functor.Linear k (rawSingletonDeletionMapFunctor C e q)

instance MagnitudeConjecture.ObjectDeletion.rawSingletonDeletionMapFunctor_full {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (q : C) : (rawSingletonDeletionMapFunctor C e q).Full

instance MagnitudeConjecture.ObjectDeletion.rawSingletonDeletionMapFunctor_faithful {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (q : C) : (rawSingletonDeletionMapFunctor C e q).Faithful

noncomputable def MagnitudeConjecture.ObjectDeletion.singletonDeletionMapFunctor {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) (q : C) : CategoryTheory.Functor (DeletionCategory C {q}) (DeletionCategory D {e.functor.obj q})

Restrict singleton-deletion change of base to the surviving objects.

instance MagnitudeConjecture.ObjectDeletion.singletonDeletionMapFunctor_additive {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) (q : C) : (singletonDeletionMapFunctor C e hobj q).Additive

instance MagnitudeConjecture.ObjectDeletion.singletonDeletionMapFunctor_linear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) (q : C) : CategoryTheory.Functor.Linear k (singletonDeletionMapFunctor C e hobj q)

instance MagnitudeConjecture.ObjectDeletion.singletonDeletionMapFunctor_full {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) (q : C) : (singletonDeletionMapFunctor C e hobj q).Full

instance MagnitudeConjecture.ObjectDeletion.singletonDeletionMapFunctor_faithful {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) (q : C) : (singletonDeletionMapFunctor C e hobj q).Faithful

theorem MagnitudeConjecture.ObjectDeletion.singletonDeletionMapFunctor_essSurj {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) (q : C) : (singletonDeletionMapFunctor C e hobj q).EssSurj

Every target survivor is represented by an inverse image survivor.

noncomputable def MagnitudeConjecture.ObjectDeletion.singletonDeletionEquivalence {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) (q : C) : DeletionCategory C {q} ≌ DeletionCategory D {e.functor.obj q}

Deleting one object commutes with an additive linear equivalence whose forward object map is a literal bijection.

instance MagnitudeConjecture.ObjectDeletion.singletonDeletionEquivalence_functor_additive {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) (q : C) : (singletonDeletionEquivalence C e hobj q).functor.Additive

instance MagnitudeConjecture.ObjectDeletion.singletonDeletionEquivalence_functor_linear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) (q : C) : CategoryTheory.Functor.Linear k (singletonDeletionEquivalence C e hobj q).functor