Extending modules across object deletion

A module over C/(S) is viewed in the manuscript as an ambient C-module which vanishes on every deleted object. This file constructs that ambient module. Its value at X is the dependent product over proofs that X survives. Thus it is canonically the original value when X ∉ S, and is a zero object when X ∈ S. Maps between survivors are induced by the deletion quotient, while maps out of a deleted object are zero.

The construction preserves linearity and finite-dimensional finite support. It is the stage-to-ambient bridge used by the common finite control window in the covering average.

@[instance_reducible]

noncomputable def MagnitudeConjecture.ObjectDeletion.deletionMembershipDecidable (C : Type u) (S : Set C) : DecidablePred fun (X : C) => X ∈ S

@[reducible, inline]

abbrev MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroObj {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) (X : C) : ModuleCat k

The value of extension by zero at an ambient object. The indexing proposition is empty precisely at a deleted object.

def MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroObjIso {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) {X : C} (hX : X ∉ S) : moduleExtensionByZeroObj C S M X ≅ M.obj (survivingObj C S hX)

At a surviving object, the dependent-product model of extension by zero is canonically the original module value.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroObjIso_hom_apply {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) {X : C} (hX : X ∉ S) (m : ↑(moduleExtensionByZeroObj C S M X)) : (ModuleCat.Hom.hom (moduleExtensionByZeroObjIso C S M hX).hom) m = m { down := hX }

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroObjIso_inv_apply {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) {X : C} (hX : X ∉ S) (m : ↑(M.obj (survivingObj C S hX))) (h : PLift (X ∉ S)) : (ModuleCat.Hom.hom (moduleExtensionByZeroObjIso C S M hX).inv) m h = m

