Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleBasicSimpleDimension

Simple dimensions for a complete primitive-projective presentation #

A complete orthogonal family decomposes every right module into its idempotent coordinates. When the family contains exactly one primitive projective from each selected isomorphism class, algebraic closedness makes every simple right module one-dimensional. Consequently a semisimple module of composition length at most two has ground-field dimension at most two.

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.instModuleCarrierMulOpposite_magnitudeConjecture {k A : Type u} [Field k] [Ring A] [Algebra k A] (X : FinitelyGeneratedCategory A) :
Module k ↑X
Instances For
    source
    theorem MagnitudeConjecture.RightModule.instIsScalarTowerMulOppositeCarrier_magnitudeConjecture {k A : Type u} [Field k] [Ring A] [Algebra k A] (X : FinitelyGeneratedCategory A) :
    IsScalarTower k Aᵐᵒᵖ ↑X
    source
    theorem MagnitudeConjecture.RightModule.instFiniteCarrierMulOpposite_magnitudeConjecture {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (X : FinitelyGeneratedCategory A) :
    Module.Finite k ↑X
    source
    def MagnitudeConjecture.RightModule.completeIdempotentCoordinateEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (X : FinitelyGeneratedCategory A) {I : Type u_1} [Fintype I] (e : I → A) (hall : CompleteOrthogonalIdempotents e) :
    ↑X ≃ₗ[k] (i : I) → ↥(idempotentCoordinate (e i) X)

    A complete orthogonal idempotent family decomposes a right module into the product of its idempotent coordinates.

    Instances For
      source
      theorem MagnitudeConjecture.RightModule.finrank_eq_sum_finrank_idempotentCoordinate {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (X : FinitelyGeneratedCategory A) {I : Type u_1} [Fintype I] (e : I → A) (hall : CompleteOrthogonalIdempotents e) :
      Module.finrank k ↑X = ∑ i : I, Module.finrank k ↥(idempotentCoordinate (e i) X)

      Ground-field dimension is the sum of the dimensions of all coordinates of a complete orthogonal idempotent family.

      source
      @[instance_reducible]
      def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgRestrictedModule {k A : Type u} [Field k] [Ring A] [Algebra k A] (X : FinitelyGeneratedCategory A) :
      Module k ↑X
      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgRestrictedScalarTower {k A : Type u} [Field k] [Ring A] [Algebra k A] (X : FinitelyGeneratedCategory A) :
        IsScalarTower k Aᵐᵒᵖ ↑X
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finrank_hom_projectiveSimpleTop_self_eq_one_of_isAlgClosed {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) :
        Module.finrank k (S.fgObj p.label ⟶ S.projectiveSimpleTop p) = 1

        The Hom space from an indecomposable projective to its simple top is one-dimensional over an algebraically closed field.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.finrank_projectiveSimpleTop_eq_one {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) :
        Module.finrank k ↑(S.projectiveSimpleTop p) = 1

        A complete primitive-projective presentation makes every selected simple top one-dimensional over the algebraically closed ground field.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.finrank_eq_one_of_isSimpleModule {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (hX : IsSimpleModule Aᵐᵒᵖ ↑X) :
        Module.finrank k ↑X = 1

        Every simple right module over an algebra with a complete primitive-projective presentation is one-dimensional.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.finrank_le_two_of_semisimple_of_length_le_two {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) [IsSemisimpleModule Aᵐᵒᵖ ↑X] (hle : Module.length Aᵐᵒᵖ ↑X ≤ 2) :
        Module.finrank k ↑X ≤ 2

        On a basic algebra presented by a complete primitive family, a semisimple module of composition length at most two has vector-space dimension at most two.