Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleGeneratedAtIdempotent

Modules generated by their idempotent coordinate #

source
def MagnitudeConjecture.RightModule.coordinateGeneratedSubmodule {k A : Type u} [Field k] [Ring A] [Algebra k A] (e : A) (X : FinitelyGeneratedCategory A) :
Submodule Aᵐᵒᵖ ↑X

The right submodule generated by Xe.

Instances For
    source
    def MagnitudeConjecture.RightModule.IsGeneratedAtIdempotent {k A : Type u} [Field k] [Ring A] [Algebra k A] (e : A) (X : FinitelyGeneratedCategory A) :
    Prop

    Every element of X is generated by its coordinate Xe.

    Instances For
      source
      theorem MagnitudeConjecture.RightModule.hom_eq_zero_of_generated_at_idempotent {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) {X Y : FinitelyGeneratedCategory A} (hX : IsGeneratedAtIdempotent e X) (hY : ∀ (y : ↑Y), MulOpposite.op e • y = 0) (f : X ⟶ Y) :
      f = 0

      A map from a module generated at e to a module killed by e is zero.

      source
      def MagnitudeConjecture.RightModule.generatedCoordinateRelations {k A : Type u} [Field k] [Ring A] [Algebra k A] (e : A) (V : FinitelyGeneratedCategory A) (R : Submodule k ↥(idempotentCoordinate e V)) :
      Submodule Aᵐᵒᵖ ↑V

      The module generated by a vector-space set of relations inside Ve.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.generatedCoordinateRelations_le_ker {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {V W : FinitelyGeneratedCategory A} (R : Submodule k ↥(idempotentCoordinate e V)) (f : V ⟶ W) (hf : ∀ r ∈ R, (CategoryTheory.ConcreteCategory.hom f) ↑r = 0) :
        generatedCoordinateRelations e V R ≤ (ModuleCat.Hom.hom f.hom).ker

        A module map killing the coordinate relations kills the generated relation submodule.

        source
        def MagnitudeConjecture.RightModule.generatedCoordinateRelationsFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (V : FinitelyGeneratedCategory A) (R : Submodule k ↥(idempotentCoordinate e V)) :
        FinitelyGeneratedCategory A

        The generated relation submodule, bundled as a finite right module.

        Instances For
          source
          theorem MagnitudeConjecture.RightModule.generatedCoordinateRelations_isGenerated {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (V : FinitelyGeneratedCategory A) (R : Submodule k ↥(idempotentCoordinate e V)) :
          IsGeneratedAtIdempotent e (generatedCoordinateRelationsFGObj e V R)

          The relation module is itself generated at e, as required for the Ext-vanishing step of the realization.