Almost-split maps under object deletion

The finite modules vanishing on a set of deleted objects form a reflective and coreflective full subcategory of the ambient finite-module category. This file proves the manuscript's intrinsic source/sink comparison: applying the right adjoint to the source of an ambient sink map produces a right almost-split map in the vanishing subcategory, and applying the left adjoint to the target of an ambient source map produces a left almost-split map there.

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

Restrict an ambient map into a vanishing module to the maximal vanishing submodule of its source.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingSubmoduleRestriction_hom {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Y : CoveringHom.FiniteDimensionalModuleCategory k} {Z : VanishingFiniteModuleCategory C S} (g : Y ⟶ Z.obj) : (finiteMaximalVanishingSubmoduleRestriction C S g).hom = CategoryTheory.CategoryStruct.comp (finiteMaximalVanishingSubmoduleInclusion C S Y) g

theorem MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingSubmoduleRestriction_isRightAlmostSplit {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Y : CoveringHom.FiniteDimensionalModuleCategory k} {Z : VanishingFiniteModuleCategory C S} (g : Y ⟶ Z.obj) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit g) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (finiteMaximalVanishingSubmoduleRestriction C S g)

Restricting an ambient right almost-split map by the right adjoint gives a right almost-split map in the vanishing subcategory.

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

Compose an ambient map out of a vanishing module with the projection to the maximal vanishing quotient of its target.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingQuotientExtension_hom {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Z : VanishingFiniteModuleCategory C S} {Y : CoveringHom.FiniteDimensionalModuleCategory k} (f : Z.obj ⟶ Y) : (finiteMaximalVanishingQuotientExtension C S f).hom = CategoryTheory.CategoryStruct.comp f (finiteMaximalVanishingQuotientProjection C S Y)

