Finite decompositions and objectwise vanishing

These elementary lemmas are shared by the incoming-Hom locality proof and by the older control-window development. They require neither a control window nor a finite quotient.

noncomputable def MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.inclusion {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasBinaryBiproducts D] {X : D} (d : FiniteIndecomposableDecomposition X) (i : Fin d.n) : d.summand i ⟶ X

Inclusion of one displayed indecomposable summand.

noncomputable def MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.projection {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasBinaryBiproducts D] {X : D} (d : FiniteIndecomposableDecomposition X) (i : Fin d.n) : X ⟶ d.summand i

Projection onto one displayed indecomposable summand.

@[simp]

theorem MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.inclusion_projection {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasBinaryBiproducts D] {X : D} (d : FiniteIndecomposableDecomposition X) (i : Fin d.n) : CategoryTheory.CategoryStruct.comp (d.inclusion i) (d.projection i) = CategoryTheory.CategoryStruct.id (d.summand i)

theorem MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.inclusion_comp_ne_zero_of_isRightMinimal {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasBinaryBiproducts D] {X Y : D} (d : FiniteIndecomposableDecomposition X) (i : Fin d.n) (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsRightMinimal f) : CategoryTheory.CategoryStruct.comp (d.inclusion i) f ≠ 0

Every displayed component of a right-minimal map is nonzero.

theorem MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.comp_projection_ne_zero_of_isLeftMinimal {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasBinaryBiproducts D] {X Y : D} (d : FiniteIndecomposableDecomposition Y) (i : Fin d.n) (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsLeftMinimal f) : CategoryTheory.CategoryStruct.comp f (d.projection i) ≠ 0

Every displayed component of a left-minimal map is nonzero.

theorem MagnitudeConjecture.ObjectDeletion.moduleVanishesOnDeleted_compl_of_moduleSupport_subset_frozen {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : CoveringHom.FiniteDimensionalModuleCategory k) (U : Set C) (hU : CoveringHom.moduleSupport k M.obj.obj ⊆ U) : ModuleVanishesOnDeleted C Uᶜ M.obj.obj

A finite-dimensional module vanishes on the complement of any set which contains its object support.

theorem MagnitudeConjecture.ObjectDeletion.moduleVanishesOnDeleted_of_iso {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : Set C) {M N : CoveringHom.FiniteDimensionalModuleCategory k} (e : M ≅ N) (hM : ModuleVanishesOnDeleted C D M.obj.obj) : ModuleVanishesOnDeleted C D N.obj.obj

Vanishing on a deleted set is invariant under isomorphism of finite ambient modules.

theorem MagnitudeConjecture.ObjectDeletion.moduleVanishesOnDeleted_of_decomposition_summands {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) (d : CategoryTheory.FiniteIndecomposableDecomposition Y) (hvanish : ∀ (i : Fin d.n), ModuleVanishesOnDeleted C S (d.summand i).obj.obj) : ModuleVanishesOnDeleted C S Y.obj.obj

If every displayed indecomposable summand of a finite decomposition vanishes on a deleted object set, then so does the decomposed module.