Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardSeparatedIntervals

Separated block deletion in the actual standard-form intervals #

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.separatedIntervalMeshHomFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : S.StandardFormMeshCategory) :
FiniteDimensional k (X ⟶ Y)
source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.separatedIntervalBaseFinite {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
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOppositeAlgebra_above_control {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (d : ℤ) (hd : ↑S.standardFormIntervalControlHeight < d) :
(S.standardFormOppositeAlgebraGrading ⋯).component d = ⊥

The common interval control height also bounds the actual standard-form algebra grading, not just its mesh Hom spaces.

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

The principal-projective category whose matrix algebra is the actual standard-form interval algebra.

Instances For
    source
    def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalSeparatedDeleted {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m r q : ℕ) :
    Set (S.standardFormIntervalPrincipalCategory m)ᵒᵖ

    Objects deleted between the separated blocks inside the actual interval.

    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalSeparated_noDeletedFactorization {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m r q : ℕ) :
      ObjectDeletion.NoDeletedFactorization (S.standardFormIntervalPrincipalCategory m)ᵒᵖ (S.standardFormIntervalSeparatedDeleted m r q)

      In the actual finite interval, deleting the gaps imposes no relations between retained objects.