Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardIntervalCategorySurplus

Intrinsic category surplus for the actual standard-form intervals #

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalCategoryBaseFinite {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.intervalCategoryAlgebraFinite {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.intervalCategoryAlgebraNoetherian {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
@[instance_reducible]
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalCategoryFintype {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.intervalCategoryOpFintype {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.standardFormIntervalCategory_finiteRepresentables {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 for the actual standard-form interval category.

      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalCategoryAlgebraEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
      CoveringHom.FiniteDimensionalModuleCategory k ≌ FinitelyGeneratedCategory (S.standardFormIntervalAlgebra m)

      Actual interval category modules and the named interval algebra have the same module category.

      Instances For
        source
        instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalCategoryAlgebraEquivalence_additive {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
        (S.standardFormIntervalCategoryAlgebraEquivalence m).functor.Additive
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalCategory_repFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
        CoveringHom.IsLocallyRepresentationFinite

        The classified interval algebra skeleton gives local representation finiteness.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalCategory_directed {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
        CoveringHom.HasAcyclicFiniteModuleNonzeroNonisomorphisms

        The shift rank proves directedness of the actual interval functor-module category.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalCategory_surplus_eq {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
        CoveringHom.finiteCategorySurplus ⋯ ⋯ = (S.standardFormIntervalSkeleton m).ambientARSurplus

        The category surplus in the packing theorem is the existing interval algebra surplus.