theorem MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingQuotientExtension_isLeftAlmostSplit {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Z : VanishingFiniteModuleCategory C S} {Y : CoveringHom.FiniteDimensionalModuleCategory k} (f : Z.obj ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (finiteMaximalVanishingQuotientExtension C S f)

Extending an ambient left almost-split map by the left adjoint gives a left almost-split map in the vanishing subcategory.

noncomputable def MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionByZeroToVanishing {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)

Extension by zero, corestricted to the full subcategory of finite ambient modules vanishing on the deleted objects.

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

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

instance MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionByZeroToVanishing_isEquivalence {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : (finiteDimensionalModuleExtensionByZeroToVanishing C S).IsEquivalence

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

The deletion-stage finite-module category is equivalent to the full vanishing subcategory of ambient finite modules.

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

The explicit deletion-stage module underlying a finite ambient module which vanishes on the deleted objects.

noncomputable def MagnitudeConjecture.ObjectDeletion.finiteVanishingModuleRestrictionExtensionIso {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (M : VanishingFiniteModuleCategory C S) : (finiteDimensionalModuleExtensionByZeroToVanishing C S).obj (finiteVanishingModuleRestriction C S M) ≅ M

Extending the explicit restriction of a vanishing finite module recovers that module inside the vanishing full subcategory.

noncomputable def MagnitudeConjecture.ObjectDeletion.finiteDeletionRightAdjointSinkCandidate {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Y : CoveringHom.FiniteDimensionalModuleCategory k} {Z : CoveringHom.FiniteDimensionalModuleCategory k} (g : Y ⟶ (finiteDimensionalModuleExtensionByZero C S).obj Z) : finiteVanishingModuleRestriction C S ((finiteMaximalVanishingSubmoduleFunctor C S).obj Y) ⟶ Z

The intrinsic deletion-stage sink candidate obtained from an ambient right almost-split map by the maximal-vanishing-submodule construction.

theorem MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionByZero_map_finiteDeletionRightAdjointSinkCandidate {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Y : CoveringHom.FiniteDimensionalModuleCategory k} {Z : CoveringHom.FiniteDimensionalModuleCategory k} (g : Y ⟶ (finiteDimensionalModuleExtensionByZero C S).obj Z) : (finiteDimensionalModuleExtensionByZero C S).map (finiteDeletionRightAdjointSinkCandidate C S g) = CategoryTheory.CategoryStruct.comp (finiteVanishingModuleRestrictionExtensionIso C S ((finiteMaximalVanishingSubmoduleFunctor C S).obj Y)).hom.hom (CategoryTheory.CategoryStruct.comp (finiteMaximalVanishingSubmoduleInclusion C S Y) g)

After extension by zero, the intrinsic deletion-stage sink candidate is the ambient map restricted along the canonical source isomorphism and the maximal-vanishing-submodule inclusion.

theorem MagnitudeConjecture.ObjectDeletion.finiteMaximalVanishingSubmoduleRestriction_arity_eq_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) (Y : CoveringHom.FiniteDimensionalModuleCategory k) (hY : ModuleVanishesOnDeleted C S Y.obj.obj) (dY : CategoryTheory.FiniteIndecomposableDecomposition Y) (dR : CategoryTheory.FiniteIndecomposableDecomposition (finiteVanishingModuleRestriction C S ((finiteMaximalVanishingSubmoduleFunctor C S).obj Y))) : dR.n = dY.n

If an ambient finite module already vanishes on the deleted objects, restricting its maximal vanishing submodule preserves the number of terms in every finite indecomposable decomposition.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletionRightAdjointSinkCandidate_mono_iff_of_source_vanishes {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Y : CoveringHom.FiniteDimensionalModuleCategory k} {Z : CoveringHom.FiniteDimensionalModuleCategory k} (g : Y ⟶ (finiteDimensionalModuleExtensionByZero C S).obj Z) (hY : ModuleVanishesOnDeleted C S Y.obj.obj) : CategoryTheory.Mono (finiteDeletionRightAdjointSinkCandidate C S g) ↔ CategoryTheory.Mono g

If the ambient source vanishes on the deleted objects, the intrinsic deletion-stage sink candidate is monic exactly when the ambient sink is.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletionRightAdjointSinkCandidate_isRightAlmostSplit {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Y : CoveringHom.FiniteDimensionalModuleCategory k} {Z : CoveringHom.FiniteDimensionalModuleCategory k} (g : Y ⟶ (finiteDimensionalModuleExtensionByZero C S).obj Z) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit g) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (finiteDeletionRightAdjointSinkCandidate C S g)

The right-adjoint sink candidate is right almost split in the literal deletion-stage module category.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletionRightAdjointSinkCandidate_isRightMinimal_of_source_vanishes {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Y : CoveringHom.FiniteDimensionalModuleCategory k} {Z : CoveringHom.FiniteDimensionalModuleCategory k} (g : Y ⟶ (finiteDimensionalModuleExtensionByZero C S).obj Z) (hg : QuotientSubmoduleEquidistribution.IsRightMinimal g) (hY : ModuleVanishesOnDeleted C S Y.obj.obj) : QuotientSubmoduleEquidistribution.IsRightMinimal (finiteDeletionRightAdjointSinkCandidate C S g)

If the source of an ambient right-minimal sink already vanishes on the deleted objects, its intrinsic deletion-stage sink candidate remains right minimal.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletion_projective_iff_of_minimal_sink_source_vanishes {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (hP : ∀ (X : C), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)) {Y : CoveringHom.FiniteDimensionalModuleCategory k} {Z : CoveringHom.FiniteDimensionalModuleCategory k} (g : Y ⟶ (finiteDimensionalModuleExtensionByZero C S).obj Z) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit g) (hgmin : QuotientSubmoduleEquidistribution.IsRightMinimal g) (hY : ModuleVanishesOnDeleted C S Y.obj.obj) : CategoryTheory.Projective Z ↔ CategoryTheory.Projective ((finiteDimensionalModuleExtensionByZero C S).obj Z)

If the source of an ambient minimal sink already vanishes on the deleted objects, deleting those objects preserves projectivity of the endpoint.

