Opposite Auslander simples from strict left tau meshes

For a surviving indecomposable X, evaluation of the strict left tau mesh starting at X gives a projective resolution of the corresponding simple module over End(G), where G is the full factor generator. This is the opposite-side counterpart of RightModuleIyamaSimpleResolution, which uses right meshes to resolve simples over the factor Auslander ring End(G)ᵒᵖ.

The projectivity input is obtained without importing a second categorical realization: full additive Yoneda identifies Hom(X,G) with the regular-Hom dual of the projective Hom(G,X), and the finite-projective duality already developed for Nakayama modules makes that dual projective over End(G).

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorOppositeAuslanderRing {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 u

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderRepresentableFGObj {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) : FGModuleCat (S.factorOppositeAuslanderRing K)ᵐᵒᵖ

A full-generator representable, bundled over the factor Auslander ring.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableRegularHomDualLinearEquiv {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) : (X ⟶ S.factorAdditiveGenerator K) ≃ₗ[S.factorOppositeAuslanderRing K] regularHomDualCarrier (S.factorAuslanderRepresentableFGObj K X)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentable_finiteProjective {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.finiteProjectiveModules (S.factorOppositeAuslanderRing K) (ModuleCat.of (S.factorOppositeAuslanderRing K) (X ⟶ S.factorAdditiveGenerator K))

Every full-generator corepresentable is finite projective over End(G).

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableRadical {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.factorOppositeAuslanderRing K) (S.factorObject K x ⟶ S.factorAdditiveGenerator K)

@[simp]

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

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorOppositeAuslanderSimple {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

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorOppositeAuslanderSimpleModule {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.factorOppositeAuslanderSimple K x)

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorOppositeAuslanderSimpleIsScalarTower {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.factorOppositeAuslanderRing K) (S.factorOppositeAuslanderSimple K x)

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableMeshNu {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).leftMesh (S.factorObject K x)).X₃ ⟶ S.factorAdditiveGenerator K) →ₗ[S.factorOppositeAuslanderRing K] (S.factorFiniteTauCategoryData K).thetaMinus x ⟶ S.factorAdditiveGenerator K

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableMeshMu {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).thetaMinus x ⟶ S.factorAdditiveGenerator K) →ₗ[S.factorOppositeAuslanderRing K] S.factorObject K x ⟶ S.factorAdditiveGenerator K

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableMesh_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.factorCorepresentableMeshNu K x) ⇑(S.factorCorepresentableMeshMu K x)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.range_factorCorepresentableMeshMu {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.factorCorepresentableMeshMu K x).range = S.factorCorepresentableRadical K x

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorOppositeAuslanderSimpleGenerator_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.factorOppositeAuslanderSimpleGenerator K x ≠ 0

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finrank_factorOppositeAuslanderSimple_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.factorOppositeAuslanderRing K) (S.factorOppositeAuslanderSimple K x)) = 1

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorOppositeAuslanderSimple_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.factorOppositeAuslanderRing K) (S.factorOppositeAuslanderSimple K x))

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableMeshMuToRadical {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).thetaMinus x ⟶ S.factorAdditiveGenerator K) →ₗ[S.factorOppositeAuslanderRing K] ↥(S.factorCorepresentableRadical K x)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableMesh_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.factorCorepresentableMeshNu K x) ⇑(S.factorCorepresentableMeshMuToRadical K x)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableMeshNu_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.factorCorepresentableMeshNu K x)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableMeshMuToRadical_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.factorCorepresentableMeshMuToRadical K x)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorOppositeAuslanderSimple_hasProjectiveDimensionLE_two {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.HasProjectiveDimensionLE (ModuleCat.of (S.factorOppositeAuslanderRing K) (S.factorOppositeAuslanderSimple K x)) 2

A strict left tau mesh gives a length-two projective resolution of the corresponding simple quotient over the opposite Auslander ring.