Strictness criteria for literal finite-module factors

The primitive deletion in the frozen manuscript has a distinguished projective source P whose covariant representable functor on the factor is faithful and which has no maps to killed modules. This file isolates the exact categorical consequences of those two facts: quotient images of ambient monomorphisms remain monic, and hence all chosen factor right meshes are strict. The dual criterion treats a distinguished injective sink.

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

A selected source label has no nonzero maps to any killed selected indecomposable.

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

A selected sink label receives no nonzero maps from any killed selected indecomposable.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.FactorRepresentableFaithful {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

Covariant representability by a selected factor object is faithful.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.FactorCorepresentableFaithful {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

Contravariant representability by a selected factor object is faithful.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.hom_eq_zero_of_inAdd_of_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)} {p : S.SurvivingLabel K} (hvanish : S.NoMapsFromKilled K p) {M : FinitelyGeneratedCategory A} (hM : S.almostSplitSkeleton.InAdd K M) (f : S.fgObj ↑p ⟶ M) : f = 0

Labelwise vanishing from a source extends to the complete additive closure of the killed labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.hom_eq_zero_of_inAdd_of_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)} {i : S.SurvivingLabel K} (hvanish : S.NoMapsToKilled K i) {M : FinitelyGeneratedCategory A} (hM : S.almostSplitSkeleton.InAdd K M) (f : M ⟶ S.fgObj ↑i) : f = 0

Labelwise vanishing into a sink extends to the complete additive closure of the killed labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factor_map_injective_on_hom_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 Y : S.SelectedAddCategory Set.univ} (f : X ⟶ Y) (hf : CategoryTheory.Mono f.hom) (a b : S.factorObject K p ⟶ (S.factorFunctor K).obj X) (hab : CategoryTheory.CategoryStruct.comp a ((S.factorFunctor K).map f) = CategoryTheory.CategoryStruct.comp b ((S.factorFunctor K).map f)) : a = b

Under source-to-killed vanishing, postcomposition by the quotient image of an ambient monomorphism is injective on Hom from the distinguished source.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factor_map_mono_of_representableFaithful {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) (hfaithful : S.FactorRepresentableFaithful K p) {X Y : S.SelectedAddCategory Set.univ} (f : X ⟶ Y) (hf : CategoryTheory.Mono f.hom) : CategoryTheory.Mono ((S.factorFunctor K).map f)

A faithful distinguished source promotes the quotient image of an ambient monomorphism to a monomorphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.labelRightMesh_f_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : CategoryTheory.Mono (S.labelRightMesh x).f

The first map of every ambient selected-label right mesh is monic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawRightMesh_f_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)} {p : S.SurvivingLabel K} (hvanish : S.NoMapsFromKilled K p) (hfaithful : S.FactorRepresentableFaithful K p) (x : Fin S.n) : CategoryTheory.Mono (S.factorRawRightMesh K x).f

Under the distinguished-source hypotheses, every raw factor right mesh has a monic first map.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLabelRightMesh_f_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)} {p : S.SurvivingLabel K} (hvanish : S.NoMapsFromKilled K p) (hfaithful : S.FactorRepresentableFaithful K p) (x : S.SurvivingLabel K) : CategoryTheory.Mono (S.factorLabelRightMesh K x).f

Under the distinguished-source hypotheses, every minimal surviving-label factor right mesh is strict.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRightMesh_f_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)} {p : S.SurvivingLabel K} (hvanish : S.NoMapsFromKilled K p) (hfaithful : S.FactorRepresentableFaithful K p) (X : S.FactorCategory K) : CategoryTheory.Mono (S.factorRightMesh K X).f

The componentwise factor right mesh is strict at every quotient object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalFactorRightMesh_f_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)} {p : S.SurvivingLabel K} (hvanish : S.NoMapsFromKilled K p) (hfaithful : S.FactorRepresentableFaithful K p) (x : S.SurvivingLabel K) : CategoryTheory.Mono (S.canonicalFactorRightMesh K (S.factorObject K x)).f

