Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardIntervalThin

Thin indecomposables and biserial projectives in zero-surplus intervals #

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalThinBaseFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
FiniteDimensional k (S.standardFormAlgebra ⋯)
source
@[instance_reducible]
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalThinFintype {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
Fintype (S.standardFormIntervalPrincipalCategory m)
Instances For
    source
    @[instance_reducible]
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalThinOpFintype {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
    Fintype (S.standardFormIntervalPrincipalCategory m)ᵒᵖ
    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalThinAlgebraFinite {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.intervalThinAlgebraNoetherian {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
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalCategory_pointwiseThin_of_ambient_eq_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hz : S.ambientARSurplus = 0) (m : ℕ) (M : CoveringHom.FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) :
      CoveringHom.IsPointwiseThin M.obj.obj

      Every indecomposable interval category module is pointwise thin at zero ambient surplus.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalCategory_representable_biserial_of_ambient_eq_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hz : S.ambientARSurplus = 0) (m : ℕ) (X : (S.standardFormIntervalPrincipalCategory m)ᵒᵖ) :
      IsBiserialObject ((CoveringHom.finiteDimensionalLinearCoyonedaFunctor ⋯).obj (Opposite.op X))

      Every representable interval module is biserial at zero ambient surplus.