Left tau-sequences in literal finite-module factor categories

This file descends the chosen ambient left Auslander--Reiten meshes through the literal quotient by maps factoring through selected labels. It is the left-right dual of the direct right-mesh descent, with an explicit quotient weak-cokernel correction and minimalization of the possibly zero right boundary.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawLeftMesh {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)) (x : Fin S.n) : CategoryTheory.ShortComplex (S.FactorCategory K)

The literal image of the selected ambient left mesh in the factor category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawLeftMesh_radical {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)) (x : Fin S.n) : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (S.factorRawLeftMesh K x).f ∧ QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (S.factorRawLeftMesh K x).g

Both maps in the raw quotient left mesh remain radical.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawLeftMesh_X₁ {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)) (x : S.SurvivingLabel K) : (S.factorRawLeftMesh K ↑x).X₁ = S.factorObject K x

The raw quotient left mesh at a surviving label starts at its literal factor object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawLeftMesh_factors_from_left {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)) (x : S.SurvivingLabel K) {W : S.FactorCategory K} (a : (S.factorRawLeftMesh K ↑x).X₁ ⟶ W) : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism a → ∃ (b : (S.factorRawLeftMesh K ↑x).X₂ ⟶ W), CategoryTheory.CategoryStruct.comp (S.factorRawLeftMesh K ↑x).f b = a

Radical maps out of a surviving source factor through the raw quotient left-mesh map.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawLeftMesh_factors_into_right {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)) (x : S.SurvivingLabel K) {W : S.FactorCategory K} (a : W ⟶ (S.factorRawLeftMesh K ↑x).X₃) : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism a → ∃ (b : W ⟶ (S.factorRawLeftMesh K ↑x).X₂), CategoryTheory.CategoryStruct.comp b (S.factorRawLeftMesh K ↑x).g = a

Radical maps into the raw quotient left mesh's right endpoint factor through its second map.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawLeftMesh_isWeakCokernel {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)) (x : S.SurvivingLabel K) : QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakCokernel (S.factorRawLeftMesh K ↑x)

The raw quotient left mesh retains the weak-cokernel property.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawLeftMesh_tauApproximation {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)) (x : S.SurvivingLabel K) : QuotientSubmoduleEquidistribution.Iyama.TauApproximation (S.factorRawLeftMesh K ↑x)

The raw quotient left mesh satisfies the radical approximation part of a left tau-sequence.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawLeftMesh_X₃_zero_or_exists_factorObject_iso {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)) (x : S.SurvivingLabel K) : CategoryTheory.Limits.IsZero (S.factorRawLeftMesh K ↑x).X₃ ∨ ∃ (y : S.SurvivingLabel K), Nonempty ((S.factorRawLeftMesh K ↑x).X₃ ≅ S.factorObject K y)

The target of a raw quotient left mesh is either zero or isomorphic to a surviving selected indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawLeftMesh_X₃_not_isZero_of_inverse_translation_survives {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)) (x : Fin S.n) (hx : ¬CategoryTheory.Injective (S.fgObj x)) (hy : ↑(S.rightTranslationEquiv.symm ⟨x, hx⟩) ∉ K) : ¬CategoryTheory.Limits.IsZero (S.factorRawLeftMesh K x).X₃

If an ambient label is noninjective and its inverse right translate survives, then the target of its raw quotient left mesh is nonzero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawLeftTau_of_nonzero {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)) (x : S.SurvivingLabel K) (htarget : ¬CategoryTheory.Limits.IsZero (S.factorRawLeftMesh K ↑x).X₃) (hg : (S.factorRawLeftMesh K ↑x).g ≠ 0) : QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence (S.factorRawLeftMesh K ↑x)

If its target and second map survive, the raw quotient left mesh is already a left tau-sequence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorZeroRightLeftMesh {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)) (x : S.SurvivingLabel K) : CategoryTheory.ShortComplex (S.FactorCategory K)

The raw quotient left mesh with its right term replaced by the chosen zero object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorZeroRightLeftTau {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)) (x : S.SurvivingLabel K) (hzero : CategoryTheory.Limits.IsZero (S.factorRawLeftMesh K ↑x).X₃ ∨ (S.factorRawLeftMesh K ↑x).g = 0) : QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence (S.factorZeroRightLeftMesh K x)

Replacing the right term by zero gives a left tau-sequence whenever the raw target is zero or the raw second map vanishes.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLabelLeftMesh {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)) (x : S.SurvivingLabel K) : CategoryTheory.ShortComplex (S.FactorCategory K)

The minimal left mesh at a surviving quotient label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLabelLeftTau {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)) (x : S.SurvivingLabel K) : QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence (S.factorLabelLeftMesh K x)

Every surviving-label factor left mesh is a left tau-sequence.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLabelLeftMesh_X₁ {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)) (x : S.SurvivingLabel K) : (S.factorLabelLeftMesh K x).X₁ = S.factorObject K x

The minimal factor left mesh still starts at its selected factor object.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLeftMesh {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)) (X : S.FactorCategory K) : CategoryTheory.ShortComplex (S.FactorCategory K)

Extend the surviving-label left meshes to every quotient object by finite componentwise biproduct.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLeftTermIso {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)) (X : S.FactorCategory K) : (S.factorLeftMesh K X).X₁ ≅ X

The assembled factor left mesh starts at the supplied quotient object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLeftTau {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)) (X : S.FactorCategory K) : QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence (S.factorLeftMesh K X)

Every assembled quotient-object left mesh is a left tau-sequence.