The tau-projective boundary Nakayama estimate

Strict left tau meshes resolve the simple modules over End(G). If X is tau-projective, every map from X into the nonprojective third term of a left mesh is radical, so the left tau approximation makes the relevant degree-two Ext class vanish. Classification of simples and finite-length induction then give injective dimension at most one for Hom(X,G).

Finite contragredient duality turns a corresponding injective copresentation into a two-term projective presentation of the Nakayama module. Finally, additivity assembles the indecomposable estimates over the literal boundary generator U.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgModuleCatHasFiniteBiproducts {R : Type u} [Ring R] [IsNoetherianRing R] : CategoryTheory.Limits.HasFiniteBiproducts (FGModuleCat R)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_factorCorepresentable_hom_of_moduleHom {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 Y : S.FactorCategory K} (P : CategoryTheory.FiniteAddPresentation (S.factorAdditiveGenerator K) Y) (α : ModuleCat.of (S.factorOppositeAuslanderRing K) (Y ⟶ S.factorAdditiveGenerator K) ⟶ ModuleCat.of (S.factorOppositeAuslanderRing K) (X ⟶ S.factorAdditiveGenerator K)) : ∃ (f : X ⟶ Y), (CategoryTheory.preadditiveYonedaObj (S.factorAdditiveGenerator K)).map f.op = α

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorHomToGenerator {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.Functor (CategoryTheory.finiteAddClosure (S.factorAdditiveGenerator K)).FullSubcategoryᵒᵖ (ModuleCat (S.factorOppositeAuslanderRing K))

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorHomToGenerator_full {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.factorHomToGenerator K).Full

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorHomToGenerator_faithful {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.factorHomToGenerator K).Faithful

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorHomToGeneratorFullyFaithful {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.factorHomToGenerator K).FullyFaithful

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentable_end_isLocalRing {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) : IsLocalRing (Module.End (S.factorOppositeAuslanderRing K) (S.factorObject K x ⟶ S.factorAdditiveGenerator K))

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableRadical_eq_jacobson {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) : S.factorCorepresentableRadical K x = Module.jacobson (S.factorOppositeAuslanderRing K) (S.factorObject K x ⟶ S.factorAdditiveGenerator K)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableToModule {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) {M : Type u} [AddCommGroup M] [Module (S.factorOppositeAuslanderRing K) M] (m : M) : (S.factorObject K x ⟶ S.factorAdditiveGenerator K) →ₗ[S.factorOppositeAuslanderRing K] M

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_factorCorepresentableToModule_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)) {M : Type u} [AddCommGroup M] [Module (S.factorOppositeAuslanderRing K) M] (m : M) (hm : m ≠ 0) : ∃ (x : S.SurvivingLabel K), S.factorCorepresentableToModule K x m ≠ 0

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_factorOppositeAuslanderSimple_linearEquiv {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)) {M : Type u} [AddCommGroup M] [Module (S.factorOppositeAuslanderRing K) M] [IsSimpleModule (S.factorOppositeAuslanderRing K) M] : ∃ (x : S.SurvivingLabel K), Nonempty (S.factorOppositeAuslanderSimple K x ≃ₗ[S.factorOppositeAuslanderRing K] M)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjective_to_leftMeshThird_isRadical {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 y : S.SurvivingLabel K) (hx : (S.factorFiniteTauCategoryData K).IsProjective x) (f : S.factorObject K x ⟶ ((S.factorFiniteTauCategoryData K).leftMesh (S.factorObject K y)).X₃) : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableMeshNu_hom_surjective_at_projective {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 y : S.SurvivingLabel K) (hx : (S.factorFiniteTauCategoryData K).IsProjective x) : Function.Surjective fun (a : ModuleCat.of (S.factorOppositeAuslanderRing K) ((S.factorFiniteTauCategoryData K).thetaMinus y ⟶ S.factorAdditiveGenerator K) ⟶ ModuleCat.of (S.factorOppositeAuslanderRing K) (S.factorObject K x ⟶ S.factorAdditiveGenerator K)) => CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (S.factorCorepresentableMeshNu K y)) a

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorOppositeAuslanderModuleHasExt {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.HasExt (ModuleCat (S.factorOppositeAuslanderRing K))

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorOppositeAuslanderSimple_ext_two_corepresentable_eq_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)} (D : S.PrimitiveFactorInput K) (x y : S.SurvivingLabel K) (hx : (S.factorFiniteTauCategoryData K).IsProjective x) (xi : CategoryTheory.Abelian.Ext (ModuleCat.of (S.factorOppositeAuslanderRing K) (S.factorOppositeAuslanderSimple K y)) (ModuleCat.of (S.factorOppositeAuslanderRing K) (S.factorObject K x ⟶ S.factorAdditiveGenerator K)) 2) : xi = 0

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.simpleModule_ext_two_corepresentable_eq_zero {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) (H : S.HasAcyclicNonzeroNonisomorphisms) (p : S.SurvivingLabel K) (hp : (S.factorFiniteTauCategoryData K).IsProjective p) {M : Type u} [AddCommGroup M] [Module (S.factorOppositeAuslanderRing K) M] [IsSimpleModule (S.factorOppositeAuslanderRing K) M] (xi : CategoryTheory.Abelian.Ext (ModuleCat.of (S.factorOppositeAuslanderRing K) M) (ModuleCat.of (S.factorOppositeAuslanderRing K) (S.factorObject K p ⟶ S.factorAdditiveGenerator K)) 2) : xi = 0

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteLengthModule_ext_two_corepresentable_eq_zero {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) (H : S.HasAcyclicNonzeroNonisomorphisms) (p : S.SurvivingLabel K) (hp : (S.factorFiniteTauCategoryData K).IsProjective p) {M : Type u} [AddCommGroup M] [Module (S.factorOppositeAuslanderRing K) M] (hM : IsFiniteLength (S.factorOppositeAuslanderRing K) M) (xi : CategoryTheory.Abelian.Ext (ModuleCat.of (S.factorOppositeAuslanderRing K) M) (ModuleCat.of (S.factorOppositeAuslanderRing K) (S.factorObject K p ⟶ S.factorAdditiveGenerator K)) 2) : xi = 0

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentableFGObj {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)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorOppositeAuslanderFGModuleHasExt {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.HasExt (FGModuleCat (S.factorOppositeAuslanderRing K))

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgModule_ext_two_corepresentable_eq_zero {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) (H : S.HasAcyclicNonzeroNonisomorphisms) (p : S.SurvivingLabel K) (hp : (S.factorFiniteTauCategoryData K).IsProjective p) (Y : FGModuleCat (S.factorOppositeAuslanderRing K)) (xi : CategoryTheory.Abelian.Ext Y (S.factorCorepresentableFGObj K (S.factorObject K p)) 2) : xi = 0

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorCorepresentable_hasInjectiveDimensionLE_one {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) (H : S.HasAcyclicNonzeroNonisomorphisms) (p : S.SurvivingLabel K) (hp : (S.factorFiniteTauCategoryData K).IsProjective p) : CategoryTheory.HasInjectiveDimensionLE (S.factorCorepresentableFGObj K (S.factorObject K p)) 1

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.dualFactorCorepresentable_hasProjectiveDimensionLE_one {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) (H : S.HasAcyclicNonzeroNonisomorphisms) (p : S.SurvivingLabel K) (hp : (S.factorFiniteTauCategoryData K).IsProjective p) : CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of (S.factorAuslanderRing K) ↑((QuotientSubmoduleEquidistribution.Contragredient.dualFunctor k (S.factorOppositeAuslanderRing K)).obj (Opposite.op (S.factorCorepresentableFGObj K (S.factorObject K p))))) 1

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderRepresentableNakayama_hasProjectiveDimensionLE_one {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) (H : S.HasAcyclicNonzeroNonisomorphisms) (p : S.SurvivingLabel K) (hp : (S.factorFiniteTauCategoryData K).IsProjective p) : CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of (S.factorAuslanderRing K) ↑(projectiveNakayamaFGObj (S.factorAuslanderRepresentableFGObj K (S.factorObject K p)))) 1

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableFGFunctor {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.Functor (S.FactorCategory K) (FGModuleCat (S.factorAuslanderRing K))

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableFGFunctor_additive {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.factorRepresentableFGFunctor K).Additive

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveNakayamaFunctor {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.Functor (FGModuleCat (S.factorAuslanderRing K)) (FGModuleCat (S.factorAuslanderRing K))

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveNakayamaFunctor_additive {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.factorProjectiveNakayamaFunctor K).Additive

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveLabelFintype {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)) : Fintype (S.FactorProjectiveLabel K)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorBoundaryRepresentableBiproductIso {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.factorBoundaryRepresentableFGObj K ≅ ⨁ fun (p : S.FactorProjectiveLabel K) => S.factorAuslanderRepresentableFGObj K (S.factorObject K ↑p)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorBoundaryNakayama_hasProjectiveDimensionLE_one {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) (H : S.HasAcyclicNonzeroNonisomorphisms) : CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of (S.factorAuslanderRing K) ↑(projectiveNakayamaFGObj (S.factorBoundaryRepresentableFGObj K))) 1