theorem MagnitudeConjecture.ObjectDeletion.exists_finiteDeletion_rightMinimal_sink_of_ambient {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Y : CoveringHom.FiniteDimensionalModuleCategory k} {Z : CoveringHom.FiniteDimensionalModuleCategory k} (g : Y ⟶ (finiteDimensionalModuleExtensionByZero C S).obj Z) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit g) : ∃ (Y' : CoveringHom.FiniteDimensionalModuleCategory k) (g' : Y' ⟶ Z), QuotientSubmoduleEquidistribution.IsRightAlmostSplit g' ∧ QuotientSubmoduleEquidistribution.IsRightMinimal g'

The deletion-stage sink map is obtained by right-minimalizing the right-adjoint image of an ambient sink map.

theorem MagnitudeConjecture.ObjectDeletion.exists_finiteDeletion_rightMinimal_sink_retract_of_ambient {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Y : CoveringHom.FiniteDimensionalModuleCategory k} {Z : CoveringHom.FiniteDimensionalModuleCategory k} (g : Y ⟶ (finiteDimensionalModuleExtensionByZero C S).obj Z) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit g) : ∃ (Y' : CoveringHom.FiniteDimensionalModuleCategory k) (g' : Y' ⟶ Z) (i : Y' ⟶ finiteVanishingModuleRestriction C S ((finiteMaximalVanishingSubmoduleFunctor C S).obj Y)), QuotientSubmoduleEquidistribution.IsRightAlmostSplit g' ∧ QuotientSubmoduleEquidistribution.IsRightMinimal g' ∧ CategoryTheory.IsSplitMono i ∧ CategoryTheory.CategoryStruct.comp i (finiteDeletionRightAdjointSinkCandidate C S g) = g'

A right-minimal deletion-stage sink has middle term a retract of the right-adjoint sink candidate.

noncomputable def MagnitudeConjecture.ObjectDeletion.finiteDeletionLeftAdjointSourceCandidate {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Z : CoveringHom.FiniteDimensionalModuleCategory k} {Y : CoveringHom.FiniteDimensionalModuleCategory k} (f : (finiteDimensionalModuleExtensionByZero C S).obj Z ⟶ Y) : Z ⟶ finiteVanishingModuleRestriction C S ((finiteMaximalVanishingQuotientFunctor C S).obj Y)

The intrinsic deletion-stage source candidate obtained from an ambient left almost-split map by the maximal-vanishing-quotient construction.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletionLeftAdjointSourceCandidate_isLeftAlmostSplit {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Z : CoveringHom.FiniteDimensionalModuleCategory k} {Y : CoveringHom.FiniteDimensionalModuleCategory k} (f : (finiteDimensionalModuleExtensionByZero C S).obj Z ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (finiteDeletionLeftAdjointSourceCandidate C S f)

The left-adjoint source candidate is left almost split in the literal deletion-stage module category.

theorem MagnitudeConjecture.ObjectDeletion.exists_finiteDeletion_leftMinimal_source_of_ambient {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Z : CoveringHom.FiniteDimensionalModuleCategory k} {Y : CoveringHom.FiniteDimensionalModuleCategory k} (f : (finiteDimensionalModuleExtensionByZero C S).obj Z ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) : ∃ (Y' : CoveringHom.FiniteDimensionalModuleCategory k) (f' : Z ⟶ Y'), QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f' ∧ QuotientSubmoduleEquidistribution.IsLeftMinimal f'

The deletion-stage source map is obtained by left-minimalizing the left-adjoint image of an ambient source map.

theorem MagnitudeConjecture.ObjectDeletion.exists_finiteDeletion_leftMinimal_source_retract_of_ambient {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) {Z : CoveringHom.FiniteDimensionalModuleCategory k} {Y : CoveringHom.FiniteDimensionalModuleCategory k} (f : (finiteDimensionalModuleExtensionByZero C S).obj Z ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) : ∃ (Y' : CoveringHom.FiniteDimensionalModuleCategory k) (f' : Z ⟶ Y') (i : Y' ⟶ finiteVanishingModuleRestriction C S ((finiteMaximalVanishingQuotientFunctor C S).obj Y)), QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f' ∧ QuotientSubmoduleEquidistribution.IsLeftMinimal f' ∧ CategoryTheory.IsSplitMono i ∧ CategoryTheory.CategoryStruct.comp f' i = finiteDeletionLeftAdjointSourceCandidate C S f

A left-minimal deletion-stage source has middle term a retract of the left-adjoint source candidate.