Module-theoretic inheritance under object deletion

Extension by zero embeds finite-dimensional modules on an object-deletion category fully faithfully into the ambient finite-dimensional module category. Its essential image consists exactly of the ambient modules which vanish on the deleted objects, and that vanishing subcategory is a Serre class. This file also formalizes the manuscript's first inheritance consequence: local representation-finiteness passes to every object-deletion category.

For a surviving base object, start from a finite ambient family covering all indecomposables nonzero there. Keep exactly those finitely many indices whose ambient representative occurs in the essential image of extension by zero, and choose one deletion-stage preimage at each retained index. Full faithfulness then reflects the ambient isomorphisms back to the deletion stage.

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

An ambient module vanishes on all objects removed by the deletion.

theorem MagnitudeConjecture.ObjectDeletion.module_isKilledBy_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 : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (hM : ModuleVanishesOnDeleted C S M) : (ideal C S).IsKilledBy M

A module which vanishes on the deleted objects kills the Hom ideal generated by those objects.

def MagnitudeConjecture.ObjectDeletion.moduleRestrictionToDeletion {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)) [M.Additive] [CategoryTheory.Functor.Linear k M] (hM : ModuleVanishesOnDeleted C S M) : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)

Descend an ambient module which vanishes on the deleted objects to the object-deletion category.

instance MagnitudeConjecture.ObjectDeletion.moduleRestrictionToDeletion_additive {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)) [M.Additive] [CategoryTheory.Functor.Linear k M] (hM : ModuleVanishesOnDeleted C S M) : (moduleRestrictionToDeletion C S M hM).Additive

instance MagnitudeConjecture.ObjectDeletion.moduleRestrictionToDeletion_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)) [M.Additive] [CategoryTheory.Functor.Linear k M] (hM : ModuleVanishesOnDeleted C S M) : CategoryTheory.Functor.Linear k (moduleRestrictionToDeletion C S M hM)

noncomputable def MagnitudeConjecture.ObjectDeletion.moduleRestrictionToDeletionIso {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M N : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] [N.Additive] [CategoryTheory.Functor.Linear k N] (hM : ModuleVanishesOnDeleted C S M) (hN : ModuleVanishesOnDeleted C S N) (e : M ≅ N) : moduleRestrictionToDeletion C S M hM ≅ moduleRestrictionToDeletion C S N hN

An isomorphism of ambient vanishing modules descends to an isomorphism of their restrictions to the object-deletion category.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.moduleRestrictionToDeletion_map_survivingMap {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)) [M.Additive] [CategoryTheory.Functor.Linear k M] (hM : ModuleVanishesOnDeleted C S M) {X Y : C} (hX : X ∉ S) (hY : Y ∉ S) (f : X ⟶ Y) : (moduleRestrictionToDeletion C S M hM).map (survivingMap C S hX hY f) = M.map f

noncomputable def MagnitudeConjecture.ObjectDeletion.moduleRestrictionExtensionIsoApp {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)) [M.Additive] [CategoryTheory.Functor.Linear k M] (hM : ModuleVanishesOnDeleted C S M) (X : C) : (moduleExtensionByZero C S (moduleRestrictionToDeletion C S M hM)).obj X ≅ M.obj X

The extension of the descended module is pointwise isomorphic to the original ambient module.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.moduleRestrictionExtensionIsoApp_of_not_mem {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)) [M.Additive] [CategoryTheory.Functor.Linear k M] (hM : ModuleVanishesOnDeleted C S M) {X : C} (hX : X ∉ S) : moduleRestrictionExtensionIsoApp C S M hM X = moduleExtensionByZeroObjIso C S (moduleRestrictionToDeletion C S M hM) hX

noncomputable def MagnitudeConjecture.ObjectDeletion.moduleRestrictionExtensionIso {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)) [M.Additive] [CategoryTheory.Functor.Linear k M] (hM : ModuleVanishesOnDeleted C S M) : moduleExtensionByZero C S (moduleRestrictionToDeletion C S M hM) ≅ M

Extension by zero after descent recovers an ambient module which vanishes on the deleted objects.

