Adjoint module truncations for object deletion

For a set S of deleted objects, ambient modules vanishing on S form the essential image of extension by zero. This file constructs the two adjoints to their inclusion. The right adjoint takes the largest submodule vanishing on S; the left adjoint takes the largest quotient vanishing on S.

def MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmoduleObj {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) (X : C) : Submodule k ↑(M.obj X)

At X, the elements of an ambient module killed by every map from X to a deleted object.

def MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmoduleNatMap {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) {M N : CategoryTheory.Functor C (ModuleCat k)} (a : M ⟶ N) (X : C) : ↥(maximalVanishingSubmoduleObj C S M X) →ₗ[k] ↥(maximalVanishingSubmoduleObj C S N X)

A module map carries maximal vanishing submodules into one another.

def MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmodule {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) : CategoryTheory.Functor C (ModuleCat k)

The maximal submodule of M which vanishes on all deleted objects.

def MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmoduleInclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) : maximalVanishingSubmodule C S M ⟶ M

The maximal vanishing submodule includes naturally into the ambient module.

instance MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmoduleInclusion_mono {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) : CategoryTheory.Mono (maximalVanishingSubmoduleInclusion C S M)

instance MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmodule_additive {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] : (maximalVanishingSubmodule C S M).Additive

The maximal vanishing submodule is additive.

instance MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmodule_linear {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) [CategoryTheory.Functor.Linear k M] : CategoryTheory.Functor.Linear k (maximalVanishingSubmodule C S M)

The maximal vanishing submodule is linear.

def MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmoduleMap {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) {M N : CategoryTheory.Functor C (ModuleCat k)} (a : M ⟶ N) : maximalVanishingSubmodule C S M ⟶ maximalVanishingSubmodule C S N

A morphism of ambient modules restricts to their maximal vanishing submodules.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmoduleMap_comp_inclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) {M N : CategoryTheory.Functor C (ModuleCat k)} (a : M ⟶ N) : CategoryTheory.CategoryStruct.comp (maximalVanishingSubmoduleMap C S a) (maximalVanishingSubmoduleInclusion C S N) = CategoryTheory.CategoryStruct.comp (maximalVanishingSubmoduleInclusion C S M) a

def MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmoduleFunctor {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) : CategoryTheory.Functor (CategoryTheory.Functor C (ModuleCat k)) (CategoryTheory.Functor C (ModuleCat k))

The maximal-vanishing-submodule construction is functorial on ambient module-valued functors.

def MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmoduleInclusionNatTrans {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) : maximalVanishingSubmoduleFunctor C S ⟶ CategoryTheory.Functor.id (CategoryTheory.Functor C (ModuleCat k))

The maximal-vanishing-submodule inclusions form a natural transformation to the identity functor.

theorem MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmodule_vanishesOnDeleted {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) : ModuleVanishesOnDeleted C S (maximalVanishingSubmodule C S M)

The maximal vanishing submodule does vanish at every deleted object.

def MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmoduleLift {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) {E M : CategoryTheory.Functor C (ModuleCat k)} (hE : ModuleVanishesOnDeleted C S E) (a : E ⟶ M) : E ⟶ maximalVanishingSubmodule C S M

Every map from a module vanishing on the deleted objects factors through the maximal vanishing submodule of its target.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmoduleLift_comp_inclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) {E M : CategoryTheory.Functor C (ModuleCat k)} (hE : ModuleVanishesOnDeleted C S E) (a : E ⟶ M) : CategoryTheory.CategoryStruct.comp (maximalVanishingSubmoduleLift C S hE a) (maximalVanishingSubmoduleInclusion C S M) = a

theorem MagnitudeConjecture.ObjectDeletion.maximalVanishingSubmoduleLift_unique {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) {E M : CategoryTheory.Functor C (ModuleCat k)} (hE : ModuleVanishesOnDeleted C S E) (a : E ⟶ M) (b : E ⟶ maximalVanishingSubmodule C S M) (hb : CategoryTheory.CategoryStruct.comp b (maximalVanishingSubmoduleInclusion C S M) = a) : b = maximalVanishingSubmoduleLift C S hE a

