Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardSupportedCategory

The intrinsic finite classification of supported standard-form graded modules #

source
@[reducible, inline]
abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportedLabel {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
Type

Labels and exactly the shifts whose support stays in the interval.

Instances For
    source
    @[reducible, inline]
    abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportedCategory {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
    Type (u + 1)
    Instances For
      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportedFamily {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) :
      S.standardFormSupportedCategory m

      The supported representative attached to an allowed label.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportedFamily_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.standardFormSupportedFamily m a)
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportedFamily_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 : S.standardFormSupportedCategory m) (hX : CategoryTheory.Indecomposable X) :
        ∃ (a : S.standardFormSupportedLabel m), Nonempty (X ≅ S.standardFormSupportedFamily m a)

        Every indecomposable in the supported category occurs in the finite family.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportedFamily_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.standardFormSupportedFamily m a ≅ S.standardFormSupportedFamily m b) :
        a = b

        Distinct supported labels represent distinct isomorphism classes.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportedLabel_card {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (hm : S.standardFormSupportHeight ≤ m) :
        ↑(Fintype.card (S.standardFormSupportedLabel m)) = ↑S.n * (↑m + 1) - ∑ i : Fin S.n, (↑(S.standardFormSupportWindow i).upper - ↑(S.standardFormSupportWindow i).lower)

        The cardinality is the exact number of supported graded indecomposable classes.