Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardGradedModules

Graded modules over the existing standard-form algebra #

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormHomModuleAction {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) (X : CategoryTheory.Mat_ S.StandardFormMeshCategory) :
Module (S.standardFormAlgebra hfinite)ᵐᵒᵖ (⨁ S.standardGradedProjectiveFamily ⟶ X)

Restrict the actual Hom-module action to the existing standard-form algebra.

Instances For
    source
    def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormHomModuleScalarTower {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) (X : CategoryTheory.Mat_ S.StandardFormMeshCategory) :
    IsScalarTower k (S.standardFormAlgebra hfinite)ᵐᵒᵖ (⨁ S.standardGradedProjectiveFamily ⟶ X)

    The transported right-module action is compatible with the original field scalars.

    Instances For
      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormHomModuleGrading {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) (X : CategoryTheory.Mat_ S.StandardFormMeshCategory) :
      Graded.ModuleGrading (S.standardFormOppositeAlgebraGrading hfinite)

      The homogeneous components define a grading over the existing standard-form algebra.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormHomModule_finite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) (X : CategoryTheory.Mat_ S.StandardFormMeshCategory) :
        FiniteDimensional k (⨁ S.standardGradedProjectiveFamily ⟶ X)

        These transported modules are finite-dimensional over the original field.

        source
        noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormHomModuleMap {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) {X Y : CategoryTheory.Mat_ S.StandardFormMeshCategory} (f : X ⟶ Y) :
        (⨁ S.standardGradedProjectiveFamily ⟶ X) →ₗ[(S.standardFormAlgebra hfinite)ᵐᵒᵖ] ⨁ S.standardGradedProjectiveFamily ⟶ Y

        Postcomposition as a map over the existing standard-form algebra.

        Instances For