def MagnitudeConjecture.ObjectDeletion.linearModuleRestrictionToDeletion {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) (hM : ModuleVanishesOnDeleted C S M.obj) : CoveringHom.LinearModuleCategory k

Descend a linear ambient module which vanishes on the deleted objects.

noncomputable def MagnitudeConjecture.ObjectDeletion.iteratedLinearModuleRestrictionIso {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) (M : CoveringHom.LinearModuleCategory k) (hUnion : ModuleVanishesOnDeleted C (S ∪ T) M.obj) (hS : ModuleVanishesOnDeleted C S M.obj) (hT : ModuleVanishesOnDeleted (DeletionCategory C S) (AdditionalDeleted C S T) (linearModuleRestrictionToDeletion C S M hS).obj) : (iteratedToUnionFunctor C S T).comp (linearModuleRestrictionToDeletion C (S ∪ T) M hUnion).obj ≅ (linearModuleRestrictionToDeletion (DeletionCategory C S) (AdditionalDeleted C S T) (linearModuleRestrictionToDeletion C S M hS) hT).obj

Restricting a vanishing linear module successively along S and T agrees with restricting it once along S ∪ T, after the canonical equivalence between the two deletion categories.

noncomputable def MagnitudeConjecture.ObjectDeletion.deletionEquivalenceOfEq_linearModuleRestrictionIso {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {T : Set C} (hST : S = T) (M : CoveringHom.LinearModuleCategory k) (hS : ModuleVanishesOnDeleted C S M.obj) (hT : ModuleVanishesOnDeleted C T M.obj) : (deletionEquivalenceOfEq C hST).functor.comp (linearModuleRestrictionToDeletion C T M hT).obj ≅ (linearModuleRestrictionToDeletion C S M hS).obj

Restriction is unchanged when the deleted-object set is replaced by an equal set and the deletion category is transported by that equality.

noncomputable def MagnitudeConjecture.ObjectDeletion.iteratedLinearModuleRestrictionIsoOfSubset {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : Set C) (hST : S ⊆ T) (M : CoveringHom.LinearModuleCategory k) (hFull : ModuleVanishesOnDeleted C T M.obj) (hS : ModuleVanishesOnDeleted C S M.obj) (hAdditional : ModuleVanishesOnDeleted (DeletionCategory C S) (AdditionalDeleted C S T) (linearModuleRestrictionToDeletion C S M hS).obj) : have hEq := ⋯; have e := (iteratedDeletionEquivalence C S T).trans (deletionEquivalenceOfEq C hEq); e.functor.comp (linearModuleRestrictionToDeletion C T M hFull).obj ≅ (linearModuleRestrictionToDeletion (DeletionCategory C S) (AdditionalDeleted C S T) (linearModuleRestrictionToDeletion C S M hS) hAdditional).obj

If S ⊆ T, successive restriction along S and the surviving part of T agrees with direct restriction along T.

noncomputable def MagnitudeConjecture.ObjectDeletion.linearModuleRestrictionExtensionIso {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) (hM : ModuleVanishesOnDeleted C S M.obj) : (linearModuleExtensionByZero C S).obj (linearModuleRestrictionToDeletion C S M hM) ≅ M

At the linear-module level, extension by zero after descent is isomorphic to the original vanishing module.

noncomputable def MagnitudeConjecture.ObjectDeletion.linearModuleExtensionRestrictionIso {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) : let F := linearModuleExtensionByZero C S; have hvanish := ⋯; linearModuleRestrictionToDeletion C S (F.obj M) hvanish ≅ M

Restricting the extension by zero of a linear deletion module recovers the original module.

theorem MagnitudeConjecture.ObjectDeletion.linearModuleExtensionByZero_essImage_iff {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) : (linearModuleExtensionByZero C S).essImage M ↔ ModuleVanishesOnDeleted C S M.obj

The essential image of extension by zero consists exactly of the ambient linear modules which vanish on the deleted objects.

theorem MagnitudeConjecture.ObjectDeletion.linearModuleRestrictionToDeletion_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.LinearModuleCategory k) (hvanish : ModuleVanishesOnDeleted C S M.obj) (hfinite : CoveringHom.IsFiniteDimensionalModule k M) : CoveringHom.IsFiniteDimensionalModule k (linearModuleRestrictionToDeletion C S M hvanish)

