Simple Auslander modules from strict tau meshes

For a surviving indecomposable X, the right tau mesh ending at X becomes, under the full-generator representable functor, the beginning of a projective resolution of the simple functor at X. Strictness makes its first map injective, while the right almost-split property identifies the image of its second map with the categorical radical.

The evaluated-mesh calculation is the only routine adapted from the clean equidistribution formalization. It is stated here directly for the literal factor category and its Auslander ring; no word-quiver or OP layer is imported.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableRadical {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) : Submodule (S.factorAuslanderRing K) (S.factorAdditiveGenerator K ⟶ S.factorObject K x)

The categorical radical inside a full-generator representable.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_factorRepresentableRadical_iff {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) (f : S.factorAdditiveGenerator K ⟶ S.factorObject K x) : f ∈ S.factorRepresentableRadical K x ↔ QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f

@[reducible, inline]

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

The simple-functor candidate at a surviving factor label.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderSimpleModule {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) : Module k (S.factorAuslanderSimple K x)

The coefficient-field structure on the radical quotient, obtained by restriction from the factor Auslander algebra.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderSimpleIsScalarTower {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) : IsScalarTower k (S.factorAuslanderRing K) (S.factorAuslanderSimple K x)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableMeshTargetMap {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.factorFiniteTauCategoryData K).thetaPlus x ⟶ S.factorObject K x

The transported second map of the right mesh, with literal endpoint factorObject K x.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableMeshNu {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.factorAdditiveGenerator K ⟶ ((S.factorFiniteTauCategoryData K).rightMesh (S.factorObject K x)).X₁) →ₗ[S.factorAuslanderRing K] S.factorAdditiveGenerator K ⟶ (S.factorFiniteTauCategoryData K).thetaPlus x

The first evaluated mesh differential.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableMeshMu {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.factorAdditiveGenerator K ⟶ (S.factorFiniteTauCategoryData K).thetaPlus x) →ₗ[S.factorAuslanderRing K] S.factorAdditiveGenerator K ⟶ S.factorObject K x

The second evaluated mesh differential.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableMesh_exact_middle {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) : Function.Exact ⇑(S.factorRepresentableMeshNu K x) ⇑(S.factorRepresentableMeshMu K x)

Exactness of the evaluated right mesh at its middle representable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.range_factorRepresentableMeshMu {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.factorRepresentableMeshMu K x).range = S.factorRepresentableRadical K x

The second evaluated mesh differential has exactly the categorical radical as its image.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorHom_mem_radical_of_ne {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)) {a x : S.SurvivingLabel K} (hax : a ≠ x) (f : S.factorObject K a ⟶ S.factorObject K x) : f ∈ (S.factorFiniteTauCategoryData K).radical.ideal.hom (S.factorObject K a) (S.factorObject K x)

Between distinct surviving indecomposables every morphism belongs to the categorical radical.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderSimpleGenerator {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.factorAuslanderSimple K x

The identity-coordinate class generating the simple functor at x.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderSimpleGenerator_ne_zero {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.factorAuslanderSimpleGenerator K x ≠ 0

The identity-coordinate class in the radical quotient is nonzero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finrank_factorAuslanderSimple_eq_one {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (K : Set (Fin S.n)) (x : S.SurvivingLabel K) : Module.finrank k ↑(ModuleCat.of (S.factorAuslanderRing K) (S.factorAuslanderSimple K x)) = 1

The categorical radical quotient at x is one-dimensional over the coefficient field.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderSimple_simple {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (K : Set (Fin S.n)) (x : S.SurvivingLabel K) : CategoryTheory.Simple (ModuleCat.of (S.factorAuslanderRing K) (S.factorAuslanderSimple K x))

The mesh radical quotient is a simple module over the factor Auslander ring.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableMeshMuToRadical {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.factorAdditiveGenerator K ⟶ (S.factorFiniteTauCategoryData K).thetaPlus x) →ₗ[S.factorAuslanderRing K] ↥(S.factorRepresentableRadical K x)

The second evaluated mesh map, corestricted to its radical image.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableMesh_exact_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 : S.SurvivingLabel K) : Function.Exact ⇑(S.factorRepresentableMeshNu K x) ⇑(S.factorRepresentableMeshMuToRadical K x)

Corestricting the second mesh differential to the radical preserves exactness at the middle representable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableMeshNu_injective {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) : Function.Injective ⇑(S.factorRepresentableMeshNu K x)

Strictness of the right mesh makes its first evaluated differential injective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableMeshMuToRadical_surjective {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) : Function.Surjective ⇑(S.factorRepresentableMeshMuToRadical K x)

The corestricted second evaluated mesh differential is onto the categorical radical.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderSimple_hasProjectiveDimensionLE_two {k A : Type u} [Field k] [IsAlgClosed 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.HasProjectiveDimensionLE (ModuleCat.of (S.factorAuslanderRing K) (S.factorAuslanderSimple K x)) 2

A strict right tau mesh gives a length-two projective resolution of the simple Auslander module at its endpoint.