Factorization through the maximal vanishing submodule is unique.

def MagnitudeConjecture.ObjectDeletion.linearMaximalVanishingSubmodule {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.LinearModuleCategory k) : CoveringHom.LinearModuleCategory k

The maximal vanishing submodule of a linear module, bundled as a linear module.

theorem MagnitudeConjecture.ObjectDeletion.linearMaximalVanishingSubmodule_isFiniteDimensional {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) : CoveringHom.IsFiniteDimensionalModule k (linearMaximalVanishingSubmodule C S M.obj)

Taking the maximal vanishing submodule preserves pointwise finite dimension and finite object support.

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingSubmodule {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) : CoveringHom.FiniteDimensionalModuleCategory k

The maximal vanishing submodule of a finite-dimensional module.

@[reducible, inline]

abbrev MagnitudeConjecture.ObjectDeletion.VanishingFiniteModuleCategory {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : Type (max u (v + 1))

The full category of ambient finite-dimensional modules vanishing on the deleted objects.

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingSubmoduleObj {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) : VanishingFiniteModuleCategory C S

The maximal vanishing submodule, bundled in the vanishing full subcategory.

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingSubmoduleFunctor {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : CategoryTheory.Functor (CoveringHom.FiniteDimensionalModuleCategory k) (VanishingFiniteModuleCategory C S)

The maximal-vanishing-submodule construction as a functor from ambient finite modules to the vanishing full subcategory.

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingSubmoduleInclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) : (finiteModuleVanishesOnDeleted C S).ι.obj ((finiteMaximalVanishingSubmoduleFunctor C S).obj M) ⟶ M

The maximal vanishing submodule includes into its ambient module.

instance MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingSubmoduleInclusion_mono {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) : CategoryTheory.Mono (finiteMaximalVanishingSubmoduleInclusion C S M)

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingSubmoduleLift {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {E : VanishingFiniteModuleCategory C S} {M : CoveringHom.FiniteDimensionalModuleCategory k} (a : E.obj ⟶ M) : E ⟶ (finiteMaximalVanishingSubmoduleFunctor C S).obj M

A morphism from a vanishing finite module to an ambient module lifts to the maximal vanishing submodule of its target.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingSubmoduleLift_comp_inclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {E : VanishingFiniteModuleCategory C S} {M : CoveringHom.FiniteDimensionalModuleCategory k} (a : E.obj ⟶ M) : CategoryTheory.CategoryStruct.comp (finiteMaximalVanishingSubmoduleLift C S a).hom (finiteMaximalVanishingSubmoduleInclusion C S M) = a

theorem MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingSubmoduleInclusion_isIso_of_vanishesOnDeleted {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) (hM : ModuleVanishesOnDeleted C S M.obj.obj) : CategoryTheory.IsIso (finiteMaximalVanishingSubmoduleInclusion C S M)

If an ambient finite module already vanishes on the deleted objects, its maximal vanishing submodule is the whole module.

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingSubmoduleHomEquiv {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (E : VanishingFiniteModuleCategory C S) (M : CoveringHom.FiniteDimensionalModuleCategory k) : ((finiteModuleVanishesOnDeleted C S).ι.obj E ⟶ M) ≃ (E ⟶ (finiteMaximalVanishingSubmoduleFunctor C S).obj M)

Universal Hom equivalence for the maximal vanishing submodule.

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingSubmoduleAdjunction {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : (finiteModuleVanishesOnDeleted C S).ι ⊣ finiteMaximalVanishingSubmoduleFunctor C S

Inclusion of the vanishing full subcategory is left adjoint to the maximal-vanishing-submodule functor.

def MagnitudeConjecture.ObjectDeletion.deletedTraceSubmoduleObj {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) (X : C) : Submodule k ↑(M.obj X)

At X, the trace generated by all maps from deleted objects into X.

theorem MagnitudeConjecture.ObjectDeletion.deletedTraceSubmoduleObj_map_le {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) {X Z : C} (h : X ⟶ Z) : deletedTraceSubmoduleObj C S M X ≤ Submodule.comap (ModuleCat.Hom.hom (M.map h)) (deletedTraceSubmoduleObj C S M Z)

The deleted trace is preserved by the structure maps of the module.

def MagnitudeConjecture.ObjectDeletion.maximalVanishingQuotient {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) : CategoryTheory.Functor C (ModuleCat k)

The largest quotient of M which vanishes on all deleted objects.

def MagnitudeConjecture.ObjectDeletion.maximalVanishingQuotientProjection {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) : M ⟶ maximalVanishingQuotient C S M

The ambient module projects naturally onto its maximal vanishing quotient.

instance MagnitudeConjecture.ObjectDeletion.maximalVanishingQuotientProjection_epi {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) : CategoryTheory.Epi (maximalVanishingQuotientProjection C S M)

instance MagnitudeConjecture.ObjectDeletion.maximalVanishingQuotient_additive {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] : (maximalVanishingQuotient C S M).Additive

The maximal vanishing quotient is additive.

instance MagnitudeConjecture.ObjectDeletion.maximalVanishingQuotient_linear {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) [CategoryTheory.Functor.Linear k M] : CategoryTheory.Functor.Linear k (maximalVanishingQuotient C S M)

The maximal vanishing quotient is linear.

theorem MagnitudeConjecture.ObjectDeletion.deletedTraceSubmoduleObj_eq_top_of_mem {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) {X : C} (hX : X ∈ S) : deletedTraceSubmoduleObj C S M X = ⊤

At a deleted object, the deleted trace is the whole module.

theorem MagnitudeConjecture.ObjectDeletion.maximalVanishingQuotient_vanishesOnDeleted {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) (M : CategoryTheory.Functor C (ModuleCat k)) : ModuleVanishesOnDeleted C S (maximalVanishingQuotient C S M)

The maximal vanishing quotient vanishes at every deleted object.

theorem MagnitudeConjecture.ObjectDeletion.deletedTraceSubmoduleObj_le_ker {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) {M E : CategoryTheory.Functor C (ModuleCat k)} (hE : ModuleVanishesOnDeleted C S E) (a : M ⟶ E) (X : C) : deletedTraceSubmoduleObj C S M X ≤ (ModuleCat.Hom.hom (a.app X)).ker

Every map from an ambient module to a module vanishing on the deleted objects kills the deleted trace.

def MagnitudeConjecture.ObjectDeletion.maximalVanishingQuotientDescend {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) {M E : CategoryTheory.Functor C (ModuleCat k)} (hE : ModuleVanishesOnDeleted C S E) (a : M ⟶ E) : maximalVanishingQuotient C S M ⟶ E

Every map from an ambient module to a module vanishing on the deleted objects descends through the maximal vanishing quotient.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.projection_comp_maximalVanishingQuotientDescend {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) {M E : CategoryTheory.Functor C (ModuleCat k)} (hE : ModuleVanishesOnDeleted C S E) (a : M ⟶ E) : CategoryTheory.CategoryStruct.comp (maximalVanishingQuotientProjection C S M) (maximalVanishingQuotientDescend C S hE a) = a

theorem MagnitudeConjecture.ObjectDeletion.maximalVanishingQuotientDescend_unique {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) {M E : CategoryTheory.Functor C (ModuleCat k)} (hE : ModuleVanishesOnDeleted C S E) (a : M ⟶ E) (b : maximalVanishingQuotient C S M ⟶ E) (hb : CategoryTheory.CategoryStruct.comp (maximalVanishingQuotientProjection C S M) b = a) : b = maximalVanishingQuotientDescend C S hE a

Descent through the maximal vanishing quotient is unique.

def MagnitudeConjecture.ObjectDeletion.maximalVanishingQuotientMap {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) {M N : CategoryTheory.Functor C (ModuleCat k)} (a : M ⟶ N) : maximalVanishingQuotient C S M ⟶ maximalVanishingQuotient C S N

A morphism of ambient modules descends to their maximal vanishing quotients.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.projection_comp_maximalVanishingQuotientMap {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) {M N : CategoryTheory.Functor C (ModuleCat k)} (a : M ⟶ N) : CategoryTheory.CategoryStruct.comp (maximalVanishingQuotientProjection C S M) (maximalVanishingQuotientMap C S a) = CategoryTheory.CategoryStruct.comp a (maximalVanishingQuotientProjection C S N)

def MagnitudeConjecture.ObjectDeletion.maximalVanishingQuotientFunctor {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) : CategoryTheory.Functor (CategoryTheory.Functor C (ModuleCat k)) (CategoryTheory.Functor C (ModuleCat k))

The maximal-vanishing-quotient construction is functorial on ambient module-valued functors.

def MagnitudeConjecture.ObjectDeletion.maximalVanishingQuotientProjectionNatTrans {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] (S : Set C) : CategoryTheory.Functor.id (CategoryTheory.Functor C (ModuleCat k)) ⟶ maximalVanishingQuotientFunctor C S

The quotient projections form a natural transformation from the identity functor.

def MagnitudeConjecture.ObjectDeletion.linearMaximalVanishingQuotient {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.LinearModuleCategory k) : CoveringHom.LinearModuleCategory k

The maximal vanishing quotient of a linear module, bundled as a linear module.

theorem MagnitudeConjecture.ObjectDeletion.linearMaximalVanishingQuotient_isFiniteDimensional {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) : CoveringHom.IsFiniteDimensionalModule k (linearMaximalVanishingQuotient C S M.obj)

Taking the maximal vanishing quotient preserves pointwise finite dimension and finite object support.

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingQuotient {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) : CoveringHom.FiniteDimensionalModuleCategory k

The maximal vanishing quotient of a finite-dimensional module.

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingQuotientObj {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) : VanishingFiniteModuleCategory C S

The maximal vanishing quotient, bundled in the vanishing full subcategory.

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingQuotientFunctor {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : CategoryTheory.Functor (CoveringHom.FiniteDimensionalModuleCategory k) (VanishingFiniteModuleCategory C S)

The maximal-vanishing-quotient construction as a functor from ambient finite modules to the vanishing full subcategory.

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingQuotientProjection {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) : M ⟶ (finiteModuleVanishesOnDeleted C S).ι.obj ((finiteMaximalVanishingQuotientFunctor C S).obj M)

The ambient finite module projects onto its maximal vanishing quotient.

instance MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingQuotientProjection_epi {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) : CategoryTheory.Epi (finiteMaximalVanishingQuotientProjection C S M)

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingQuotientDescend {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {M : CoveringHom.FiniteDimensionalModuleCategory k} {E : VanishingFiniteModuleCategory C S} (a : M ⟶ E.obj) : (finiteMaximalVanishingQuotientFunctor C S).obj M ⟶ E

A morphism from an ambient finite module to a vanishing finite module descends through the maximal vanishing quotient.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.projection_comp_finiteMaximalVanishingQuotientDescend {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {M : CoveringHom.FiniteDimensionalModuleCategory k} {E : VanishingFiniteModuleCategory C S} (a : M ⟶ E.obj) : CategoryTheory.CategoryStruct.comp (finiteMaximalVanishingQuotientProjection C S M) (finiteMaximalVanishingQuotientDescend C S a).hom = a

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingQuotientHomEquiv {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) (E : VanishingFiniteModuleCategory C S) : ((finiteMaximalVanishingQuotientFunctor C S).obj M ⟶ E) ≃ (M ⟶ (finiteModuleVanishesOnDeleted C S).ι.obj E)

Universal Hom equivalence for the maximal vanishing quotient.

def MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingQuotientAdjunction {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : finiteMaximalVanishingQuotientFunctor C S ⊣ (finiteModuleVanishesOnDeleted C S).ι

The maximal-vanishing-quotient functor is left adjoint to inclusion of the vanishing full subcategory.