Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardIntervalBetaTransfer

One-sided beta transfer to the single control interval #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalBetaQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
Quiver (Fin S.n)
Instances For
    source
    @[instance_reducible]
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalBetaArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) :
    Fintype (x ⟶ y)
    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalBetaBaseFinite {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.intervalBetaFinite {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.intervalBetaNoetherian {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.intervalBetaEnoughProjectives {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
      CategoryTheory.EnoughProjectives (FGModuleCat (S.standardFormIntervalAlgebra m)ᵐᵒᵖ)
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instEnoughProjectivesFGModuleCatMulOpposite_1 {A : Type u} [Ring A] :
      CategoryTheory.EnoughProjectives (FGModuleCat Aᵐᵒᵖ)
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInterval_betaAt_le {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (hz : ¬CategoryTheory.Projective (S.fgObj z)) :
      FiniteTauMatrix.betaAt S.finiteTauCategoryData.toFiniteRightTauCategoryData z ≤ FiniteTauMatrix.beta (S.standardFormIntervalSkeleton (S.standardFormIntervalControlHeight + 2)).finiteTauCategoryData.toFiniteRightTauCategoryData

      Each original nonprojective endpoint's beta count is bounded by the single interval's beta, using the actual graded incoming sequence.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.beta_le_standardFormInterval_beta {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ FiniteTauMatrix.beta (S.standardFormIntervalSkeleton (S.standardFormIntervalControlHeight + 2)).finiteTauCategoryData.toFiniteRightTauCategoryData

      The manuscript's one-sided transfer, with the original algebra's beta already identified with its standard form by the arrow occurrence labels.