Ambient multiplicity data for a primitive deletion

The frozen manuscript uses one natural-valued function d_X = [X:E] on all ambient indecomposable modules. Its zero set is the killed subcategory, and the projective cover and injective envelope identify it with both ambient Hom dimensions. This file proves that those ambient identities descend across the literal factor and supply PrimitiveTraceInput automatically.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorFunctor_map_injective_from {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} {p : S.SurvivingLabel K} (hvanish : S.NoMapsFromKilled K p) (x : S.SurvivingLabel K) : Function.Injective (S.factorFunctor K).map

Source-to-killed vanishing makes the quotient functor injective on every ambient Hom space from the distinguished source.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorFunctor_map_injective_from_object {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} {p : S.SurvivingLabel K} (hvanish : S.NoMapsFromKilled K p) (X : S.SelectedAddCategory Set.univ) : Function.Injective (S.factorFunctor K).map

Source-to-killed vanishing makes the quotient functor injective from the distinguished source to every object of the ambient additive closure.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorFunctor_map_injective_to {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} {i : S.SurvivingLabel K} (hvanish : S.NoMapsToKilled K i) (x : S.SurvivingLabel K) : Function.Injective (S.factorFunctor K).map

Killed-to-sink vanishing makes the quotient functor injective on every ambient Hom space into the distinguished sink.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorFunctor_map_injective_to_object {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} {i : S.SurvivingLabel K} (hvanish : S.NoMapsToKilled K i) (X : S.SelectedAddCategory Set.univ) : Function.Injective (S.factorFunctor K).map

Killed-to-sink vanishing makes the quotient functor injective from every object of the ambient additive closure to the distinguished sink.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorHomFromSelectedLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} {p : S.SurvivingLabel K} (hvanish : S.NoMapsFromKilled K p) (x : S.SurvivingLabel K) : (S.ambientAddPoint ↑p ⟶ S.ambientAddPoint ↑x) ≃ₗ[k] S.factorObject K p ⟶ S.factorObject K x

The quotient functor identifies the selected ambient source Hom space with the corresponding factor Hom space.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorHomFromSelectedObjectLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} {p : S.SurvivingLabel K} (hvanish : S.NoMapsFromKilled K p) (X : S.SelectedAddCategory Set.univ) : (S.ambientAddPoint ↑p ⟶ X) ≃ₗ[k] S.factorObject K p ⟶ (S.factorFunctor K).obj X

The quotient functor identifies Hom from the selected ambient source to an arbitrary object of the ambient additive closure.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorHomToSelectedLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} {i : S.SurvivingLabel K} (hvanish : S.NoMapsToKilled K i) (x : S.SurvivingLabel K) : (S.ambientAddPoint ↑x ⟶ S.ambientAddPoint ↑i) ≃ₗ[k] S.factorObject K x ⟶ S.factorObject K i

The quotient functor identifies the selected ambient sink Hom space with the corresponding factor Hom space.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorHomToSelectedObjectLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} {i : S.SurvivingLabel K} (hvanish : S.NoMapsToKilled K i) (X : S.SelectedAddCategory Set.univ) : (X ⟶ S.ambientAddPoint ↑i) ≃ₗ[k] (S.factorFunctor K).obj X ⟶ S.factorObject K i

The quotient functor identifies Hom from an arbitrary object of the ambient additive closure to the selected ambient sink.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorHomFromLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} {p : S.SurvivingLabel K} (hvanish : S.NoMapsFromKilled K p) (x : S.SurvivingLabel K) : (S.fgObj ↑p ⟶ S.fgObj ↑x) ≃ₗ[k] S.factorObject K p ⟶ S.factorObject K x

Ambient finitely generated source Hom is linearly equivalent to factor Hom.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorHomFromFGObjLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} {p : S.SurvivingLabel K} (hvanish : S.NoMapsFromKilled K p) (X : FinitelyGeneratedCategory A) : (S.fgObj ↑p ⟶ X) ≃ₗ[k] S.factorObject K p ⟶ (S.factorModuleFunctor K).obj X

Ambient finitely generated Hom from the selected source is linearly equivalent to factor Hom for an arbitrary finitely generated target.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorHomToLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} {i : S.SurvivingLabel K} (hvanish : S.NoMapsToKilled K i) (x : S.SurvivingLabel K) : (S.fgObj ↑x ⟶ S.fgObj ↑i) ≃ₗ[k] S.factorObject K x ⟶ S.factorObject K i