Restriction of a vanishing module preserves pointwise finite dimension and finite object support.

def MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleRestrictionToDeletion {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) : CoveringHom.FiniteDimensionalModuleCategory k

Descend a finite-dimensional ambient module which vanishes on the deleted objects.

noncomputable def MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleRestrictionExtensionIso {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) : (finiteDimensionalModuleExtensionByZero C S).obj (finiteDimensionalModuleRestrictionToDeletion C S M hM) ≅ M

At the finite-dimensional-module level, extension by zero after descent is isomorphic to the original vanishing module.

noncomputable def MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionRestrictionIso {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) : finiteDimensionalModuleRestrictionToDeletion C S ((finiteDimensionalModuleExtensionByZero C S).obj M) ⋯ ≅ M

theorem MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleRestrictionToDeletion_indec {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 : CategoryTheory.Indecomposable M) (hvanish : ModuleVanishesOnDeleted C S M.obj.obj) : CategoryTheory.Indecomposable (finiteDimensionalModuleRestrictionToDeletion C S M hvanish)

Restriction to the deletion category preserves indecomposability for an ambient finite module which vanishes on the deleted objects.

theorem MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionByZero_essImage_iff {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) : (finiteDimensionalModuleExtensionByZero C S).essImage M ↔ ModuleVanishesOnDeleted C S M.obj.obj

The essential image of extension by zero consists exactly of the ambient finite-dimensional modules which vanish on the deleted objects.

def MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleEvaluation {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : CategoryTheory.Functor (CoveringHom.FiniteDimensionalModuleCategory k) (ModuleCat k)

Evaluation of a finite-dimensional linear module at an object of the base category.

theorem MagnitudeConjecture.ObjectDeletion.instPreservesLimitFiniteDimensionalModuleCategoryLinearModuleCategoryWalkingParallelPairParallelPairOfNatHomFiniteModuleInclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : CoveringHom.FiniteDimensionalModuleCategory k} (f : M ⟶ N) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) (MagnitudeConjecture.ObjectDeletion.finiteModuleInclusion✝ C)

theorem MagnitudeConjecture.ObjectDeletion.instPreservesColimitFiniteDimensionalModuleCategoryLinearModuleCategoryWalkingParallelPairParallelPairOfNatHomFiniteModuleInclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : CoveringHom.FiniteDimensionalModuleCategory k} (f : M ⟶ N) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) (MagnitudeConjecture.ObjectDeletion.finiteModuleInclusion✝ C)

theorem MagnitudeConjecture.ObjectDeletion.instPreservesLimitLinearModuleCategoryFunctorModuleCatWalkingParallelPairParallelPairOfNatHomLinearModuleInclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : CoveringHom.LinearModuleCategory k} (f : M ⟶ N) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) (MagnitudeConjecture.ObjectDeletion.linearModuleInclusion✝ C)

theorem MagnitudeConjecture.ObjectDeletion.instPreservesColimitLinearModuleCategoryFunctorModuleCatWalkingParallelPairParallelPairOfNatHomLinearModuleInclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : CoveringHom.LinearModuleCategory k} (f : M ⟶ N) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) (MagnitudeConjecture.ObjectDeletion.linearModuleInclusion✝ C)

theorem MagnitudeConjecture.ObjectDeletion.instPreservesFiniteLimitsFullSubcategoryLinearModuleCategoryIsFiniteDimensionalModuleFiniteModuleInclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Limits.PreservesFiniteLimits (MagnitudeConjecture.ObjectDeletion.finiteModuleInclusion✝ C)

theorem MagnitudeConjecture.ObjectDeletion.instPreservesFiniteColimitsFullSubcategoryLinearModuleCategoryIsFiniteDimensionalModuleFiniteModuleInclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Limits.PreservesFiniteColimits (MagnitudeConjecture.ObjectDeletion.finiteModuleInclusion✝ C)

