Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardIntervalBiserial

Special-biserial interval algebras at zero ambient surplus #

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalBiserialBaseFinite {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.intervalBiserialFintype {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.intervalBiserialOpFintype {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.intervalBiserialFinite {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.intervalBiserialNoetherian {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_finiteCovariantRepresentables {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.standardFormIntervalPrincipalCategory m) :
      CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)

      Finite representables in the other variance of the actual interval.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalCategory_end_isLocalRing {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.standardFormIntervalPrincipalCategory m) :
      IsLocalRing (CategoryTheory.End X)

      Endomorphism rings of the interval objects are local in both variances.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalAlgebra_admitsSpecialBiserialPresentation_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 : ℕ) :
      BoundQuiver.AdmitsSpecialBiserialPresentation k (S.standardFormIntervalAlgebra m)

      Every interval algebra at zero ambient surplus admits the literal special-biserial presentation obtained from its two-sided biserial projectives.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalAlgebra_isSpecialBiserial_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 : ℕ) :
      BoundQuiver.IsSpecialBiserial k (S.standardFormIntervalAlgebra m)

      Zero ambient surplus makes every interval algebra special biserial.