Finite-skeleton local change under object deletion

For complete finite indecomposable skeletons before and after deletion, extension by zero identifies the post-deletion labels with exactly the ambient labels which vanish on the deleted objects. Consequently the sum of the intrinsic pointwise deletion changes is the difference of the two Auslander--Reiten surpluses.

@[reducible, inline]

abbrev MagnitudeConjecture.ObjectDeletion.FiniteDeletionSkeleton.SurvivingLabel {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) (S : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) : Type

Labels of the ambient skeleton represented by modules which survive the deletion.

noncomputable def MagnitudeConjecture.ObjectDeletion.FiniteDeletionSkeleton.restrictionSkeleton {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) (S : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton

The complete post-deletion skeleton obtained by keeping exactly the ambient indecomposable representatives which vanish on the deleted objects and restricting them to the deletion category.

noncomputable def MagnitudeConjecture.ObjectDeletion.FiniteDeletionSkeleton.survivingRelabel {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) (S : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (T : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (j : Fin T.n) : Fin S.n

The ambient skeleton label representing extension by zero of a post-deletion skeleton object.

noncomputable def MagnitudeConjecture.ObjectDeletion.FiniteDeletionSkeleton.survivingRelabelIso {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) (S : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (T : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (j : Fin T.n) : (finiteDimensionalModuleExtensionByZero C D).obj (T.obj j) ≅ S.obj (survivingRelabel D S T j)

The chosen isomorphism underlying the surviving relabelling.

theorem MagnitudeConjecture.ObjectDeletion.FiniteDeletionSkeleton.survivingRelabel_vanishes {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) (S : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (T : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (j : Fin T.n) : ModuleVanishesOnDeleted C D (S.obj (survivingRelabel D S T j)).obj.obj

Extension by zero lands in the vanishing part of the ambient skeleton.

noncomputable def MagnitudeConjecture.ObjectDeletion.FiniteDeletionSkeleton.survivingRelabelSubtype {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) (S : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (T : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (j : Fin T.n) : SurvivingLabel D S

Surviving relabelling with its vanishing certificate.

theorem MagnitudeConjecture.ObjectDeletion.FiniteDeletionSkeleton.survivingRelabelSubtype_injective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) (S : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (T : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) : Function.Injective (survivingRelabelSubtype D S T)

theorem MagnitudeConjecture.ObjectDeletion.FiniteDeletionSkeleton.survivingRelabelSubtype_surjective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) (S : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (T : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) : Function.Surjective (survivingRelabelSubtype D S T)

noncomputable def MagnitudeConjecture.ObjectDeletion.FiniteDeletionSkeleton.survivingRelabelEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) (S : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (T : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) : Fin T.n ≃ SurvivingLabel D S

Post-deletion labels are equivalent to the vanishing labels of the ambient skeleton.

theorem MagnitudeConjecture.ObjectDeletion.FiniteDeletionSkeleton.finiteDeletionExtendedLocalDensity_survivingRelabel {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) (S : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (T : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (hlocal : CoveringHom.IsLocallyRepresentationFinite) (j : Fin T.n) : finiteDeletionExtendedLocalDensity C hlocal D (S.obj (survivingRelabel D S T j)) ⋯ = CoveringHom.finiteModuleLocalDensity ⋯ (T.obj j) ⋯

At corresponding labels, deletion-extended ambient density is the intrinsic density of the post-deletion skeleton object.

theorem MagnitudeConjecture.ObjectDeletion.FiniteDeletionSkeleton.sum_finiteDeletionExtendedLocalDensity_eq {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) (S : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (T : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (hlocal : CoveringHom.IsLocallyRepresentationFinite) : ∑ i : Fin S.n, finiteDeletionExtendedLocalDensity C hlocal D (S.obj i) ⋯ = ∑ j : Fin T.n, CoveringHom.finiteModuleLocalDensity ⋯ (T.obj j) ⋯

Summing the extended density over the ambient skeleton gives the total intrinsic density of the post-deletion skeleton.

theorem MagnitudeConjecture.ObjectDeletion.FiniteDeletionSkeleton.sum_finiteDeletionLocalChangeAt_eq_surplus_sub {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) (S : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) (T : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (CoveringHom.FiniteDimensionalModuleCategory k)] [CategoryTheory.EnoughProjectives (CoveringHom.FiniteDimensionalModuleCategory k)] (hlocal : CoveringHom.IsLocallyRepresentationFinite) : ∑ i : Fin S.n, finiteDeletionLocalChangeAt C hlocal D (S.obj i) ⋯ = ARCount.surplus (FiniteTauMatrix.arrowMultiplicity S.toFiniteRightTauCategoryData) S.toFiniteRightTauCategoryData.IsProjective - ARCount.surplus (FiniteTauMatrix.arrowMultiplicity T.toFiniteRightTauCategoryData) T.toFiniteRightTauCategoryData.IsProjective

The finite sum of intrinsic pointwise deletion changes is exactly the difference of the before and after Auslander--Reiten surpluses.

theorem MagnitudeConjecture.ObjectDeletion.FiniteDeletionSkeleton.sum_finiteDeletionLocalChangeAt_eq_restrictionSkeleton_surplus_sub {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) (S : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (CoveringHom.FiniteDimensionalModuleCategory k)] [CategoryTheory.EnoughProjectives (CoveringHom.FiniteDimensionalModuleCategory k)] (hlocal : CoveringHom.IsLocallyRepresentationFinite) : ∑ i : Fin S.n, finiteDeletionLocalChangeAt C hlocal D (S.obj i) ⋯ = ARCount.surplus (FiniteTauMatrix.arrowMultiplicity S.toFiniteRightTauCategoryData) S.toFiniteRightTauCategoryData.IsProjective - ARCount.surplus (FiniteTauMatrix.arrowMultiplicity (restrictionSkeleton D S).toFiniteRightTauCategoryData) (restrictionSkeleton D S).toFiniteRightTauCategoryData.IsProjective

The deletion difference may be stated using the canonical restriction skeleton obtained directly from the ambient complete skeleton.