Trace criteria for primitive-deletion factors

The frozen manuscript proves faithfulness of the distinguished factor representable by a trace argument: a morphism killed by every map from the projective cover factors through the killed module subcategory. This file isolates that ambient factorization statement and proves that it supplies the faithfulness hypotheses used by PrimitiveFactorInput. The dual statement uses the distinguished injective sink.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SourceTraceFactorization {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) : Prop

The paper's source-trace factorization statement: an ambient morphism annihilated after precomposition by every map from the distinguished source factors through the killed additive subcategory.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SinkRejectFactorization {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) : Prop

The dual sink-reject factorization statement: an ambient morphism annihilated after postcomposition by every map to the distinguished sink factors through the killed additive subcategory.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sourceTraceSubmodule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (X : FinitelyGeneratedCategory A) : Submodule Aᵐᵒᵖ ↑X

The singleton trace of the distinguished source in a finitely generated ambient module.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sourceTraceQuotient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (X : FinitelyGeneratedCategory A) : FinitelyGeneratedCategory A

The ambient module quotient by the singleton source trace.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sourceTraceQuotientMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (X : FinitelyGeneratedCategory A) : X ⟶ S.sourceTraceQuotient p X

The canonical map to the quotient by the singleton source trace.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sinkRejectObject {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) (Y : FinitelyGeneratedCategory A) : FinitelyGeneratedCategory A

The singleton reject of the distinguished sink, regarded as a finitely generated ambient submodule.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sinkRejectInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) (Y : FinitelyGeneratedCategory A) : S.sinkRejectObject i Y ⟶ Y

The canonical inclusion of the singleton sink reject.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sourceTraceSubmodule_le_ker {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) (hzero : ∀ (a : S.almostSplitSkeleton.obj p ⟶ X), CategoryTheory.CategoryStruct.comp a f = 0) : S.sourceTraceSubmodule p X ≤ (ModuleCat.Hom.hom f.hom).ker

If every map from p becomes zero after postcomposition by f, then the singleton source trace is contained in the kernel of f.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.range_le_sinkReject {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) (hzero : ∀ (a : Y ⟶ S.almostSplitSkeleton.obj i), CategoryTheory.CategoryStruct.comp f a = 0) : (ModuleCat.Hom.hom f.hom).range ≤ S.almostSplitSkeleton.reject {i} Y

If every map to i becomes zero after precomposition by f, then the range of f lies in the singleton sink reject.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SourceTraceQuotientsKilled {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) : Prop

Every singleton source-trace quotient belongs to the killed additive subcategory. This is the module-theoretic content needed in the paper's trace proof.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SinkRejectsKilled {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) : Prop

Every singleton sink reject belongs to the killed additive subcategory. This is the dual module-theoretic content of the paper's trace proof.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sourceHomKilledLabels {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) : Set (Fin S.n)

Labels on which the distinguished source representable vanishes.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sinkHomKilledLabels {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : Set (Fin S.n)

Labels on which the distinguished sink corepresentable vanishes.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.inAdd_sourceHomKilledLabels_of_noMaps {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (M : FinitelyGeneratedCategory A) (hzero : ∀ (f : S.fgObj p ⟶ M), f = 0) : S.almostSplitSkeleton.InAdd (S.sourceHomKilledLabels p) M

If a module receives no nonzero map from the distinguished source, all of its indecomposable summands have source-vanishing labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.inAdd_sinkHomKilledLabels_of_noMaps {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) (M : FinitelyGeneratedCategory A) (hzero : ∀ (f : M ⟶ S.fgObj i), f = 0) : S.almostSplitSkeleton.InAdd (S.sinkHomKilledLabels i) M

If a module has no nonzero map to the distinguished sink, all of its indecomposable summands have sink-vanishing labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sourceTraceQuotient_noMaps_of_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) (X : FinitelyGeneratedCategory A) (f : S.fgObj p ⟶ S.sourceTraceQuotient p X) : f = 0

The quotient by the singleton source trace receives no nonzero map from that source when the source is projective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sourceTraceQuotientsKilled_of_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) (X : FinitelyGeneratedCategory A) : S.almostSplitSkeleton.InAdd (S.sourceHomKilledLabels p) (S.sourceTraceQuotient p X)

Projectivity makes every singleton source-trace quotient an object of the source-Hom-vanishing additive subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sinkReject_le_ker {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) (Y : FinitelyGeneratedCategory A) (f : Y ⟶ S.fgObj i) : S.almostSplitSkeleton.reject {i} Y ≤ (ModuleCat.Hom.hom f.hom).ker

The singleton sink reject is contained in the kernel of every map to the distinguished sink.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sinkRejectObject_noMaps_of_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) (hi : CategoryTheory.Injective (S.fgObj i)) (Y : FinitelyGeneratedCategory A) (f : S.sinkRejectObject i Y ⟶ S.fgObj i) : f = 0

The singleton sink reject has no nonzero maps to an injective distinguished sink.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sinkRejectsKilled_of_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) (hi : CategoryTheory.Injective (S.fgObj i)) (Y : FinitelyGeneratedCategory A) : S.almostSplitSkeleton.InAdd (S.sinkHomKilledLabels i) (S.sinkRejectObject i Y)