def MagnitudeConjecture.ObjectDeletion.survivingObjIso {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (X : DeletionCategory C S) : survivingObj C S ⋯ ≅ X

Every object of the deletion category is canonically isomorphic to the surviving object represented by its underlying ambient object.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.survivingObjIso_survivingObj {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {X : C} (hX : X ∉ S) : survivingObjIso C S (survivingObj C S hX) = CategoryTheory.Iso.refl (survivingObj C S ⋯)

def MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroObjIsoAt {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) (X : DeletionCategory C S) : moduleExtensionByZeroObj C S M X.obj.as ≅ M.obj X

The surviving-value identification, expressed at an arbitrary object of the deletion category.

noncomputable def MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroMap {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) {X Y : C} (f : X ⟶ Y) : moduleExtensionByZeroObj C S M X ⟶ moduleExtensionByZeroObj C S M Y

The action of extension by zero on an ambient morphism.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroMap_apply_of_not_mem {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) {X Y : C} (f : X ⟶ Y) (hX : X ∉ S) (m : ↑(moduleExtensionByZeroObj C S M X)) (hY : PLift (Y ∉ S)) : (ModuleCat.Hom.hom (moduleExtensionByZeroMap C S M f)) m hY = (ModuleCat.Hom.hom (M.map (survivingMap C S hX ⋯ f))) (m { down := hX })

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroMap_apply_of_mem {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) {X Y : C} (f : X ⟶ Y) (hX : X ∈ S) (m : ↑(moduleExtensionByZeroObj C S M X)) (hY : PLift (Y ∉ S)) : (ModuleCat.Hom.hom (moduleExtensionByZeroMap C S M f)) m hY = 0

noncomputable def MagnitudeConjecture.ObjectDeletion.moduleExtensionByZero {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) [M.Additive] : CategoryTheory.Functor C (ModuleCat k)

Extension by zero from modules on the object-deletion category to ambient modules.

theorem MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroObjIso_map {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) [M.Additive] {X Y : C} (hX : X ∉ S) (hY : Y ∉ S) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((moduleExtensionByZero C S M).map f) (moduleExtensionByZeroObjIso C S M hY).hom = CategoryTheory.CategoryStruct.comp (moduleExtensionByZeroObjIso C S M hX).hom (M.map (survivingMap C S hX hY f))

Evaluation at surviving objects intertwines the extended action with the original deletion-category action.

theorem MagnitudeConjecture.ObjectDeletion.moduleExtensionByZero_obj_isZero_of_mem {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) [M.Additive] {X : C} (hX : X ∈ S) : CategoryTheory.Limits.IsZero ((moduleExtensionByZero C S M).obj X)

A deleted object has zero value in the extended module.

instance MagnitudeConjecture.ObjectDeletion.moduleExtensionByZero_additive {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) [M.Additive] : (moduleExtensionByZero C S M).Additive

instance MagnitudeConjecture.ObjectDeletion.moduleExtensionByZero_linear {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] : CategoryTheory.Functor.Linear k (moduleExtensionByZero C S M)

def MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroNatTransApp {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {M N : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)} [M.Additive] [N.Additive] (α : M ⟶ N) (X : C) : moduleExtensionByZeroObj C S M X ⟶ moduleExtensionByZeroObj C S N X

The component of extension by zero on a natural transformation.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroNatTransApp_apply {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {M N : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)} [M.Additive] [N.Additive] (α : M ⟶ N) (X : C) (m : ↑(moduleExtensionByZeroObj C S M X)) (hX : PLift (X ∉ S)) : (ModuleCat.Hom.hom (moduleExtensionByZeroNatTransApp C S α X)) m hX = (ModuleCat.Hom.hom (α.app (survivingObj C S ⋯))) (m hX)

def MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroNatTrans {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {M N : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)} [M.Additive] [N.Additive] (α : M ⟶ N) : moduleExtensionByZero C S M ⟶ moduleExtensionByZero C S N

Extension by zero of a natural transformation.

theorem MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroObjIso_naturality {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {M N : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)} [M.Additive] [N.Additive] (α : M ⟶ N) {X : C} (hX : X ∉ S) : CategoryTheory.CategoryStruct.comp ((moduleExtensionByZeroNatTrans C S α).app X) (moduleExtensionByZeroObjIso C S N hX).hom = CategoryTheory.CategoryStruct.comp (moduleExtensionByZeroObjIso C S M hX).hom (α.app (survivingObj C S hX))

Evaluation at a surviving object also intertwines extended natural transformations with their original components.

noncomputable def MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroConjugateApp {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {M N : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)} [M.Additive] [N.Additive] (β : moduleExtensionByZero C S M ⟶ moduleExtensionByZero C S N) {X : C} (hX : X ∉ S) : M.obj (survivingObj C S hX) ⟶ N.obj (survivingObj C S hX)

Conjugating an ambient morphism between two extensions by the surviving evaluation isomorphisms recovers a morphism between the original values.

theorem MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroConjugateApp_naturality {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {M N : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)} [M.Additive] [N.Additive] (β : moduleExtensionByZero C S M ⟶ moduleExtensionByZero C S N) {X Y : C} (hX : X ∉ S) (hY : Y ∉ S) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (M.map (survivingMap C S hX hY f)) (moduleExtensionByZeroConjugateApp C S β hY) = CategoryTheory.CategoryStruct.comp (moduleExtensionByZeroConjugateApp C S β hX) (N.map (survivingMap C S hX hY f))

The conjugated components of an ambient natural transformation are natural for every morphism between surviving ambient objects.

noncomputable def MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroPreimageApp {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {M N : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)} [M.Additive] [N.Additive] (β : moduleExtensionByZero C S M ⟶ moduleExtensionByZero C S N) (X : DeletionCategory C S) : M.obj X ⟶ N.obj X

Restrict an ambient morphism between two extensions back to the deletion category. The object is first moved to its canonical surviving representative, where the ambient component can be conjugated by evaluation, and then moved back.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroPreimageApp_survivingObj {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {M N : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)} [M.Additive] [N.Additive] (β : moduleExtensionByZero C S M ⟶ moduleExtensionByZero C S N) {X : C} (hX : X ∉ S) : moduleExtensionByZeroPreimageApp C S β (survivingObj C S hX) = moduleExtensionByZeroConjugateApp C S β hX

noncomputable def MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroPreimage {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {M N : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)} [M.Additive] [N.Additive] (β : moduleExtensionByZero C S M ⟶ moduleExtensionByZero C S N) : M ⟶ N

Restriction of an ambient morphism between extensions is natural on the object-deletion category.

theorem MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroNatTrans_id {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)) [M.Additive] : moduleExtensionByZeroNatTrans C S (CategoryTheory.CategoryStruct.id M) = CategoryTheory.CategoryStruct.id (moduleExtensionByZero C S M)

theorem MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroNatTrans_comp {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {M N P : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)} [M.Additive] [N.Additive] [P.Additive] (α : M ⟶ N) (β : N ⟶ P) : moduleExtensionByZeroNatTrans C S (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (moduleExtensionByZeroNatTrans C S α) (moduleExtensionByZeroNatTrans C S β)

theorem MagnitudeConjecture.ObjectDeletion.moduleExtensionByZeroNatTrans_add {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {M N : CategoryTheory.Functor (DeletionCategory C S) (ModuleCat k)} [M.Additive] [N.Additive] (α β : M ⟶ N) : moduleExtensionByZeroNatTrans C S (α + β) = moduleExtensionByZeroNatTrans C S α + moduleExtensionByZeroNatTrans C S β

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

Extension by zero restricts to linear modules.

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

instance MagnitudeConjecture.ObjectDeletion.linearModuleExtensionByZero_faithful {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : (linearModuleExtensionByZero C S).Faithful

instance MagnitudeConjecture.ObjectDeletion.linearModuleExtensionByZero_full {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : (linearModuleExtensionByZero C S).Full

theorem MagnitudeConjecture.ObjectDeletion.moduleSupport_moduleExtensionByZero_subset {k : Type w} [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.moduleSupport k (moduleExtensionByZero C S M.obj) ⊆ (fun (X : DeletionCategory C S) => X.obj.as) '' CoveringHom.moduleSupport k M.obj

The support of an extended module is contained in the image of the original support under the surviving-object inclusion.

theorem MagnitudeConjecture.ObjectDeletion.mem_moduleSupport_moduleExtensionByZero_of_mem {k : Type w} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : CoveringHom.LinearModuleCategory k) (X : DeletionCategory C S) (hX : X ∈ CoveringHom.moduleSupport k M.obj) : X.obj.as ∈ CoveringHom.moduleSupport k (moduleExtensionByZero C S M.obj)

A support point of a deletion-stage module remains a support point after extension by zero, at its underlying ambient object.

theorem MagnitudeConjecture.ObjectDeletion.linearModuleExtensionByZero_isFiniteDimensional {k : Type w} [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 : CoveringHom.IsFiniteDimensionalModule k M) : CoveringHom.IsFiniteDimensionalModule k ((linearModuleExtensionByZero C S).obj M)

Extension by zero preserves pointwise finite dimension and finite object support.

noncomputable def MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionByZero {k : Type w} [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) (CoveringHom.FiniteDimensionalModuleCategory k)

Extension by zero restricts to finite-dimensional modules with finite object support.

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

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

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

theorem MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionByZero_indec {k : Type w} [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) : CategoryTheory.Indecomposable ((finiteDimensionalModuleExtensionByZero C S).obj M)

A finite-dimensional indecomposable module remains indecomposable after extension by zero to the ambient category.

theorem MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionByZero_indec_iff {k : Type w} [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.Indecomposable ((finiteDimensionalModuleExtensionByZero C S).obj M) ↔ CategoryTheory.Indecomposable M

Extension by zero identifies indecomposability of finite-dimensional modules on the deletion category with indecomposability of their ambient extensions.