Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardIntervalClassification

Actual indecomposable modules of the standard-form interval algebra #

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardIntervalClassificationFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
FiniteDimensional k (S.standardFormIntervalAlgebra m)
source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardIntervalClassificationNoetherian {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
IsNoetherianRing (S.standardFormIntervalAlgebra m)ᵐᵒᵖ
source
instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalEquivalence_additive {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
(S.standardFormIntervalAlgebraEquivalence m).functor.Additive
source
instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalEquivalence_inverse_additive {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
(S.standardFormIntervalAlgebraEquivalence m).inverse.Additive
source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalFamily {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (a : S.standardFormSupportedLabel m) :
FGModuleCat (S.standardFormIntervalAlgebra m)ᵐᵒᵖ

The indecomposable right interval modules, indexed by the exact allowed shifts.

Instances For
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalFamily_indecomposable {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (a : S.standardFormSupportedLabel m) :
    CategoryTheory.Indecomposable (S.standardFormIntervalFamily m a)

    Every member of the interval family is indecomposable.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalFamily_complete {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (X : FGModuleCat (S.standardFormIntervalAlgebra m)ᵐᵒᵖ) (hX : CategoryTheory.Indecomposable X) :
    ∃ (a : S.standardFormSupportedLabel m), Nonempty (X ≅ S.standardFormIntervalFamily m a)

    Every indecomposable right interval module occurs in the finite family.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalFamily_skeletal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (a b : S.standardFormSupportedLabel m) (e : S.standardFormIntervalFamily m a ≅ S.standardFormIntervalFamily m b) :
    a = b

    The interval family has no repeated isomorphism class.