Injectivity makes every singleton sink reject an object of the sink-Hom-vanishing additive subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sourceTraceFactorization_of_quotientsKilled {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} (hkilled : S.SourceTraceQuotientsKilled K p) : S.SourceTraceFactorization K p

Killed singleton trace quotients give the source-trace factorization criterion used to prove quotient faithfulness.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sinkRejectFactorization_of_rejectsKilled {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} (hkilled : S.SinkRejectsKilled K i) : S.SinkRejectFactorization K i

Killed singleton sink rejects give the dual reject-factorization criterion used to prove quotient corepresentable faithfulness.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableFaithful_of_sourceTrace {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) (htrace : S.SourceTraceFactorization K p) : S.FactorRepresentableFaithful K p

Source-to-killed vanishing upgrades the ambient trace-factorization criterion to faithfulness of the represented Hom functor on the factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableFaithful_of_sinkReject {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) (hreject : S.SinkRejectFactorization K i) : S.FactorCorepresentableFaithful K i

Killed-to-sink vanishing upgrades the ambient reject-factorization criterion to faithfulness of the corepresented Hom functor on the factor.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveTraceInput {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)) : Type

Primitive-factor data phrased with the manuscript's concrete trace quotients and reject submodules rather than quotient faithfulness assumptions.

• source : S.SurvivingLabel K
• sink : S.SurvivingLabel K
• source_projective : CategoryTheory.Projective (S.fgObj ↑self.source)
• sink_injective : CategoryTheory.Injective (S.fgObj ↑self.sink)
• killed_iff_sourceHomZero (x : Fin S.n) : x ∈ K ↔ ∀ (f : S.fgObj ↑self.source ⟶ S.fgObj x), f = 0
• killed_iff_sinkHomZero (x : Fin S.n) : x ∈ K ↔ ∀ (f : S.fgObj x ⟶ S.fgObj ↑self.sink), f = 0
• weight : S.SurvivingLabel K → ℤ
• weight_pos (x : S.SurvivingLabel K) : 0 < self.weight x
• weight_eq_from (x : S.SurvivingLabel K) : self.weight x = FiniteTauMatrix.homFromWeight (S.factorFiniteTauCategoryData K) self.source x
• weight_eq_to (x : S.SurvivingLabel K) : self.weight x = FiniteTauMatrix.homToWeight (S.factorFiniteTauCategoryData K) self.sink x

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveTraceInput.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.PrimitiveTraceInput K) : S.NoMapsFromKilled K D.source

The source Hom-vanishing characterization immediately gives the source-to-killed vanishing used in the factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveTraceInput.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.PrimitiveTraceInput K) : S.NoMapsToKilled K D.sink

The sink Hom-vanishing characterization immediately gives the killed-to-sink vanishing used in the factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveTraceInput.sourceTraceQuotientsKilled {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.PrimitiveTraceInput K) : S.SourceTraceQuotientsKilled K D.source

Projectivity and the exact source Hom-vanishing characterization put every singleton trace quotient in the killed additive subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveTraceInput.sinkRejectsKilled {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.PrimitiveTraceInput K) : S.SinkRejectsKilled K D.sink

Injectivity and the exact sink Hom-vanishing characterization put every singleton reject in the killed additive subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveTraceInput.sourceTraceFactorization {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.PrimitiveTraceInput K) : S.SourceTraceFactorization K D.source

The concrete killed trace quotients supply the paper's ambient source factorization statement.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveTraceInput.sinkRejectFactorization {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.PrimitiveTraceInput K) : S.SinkRejectFactorization K D.sink

The concrete killed-reject field supplies the dual ambient factorization statement.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveTraceInput.toPrimitiveFactorInput {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.PrimitiveTraceInput K) : S.PrimitiveFactorInput K

The trace-form primitive input supplies the quotient-faithfulness form used by the strict factor and unit-equation theorems.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveTraceInput.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.PrimitiveTraceInput K) (x : S.SurvivingLabel K) : CategoryTheory.Mono ((S.factorFiniteTauCategoryData K).rightMesh ((S.factorFiniteTauCategoryData K).obj x)).f

The manuscript's source trace statement makes all factor right meshes strict.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveTraceInput.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.PrimitiveTraceInput K) (x : S.SurvivingLabel K) : CategoryTheory.Epi ((S.factorFiniteTauCategoryData K).leftMesh ((S.factorFiniteTauCategoryData K).obj x)).g

The dual sink reject statement makes all factor left meshes strict.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveTraceInput.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.PrimitiveTraceInput K) : FiniteTauMatrix.HomMeshInverseData (S.factorFiniteTauCategoryData K)

Over an algebraically closed field, trace-form primitive data supplies the complete Hom--mesh inverse package.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveTraceInput.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.PrimitiveTraceInput K) : (∀ (target : S.SurvivingLabel K), FiniteTauMatrix.meshColumnWeight (S.factorFiniteTauCategoryData K) D.weight target = if target = D.source then 1 else 0) ∧ ∀ (source : S.SurvivingLabel K), FiniteTauMatrix.meshRowWeight (S.factorFiniteTauCategoryData K) D.weight source = if source = D.sink then 1 else 0

Trace-form primitive data satisfies both mesh unit equations.