Ambient finitely generated sink Hom is linearly equivalent to factor Hom.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorHomToFGObjLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} {i : S.SurvivingLabel K} (hvanish : S.NoMapsToKilled K i) (X : FinitelyGeneratedCategory A) : (X ⟶ S.fgObj ↑i) ≃ₗ[k] (S.factorModuleFunctor K).obj X ⟶ S.factorObject K i

Ambient finitely generated Hom to the selected sink is linearly equivalent to factor Hom for an arbitrary finitely generated source.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : Type

Exact ambient multiplicity data supplied by the projective cover and injective envelope of the deleted simple.

• source : S.SurvivingLabel K
• sink : S.SurvivingLabel K
• source_projective : CategoryTheory.Projective (S.fgObj ↑self.source)
• sink_injective : CategoryTheory.Injective (S.fgObj ↑self.sink)
• multiplicity : Fin S.n → ℕ
• killed_iff_multiplicity_zero (x : Fin S.n) : x ∈ K ↔ self.multiplicity x = 0
• multiplicity_eq_sourceHom (x : Fin S.n) : self.multiplicity x = Module.finrank k (S.fgObj ↑self.source ⟶ S.fgObj x)
• multiplicity_eq_sinkHom (x : Fin S.n) : self.multiplicity x = Module.finrank k (S.fgObj x ⟶ S.fgObj ↑self.sink)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.killed_iff_sourceHomZero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) (x : Fin S.n) : x ∈ K ↔ ∀ (f : S.fgObj ↑D.source ⟶ S.fgObj x), f = 0

The ambient source Hom identity characterizes exactly the killed labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.killed_iff_sinkHomZero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) (x : Fin S.n) : x ∈ K ↔ ∀ (f : S.fgObj x ⟶ S.fgObj ↑D.sink), f = 0

The ambient sink Hom identity characterizes exactly the killed labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.noMapsFromKilled {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) : S.NoMapsFromKilled K D.source

The ambient multiplicity zero set gives source-to-killed vanishing.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.noMapsToKilled {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) : S.NoMapsToKilled K D.sink

The ambient multiplicity zero set gives killed-to-sink vanishing.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.multiplicity_pos {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) (x : S.SurvivingLabel K) : 0 < D.multiplicity ↑x

The ambient multiplicity is strictly positive on every surviving label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.weight_eq_from {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) (x : S.SurvivingLabel K) : ↑(D.multiplicity ↑x) = FiniteTauMatrix.homFromWeight (S.factorFiniteTauCategoryData K) D.source x

The ambient source multiplicity identity descends to the factor Hom row.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.weight_eq_to {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) (x : S.SurvivingLabel K) : ↑(D.multiplicity ↑x) = FiniteTauMatrix.homToWeight (S.factorFiniteTauCategoryData K) D.sink x

The ambient sink multiplicity identity descends to the factor Hom column.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.toPrimitiveTraceInput {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) : S.PrimitiveTraceInput K

Ambient multiplicity data supplies the complete trace-form primitive input.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.rightMesh_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) (x : S.SurvivingLabel K) : CategoryTheory.Mono ((S.factorFiniteTauCategoryData K).rightMesh ((S.factorFiniteTauCategoryData K).obj x)).f

Ambient multiplicity data gives strict factor meshes.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.leftMesh_epi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) (x : S.SurvivingLabel K) : CategoryTheory.Epi ((S.factorFiniteTauCategoryData K).leftMesh ((S.factorFiniteTauCategoryData K).obj x)).g

Ambient multiplicity data gives strict factor left meshes.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.homMeshInverseData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) : FiniteTauMatrix.HomMeshInverseData (S.factorFiniteTauCategoryData K)

Over an algebraically closed field, ambient multiplicity data supplies the complete Hom--mesh inverse package for the factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.meshUnitEquations {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) : (∀ (target : S.SurvivingLabel K), FiniteTauMatrix.meshColumnWeight (S.factorFiniteTauCategoryData K) (fun (x : S.SurvivingLabel K) => ↑(D.multiplicity ↑x)) target = if target = D.source then 1 else 0) ∧ ∀ (source : S.SurvivingLabel K), FiniteTauMatrix.meshRowWeight (S.factorFiniteTauCategoryData K) (fun (x : S.SurvivingLabel K) => ↑(D.multiplicity ↑x)) source = if source = D.sink then 1 else 0

Ambient multiplicity data gives both factor mesh unit equations.