The canonical factor right mesh is strict at every surviving label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factor_map_injective_on_hom_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 Y : S.SelectedAddCategory Set.univ} (f : X ⟶ Y) (hf : CategoryTheory.Epi f.hom) (a b : (S.factorFunctor K).obj Y ⟶ S.factorObject K i) (hab : CategoryTheory.CategoryStruct.comp ((S.factorFunctor K).map f) a = CategoryTheory.CategoryStruct.comp ((S.factorFunctor K).map f) b) : a = b

Under killed-to-sink vanishing, precomposition by the quotient image of an ambient epimorphism is injective on Hom into the distinguished sink.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factor_map_epi_of_corepresentableFaithful {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) (hfaithful : S.FactorCorepresentableFaithful K i) {X Y : S.SelectedAddCategory Set.univ} (f : X ⟶ Y) (hf : CategoryTheory.Epi f.hom) : CategoryTheory.Epi ((S.factorFunctor K).map f)

A faithful distinguished sink promotes the quotient image of an ambient epimorphism to an epimorphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.labelLeftMesh_g_epi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : CategoryTheory.Epi (S.labelLeftMesh x).g

The second map of every ambient selected-label left mesh is epic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawLeftMesh_g_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)} {i : S.SurvivingLabel K} (hvanish : S.NoMapsToKilled K i) (hfaithful : S.FactorCorepresentableFaithful K i) (x : Fin S.n) : CategoryTheory.Epi (S.factorRawLeftMesh K x).g

Under the distinguished-sink hypotheses, every raw factor left mesh has an epic second map.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLabelLeftMesh_g_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)} {i : S.SurvivingLabel K} (hvanish : S.NoMapsToKilled K i) (hfaithful : S.FactorCorepresentableFaithful K i) (x : S.SurvivingLabel K) : CategoryTheory.Epi (S.factorLabelLeftMesh K x).g

Under the distinguished-sink hypotheses, every minimal surviving-label factor left mesh is strict.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLeftMesh_g_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)} {i : S.SurvivingLabel K} (hvanish : S.NoMapsToKilled K i) (hfaithful : S.FactorCorepresentableFaithful K i) (X : S.FactorCategory K) : CategoryTheory.Epi (S.factorLeftMesh K X).g

The componentwise factor left mesh is strict at every quotient object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalFactorLeftMesh_g_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)} {i : S.SurvivingLabel K} (hvanish : S.NoMapsToKilled K i) (hfaithful : S.FactorCorepresentableFaithful K i) (x : S.SurvivingLabel K) : CategoryTheory.Epi (S.canonicalFactorLeftMesh K (S.factorObject K x)).g

The canonical factor left mesh is strict at every surviving label.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveFactorInput {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

Exact categorical input supplied by a primitive directed deletion after the projective cover, injective envelope, and multiplicity weight have been identified.

• source : S.SurvivingLabel K
• sink : S.SurvivingLabel K
• source_projective : CategoryTheory.Projective (S.fgObj ↑self.source)
• sink_injective : CategoryTheory.Injective (S.fgObj ↑self.sink)
• noMapsFromKilled : S.NoMapsFromKilled K self.source
• noMapsToKilled : S.NoMapsToKilled K self.sink
• representableFaithful : S.FactorRepresentableFaithful K self.source
• corepresentableFaithful : S.FactorCorepresentableFaithful K self.sink
• 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

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorIsProjectiveDecidablePred {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)) : DecidablePred (S.factorFiniteTauCategoryData K).IsProjective

Projectivity of a surviving factor label is decidable because the label type is finite.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveFactorInput.source_isProjective {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.PrimitiveFactorInput K) : (S.factorFiniteTauCategoryData K).IsProjective D.source

The distinguished ambient projective becomes tau-projective in the literal factor category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveFactorInput.sink_isInjective {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.PrimitiveFactorInput K) : (S.factorFiniteTauCategoryData K).IsInjective D.sink

The distinguished ambient injective becomes tau-injective in the literal factor category.

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

Every canonical factor right mesh is strict under the primitive-factor input.

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

Every canonical factor left mesh is strict under the primitive-factor input.

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

Over an algebraically closed field, the strict primitive factor has the manuscript's Hom--mesh inverse data.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveFactorInput.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.PrimitiveFactorInput 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

The primitive multiplicity weight satisfies both unit equations of the factor-structure proposition.