Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleSocleReductionString

Socle reduction to a string algebra #

This file isolates the axiom-free numerical consequence of the structural socle-reduction theorem. It selects all nonuniserial indecomposable projective-injective right modules, rejects their socles simultaneously, and uses a supplied string presentation of the quotient to force vanishing of the ambient Auslander--Reiten surplus.

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.nonuniserialProjectiveInjectiveLabels {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
Finset S.ProjectiveLabel

The canonical finite family of indecomposable projective-injective right modules which are not uniserial.

Instances For
    source
    @[simp]
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_nonuniserialProjectiveInjectiveLabels_iff {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) :
    p ∈ S.nonuniserialProjectiveInjectiveLabels ↔ CategoryTheory.Injective (S.fgObj p.label) ∧ ¬IsUniserialModule Aᵐᵒᵖ ↑(S.fgObj p.label)
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.nonuniserialProjectiveInjectiveLabels_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) (hp : p ∈ S.nonuniserialProjectiveInjectiveLabels) :
    CategoryTheory.Injective (S.fgObj p.label)

    Every member of the canonical family is injective.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.nonuniserialProjectiveInjectiveLabels_notSimple {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) (hp : p ∈ S.nonuniserialProjectiveInjectiveLabels) :
    ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)

    Every member of the canonical family is non-simple.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamily_ambientARSurplus_eq {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] :
    S.ambientARSurplus = (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).ambientARSurplus

    Simultaneous socle rejection preserves the categorical ambient Auslander--Reiten surplus.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.ambientARSurplus_eq_zero_of_socleFamilyQuotient_admitsStringPresentation {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hString : BoundQuiver.AdmitsStringPresentation k (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal S.nonuniserialProjectiveInjectiveLabels ⋯))) :
    S.ambientARSurplus = 0

    If the canonical simultaneous socle quotient is a string algebra, then the original module category has zero Auslander--Reiten surplus. This is the axiom-free consequence consumed by the final converse.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.beta_le_two_of_socleFamilyQuotient_admitsStringPresentation {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hString : BoundQuiver.AdmitsStringPresentation k (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal S.nonuniserialProjectiveInjectiveLabels ⋯))) :
    FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ 2

    If the canonical simultaneous socle quotient is a string algebra, then the original module category satisfies the sharp bound beta ≤ 2.