Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleIyamaGlobalDimension

The global-dimension bound for the factor Auslander algebra #

The strict right meshes resolve the simple tops of all indecomposable represented projectives. This file identifies those tops with all simple modules over the factor Auslander algebra and then propagates the resulting projective-dimension bound through finite-length modules.

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderRepresentable_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.factorAuslanderRing K) (S.factorAdditiveGenerator K ⟶ S.factorObject K x))

A represented surviving indecomposable has local module-endomorphism ring over the factor Auslander algebra.

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableRadical_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.factorRepresentableRadical K x = Module.jacobson (S.factorAuslanderRing K) (S.factorAdditiveGenerator K ⟶ S.factorObject K x)

The categorical radical is the unique maximal submodule of the represented indecomposable.

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRepresentableToModule {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.factorAuslanderRing K) M] (m : M) :
(S.factorAdditiveGenerator K ⟶ S.factorObject K x) →ₗ[S.factorAuslanderRing K] M

A vector in an arbitrary Auslander module induces a map from each indecomposable represented projective.

Instances For
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_factorRepresentableToModule_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.factorAuslanderRing K) M] (m : M) (hm : m ≠ 0) :
    ∃ (x : S.SurvivingLabel K), S.factorRepresentableToModule K x m ≠ 0

    The represented indecomposable projectives generate the module category: some coordinate map induced by a nonzero vector is nonzero.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_factorAuslanderSimple_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.factorAuslanderRing K) M] [IsSimpleModule (S.factorAuslanderRing K) M] :
    ∃ (x : S.SurvivingLabel K), Nonempty (S.factorAuslanderSimple K x ≃ₗ[S.factorAuslanderRing K] M)

    Every simple module over the factor Auslander algebra is one of the radical quotients attached to a surviving indecomposable.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.simpleModule_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) (H : S.HasAcyclicNonzeroNonisomorphisms) {M : Type u} [AddCommGroup M] [Module (S.factorAuslanderRing K) M] [IsSimpleModule (S.factorAuslanderRing K) M] :
    CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of (S.factorAuslanderRing K) M) 2

    Consequently every simple factor-Auslander module has projective dimension at most two.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteLengthModule_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) (H : S.HasAcyclicNonzeroNonisomorphisms) {M : Type u} [AddCommGroup M] [Module (S.factorAuslanderRing K) M] (hM : IsFiniteLength (S.factorAuslanderRing K) M) :
    CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of (S.factorAuslanderRing K) M) 2

    The simple-module bound is stable under finite extensions.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteModule_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) (H : S.HasAcyclicNonzeroNonisomorphisms) {M : Type u} [AddCommGroup M] [Module (S.factorAuslanderRing K) M] [Module.Finite (S.factorAuslanderRing K) M] :
    CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of (S.factorAuslanderRing K) M) 2

    Every finite module over the finite-dimensional factor Auslander algebra has projective dimension at most two.