Quotienting a linear category by deleted objects

For a set S of objects of a linear category C, the manuscript writes C/(S) for the category whose objects are those outside S and whose Hom spaces are quotiented by the ideal of maps factoring through finite direct sums of objects of S.

The ideal below is generated by all endomorphisms of objects in S. Equivalently it is generated by their identity morphisms, so its elements are finite linear combinations of maps factoring through deleted objects. We first form the raw Hom-ideal quotient and then take the full subcategory on the surviving objects; deleted objects therefore do not remain as a family of isomorphic zero objects.

def MagnitudeConjecture.ObjectDeletion.endomorphismRelations (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) (X Y : C) : Set (X ⟶ Y)

Relation generators supported at a deleted object. Taking all endomorphisms rather than only the identity gives the same generated ideal and avoids transporting identities across object equalities.

def MagnitudeConjecture.ObjectDeletion.ideal {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal C

The two-sided linear Hom ideal generated by the deleted objects.

theorem MagnitudeConjecture.ObjectDeletion.endomorphism_mem_ideal {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) (f : X ⟶ X) : f ∈ (ideal C S).hom X X

Every endomorphism of a deleted object belongs to the deletion ideal.

theorem MagnitudeConjecture.ObjectDeletion.id_mem_ideal {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) : CategoryTheory.CategoryStruct.id X ∈ (ideal C S).hom X X

In particular, the identity of a deleted object belongs to the deletion ideal.

theorem MagnitudeConjecture.ObjectDeletion.comp_mem_ideal {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} (hZ : Z ∈ S) (a : X ⟶ Z) (b : Z ⟶ Y) : CategoryTheory.CategoryStruct.comp a b ∈ (ideal C S).hom X Y

Every map which factors through one deleted object belongs to the deletion ideal.

@[reducible, inline]

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

The raw quotient in which deleted objects are still present as zero objects.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.ObjectDeletion.rawPreadditive {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : CategoryTheory.Preadditive (RawCategory C S)

@[reducible, inline]

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

The raw quotient functor.

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

@[instance_reducible]

noncomputable instance MagnitudeConjecture.ObjectDeletion.rawLinear {k : Type w} [Ring k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : CategoryTheory.Linear k (RawCategory C S)

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

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

The full subcategory of original objects which survive the deletion.

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

The full subcategory of raw quotient objects represented by surviving objects.

@[reducible, inline]

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

The manuscript's category C/(S): surviving objects with Hom spaces modulo maps factoring through deleted objects.

@[reducible, inline]

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

The ambient full subcategory on the surviving objects.

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

The quotient functor on surviving objects.

instance MagnitudeConjecture.ObjectDeletion.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) : (functor C S).Additive

instance MagnitudeConjecture.ObjectDeletion.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) : CategoryTheory.Functor.Linear k (functor C S)

instance MagnitudeConjecture.ObjectDeletion.functor_full {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).Full

theorem MagnitudeConjecture.ObjectDeletion.functor_map_eq_zero_iff {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 : SurvivingCategory C S} (f : X ⟶ Y) : (functor C S).map f = 0 ↔ f.hom ∈ (ideal C S).hom X.obj Y.obj

A surviving morphism maps to zero exactly when its ambient representative belongs to the ideal generated by the deleted objects.

theorem MagnitudeConjecture.ObjectDeletion.rawFunctor_obj_isZero {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) : CategoryTheory.Limits.IsZero ((rawFunctor C S).obj X)

Every deleted object becomes a zero object in the raw quotient.