Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormGlobalDimension

Global dimension of the standard-form mesh module category #

The standard-form mesh simples exhaust the simple finite modules. Their mesh resolutions therefore give a projective-dimension bound of two for all simple objects, and finite length propagates that bound to every finite module.

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGlobalDimensionQuiver {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.standardFormGlobalDimensionArrowFintype {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.standardFormFiniteContravariantRepresentables {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.standardFormRightMeshData.FiniteContravariantRepresentables

      Every contravariant representable of the full standard-form mesh category is finite-dimensional.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormVertexCategoryEndLocal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : S.standardFormRightMeshData.VertexCategory) :
      IsLocalRing (CategoryTheory.End X)

      Every vertex of the full standard-form mesh category has local endomorphism ring.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOppositeVertexCategoryEndLocal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : S.standardFormRightMeshData.VertexCategoryᵒᵖ) :
      IsLocalRing (CategoryTheory.End X)

      Local vertex endomorphism rings pass to the opposite vertex category used for contravariant finite modules.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_iso_standardFormSimpleFiniteModule_of_simple {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) [CategoryTheory.Simple M] :
      ∃ (z : Fin S.n), Nonempty (M ≅ S.standardFormRightMeshData.simpleFiniteModule z)

      Every simple object of the standard-form finite mesh-module category is one of the vertex mesh simples.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSimpleObject_hasProjectiveDimensionLE_two {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) [CategoryTheory.Simple M] :
      CategoryTheory.HasProjectiveDimensionLE M 2

      Every simple object of the standard-form finite mesh-module category has projective dimension at most two.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormFiniteModule_hasProjectiveDimensionLE_two {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) :
      CategoryTheory.HasProjectiveDimensionLE M 2

      Every finite-dimensional module on the standard-form mesh category has projective dimension at most two.