Right tau-sequences in literal finite-module factor categories

This file descends the chosen ambient right Auslander--Reiten meshes through the literal quotient by maps factoring through selected labels. The raw quotient mesh retains the radical approximation and weak-kernel properties; only its possibly zero left boundary requires minimalization.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawRightMesh {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 right mesh in the factor category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawRightMesh_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.factorRawRightMesh K x).f ∧ QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (S.factorRawRightMesh K x).g

Both maps in the raw quotient mesh remain radical.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawRightMesh_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.factorRawRightMesh K ↑x).X₃ = S.factorObject K x

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

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

Radical maps into a surviving endpoint factor through the raw quotient right-mesh map.

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

Radical maps out of the raw quotient mesh's left endpoint factor through its first map.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawRightMesh_isWeakKernel {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.IsWeakKernel (S.factorRawRightMesh K ↑x)

The raw quotient mesh retains the weak-kernel property.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawRightMesh_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.factorRawRightMesh K ↑x)

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawRightMesh_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.factorRawRightMesh K ↑x).X₁ ∨ ∃ (y : S.SurvivingLabel K), Nonempty ((S.factorRawRightMesh K ↑x).X₁ ≅ S.factorObject K y)

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawRightMesh_X₁_not_isZero_of_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.Projective (S.fgObj x)) (hy : S.rightTranslationLabel ⟨x, hx⟩ ∉ K) : ¬CategoryTheory.Limits.IsZero (S.factorRawRightMesh K x).X₁

If an ambient label is nonprojective and its right translate survives, then the source of its raw quotient right mesh is nonzero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawRightTau_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) (hsource : ¬CategoryTheory.Limits.IsZero (S.factorRawRightMesh K ↑x).X₁) (hf : (S.factorRawRightMesh K ↑x).f ≠ 0) : QuotientSubmoduleEquidistribution.Iyama.RightTauSequence (S.factorRawRightMesh K ↑x)

If its source and first map survive, the raw quotient mesh is already a right tau-sequence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorZeroObject {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)) : S.FactorCategory K

A chosen zero object in the factor category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorZeroObject_isZero {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)) : CategoryTheory.Limits.IsZero (S.factorZeroObject K)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorZeroLeftRightMesh {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 mesh with its left term replaced by a chosen zero object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorZeroLeftRightTau {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.factorRawRightMesh K ↑x).X₁ ∨ (S.factorRawRightMesh K ↑x).f = 0) : QuotientSubmoduleEquidistribution.Iyama.RightTauSequence (S.factorZeroLeftRightMesh K x)

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLabelRightMesh {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 right mesh at a surviving quotient label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLabelRightTau {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.RightTauSequence (S.factorLabelRightMesh K x)

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLabelRightMesh_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.factorLabelRightMesh K x).X₃ = S.factorObject K x

The minimal factor right mesh still ends at its selected factor object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLabelRightMesh_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.factorLabelRightMesh K x).X₂ = (S.factorRawRightMesh K ↑x).X₂

Minimalizing the raw factor mesh changes only its left term; its middle term remains the image of the ambient right-mesh middle term.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.survivingLabelFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : Fintype (S.SurvivingLabel K)

The surviving subtype inherits a finite enumeration from the ambient finite skeleton.

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

A chosen decomposition of a factor-category object into the surviving indecomposable representatives.

• n : ℕ
• label : Fin self.n → S.SurvivingLabel K
• iso : X ≅ ⨁ fun (i : Fin self.n) => S.factorObject K (self.label i)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.chosenFactorLabelDecomposition {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.ChosenFactorLabelDecomposition K X

Choose one surviving-label decomposition for every quotient object.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRightMesh {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 right meshes to every quotient object by finite componentwise biproduct.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRightTermIso {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.factorRightMesh K X).X₃ ≅ X

The assembled factor right mesh ends at the supplied quotient object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRightTau {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.RightTauSequence (S.factorRightMesh K X)

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorFiniteRightTauCategoryData {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)) : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData (S.FactorCategory K) (S.SurvivingLabel K)

The literal quotient by any selected labels carries all finite right-tau-category data, with the surviving skeleton as its labels.