theorem MagnitudeConjecture.ObjectDeletion.instPreservesFiniteLimitsFullSubcategoryFunctorModuleCatIsLinearModuleLinearModuleInclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Limits.PreservesFiniteLimits (MagnitudeConjecture.ObjectDeletion.linearModuleInclusion✝ C)

theorem MagnitudeConjecture.ObjectDeletion.instPreservesFiniteColimitsFullSubcategoryFunctorModuleCatIsLinearModuleLinearModuleInclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Limits.PreservesFiniteColimits (MagnitudeConjecture.ObjectDeletion.linearModuleInclusion✝ C)

theorem MagnitudeConjecture.ObjectDeletion.instPreservesFiniteLimitsFullSubcategoryLinearModuleCategoryIsFiniteDimensionalModuleFunctorModuleCatCompFiniteModuleInclusionLinearModuleInclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Limits.PreservesFiniteLimits ((MagnitudeConjecture.ObjectDeletion.finiteModuleInclusion✝ C).comp (MagnitudeConjecture.ObjectDeletion.linearModuleInclusion✝ C))

theorem MagnitudeConjecture.ObjectDeletion.instPreservesFiniteColimitsFullSubcategoryLinearModuleCategoryIsFiniteDimensionalModuleFunctorModuleCatCompFiniteModuleInclusionLinearModuleInclusion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Limits.PreservesFiniteColimits ((MagnitudeConjecture.ObjectDeletion.finiteModuleInclusion✝ C).comp (MagnitudeConjecture.ObjectDeletion.linearModuleInclusion✝ C))

theorem MagnitudeConjecture.ObjectDeletion.instPreservesFiniteLimitsFullSubcategoryLinearModuleCategoryIsFiniteDimensionalModuleModuleCatCompFiniteModuleInclusionFunctorLinearModuleInclusionObjEvaluation {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : CategoryTheory.Limits.PreservesFiniteLimits ((MagnitudeConjecture.ObjectDeletion.finiteModuleInclusion✝ C).comp ((MagnitudeConjecture.ObjectDeletion.linearModuleInclusion✝ C).comp ((CategoryTheory.evaluation C (ModuleCat k)).obj X)))

theorem MagnitudeConjecture.ObjectDeletion.instPreservesFiniteColimitsFullSubcategoryLinearModuleCategoryIsFiniteDimensionalModuleModuleCatCompFiniteModuleInclusionFunctorLinearModuleInclusionObjEvaluation {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : CategoryTheory.Limits.PreservesFiniteColimits ((MagnitudeConjecture.ObjectDeletion.finiteModuleInclusion✝ C).comp ((MagnitudeConjecture.ObjectDeletion.linearModuleInclusion✝ C).comp ((CategoryTheory.evaluation C (ModuleCat k)).obj X)))

instance MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleEvaluation_preservesFiniteLimits {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : CategoryTheory.Limits.PreservesFiniteLimits (finiteDimensionalModuleEvaluation C X)

instance MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleEvaluation_preservesFiniteColimits {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : CategoryTheory.Limits.PreservesFiniteColimits (finiteDimensionalModuleEvaluation C X)

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

The ambient finite-dimensional modules which vanish on every deleted object.

instance MagnitudeConjecture.ObjectDeletion.finiteModuleVanishesOnDeleted_isSerreClass {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).IsSerreClass

Modules vanishing on the deleted objects are closed under subobjects, quotients, and extensions inside the ambient finite-dimensional module category.

theorem MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionByZero_essImage_eq {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : (finiteDimensionalModuleExtensionByZero C S).essImage = finiteModuleVanishesOnDeleted C S

The essential image of finite-dimensional extension by zero is the vanishing Serre class, as an equality of object properties.

instance MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionByZero_essImage_isSerreClass {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : (finiteDimensionalModuleExtensionByZero C S).essImage.IsSerreClass

The essential image of finite-dimensional extension by zero is closed under subobjects, quotients, and extensions.

theorem MagnitudeConjecture.ObjectDeletion.isLocallyRepresentationFinite_deletion {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (hlocal : CoveringHom.IsLocallyRepresentationFinite) : CoveringHom.IsLocallyRepresentationFinite

Local representation-finiteness of finite-support modules passes from an ambient category to any object-deletion category.