Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStableHom

Projective-stable Hom spaces for right modules #

This file forms the scalar quotient of a right-module Hom space by maps factoring through finitely generated projectives. Only the one-sided projective-stable vector spaces and their postcomposition maps are retained; no unrelated stable-category infrastructure is imported.

source
structure MagnitudeConjecture.RightModule.FactorsThroughProjective {B : Type u} [Ring B] {X Y : FGModuleCat Bᵐᵒᵖ} (f : X ⟶ Y) :
Type (u + 1)

A morphism of finitely generated right modules factors through a finitely generated categorical projective.

  • middle : FGModuleCat Bᵐᵒᵖ
  • projective : CategoryTheory.Projective self.middle
  • left : X ⟶ self.middle
  • right : self.middle ⟶ Y
  • fac : CategoryTheory.CategoryStruct.comp self.left self.right = f
Instances For
    source
    def MagnitudeConjecture.RightModule.FactorsThroughProjective.zero {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] {X Y : FGModuleCat Bᵐᵒᵖ} :
    FactorsThroughProjective 0

    The zero map factors through the zero module.

    Instances For
      source
      noncomputable def MagnitudeConjecture.RightModule.FactorsThroughProjective.add {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] {X Y : FGModuleCat Bᵐᵒᵖ} {f g : X ⟶ Y} (hf : FactorsThroughProjective f) (hg : FactorsThroughProjective g) :
      FactorsThroughProjective (f + g)

      Projective factorizations are closed under addition.

      Instances For
        source
        def MagnitudeConjecture.RightModule.FactorsThroughProjective.smul {k B : Type u} [Field k] [Ring B] [Algebra k B] {X Y : FGModuleCat Bᵐᵒᵖ} {f : X ⟶ Y} (a : k) (hf : FactorsThroughProjective f) :
        FactorsThroughProjective (a • f)

        Projective factorizations are closed under scalar multiplication.

        Instances For
          source
          def MagnitudeConjecture.RightModule.FactorsThroughProjective.postcomp {B : Type u} [Ring B] {X Y Z : FGModuleCat Bᵐᵒᵖ} {f : X ⟶ Y} (hf : FactorsThroughProjective f) (g : Y ⟶ Z) :
          FactorsThroughProjective (CategoryTheory.CategoryStruct.comp f g)

          Postcomposition preserves projective factorization.

          Instances For
            source
            def MagnitudeConjecture.RightModule.FactorsThroughProjective.precomp {B : Type u} [Ring B] {W X Y : FGModuleCat Bᵐᵒᵖ} (g : W ⟶ X) {f : X ⟶ Y} (hf : FactorsThroughProjective f) :
            FactorsThroughProjective (CategoryTheory.CategoryStruct.comp g f)

            Precomposition preserves projective factorization.

            Instances For
              source
              def MagnitudeConjecture.RightModule.projectiveFactorSubmodule {k B : Type u} [Field k] [Ring B] [Algebra k B] [IsNoetherianRing Bᵐᵒᵖ] (X Y : FGModuleCat Bᵐᵒᵖ) :
              Submodule k (X ⟶ Y)

              The subspace of morphisms factoring through projectives.

              Instances For
                source
                @[reducible, inline]
                abbrev MagnitudeConjecture.RightModule.projectiveStableHom {k B : Type u} [Field k] [Ring B] [Algebra k B] [IsNoetherianRing Bᵐᵒᵖ] (X Y : FGModuleCat Bᵐᵒᵖ) :
                Type u

                The projective-stable Hom vector space.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev MagnitudeConjecture.RightModule.projectiveStableClass {k B : Type u} [Field k] [Ring B] [Algebra k B] [IsNoetherianRing Bᵐᵒᵖ] {X Y : FGModuleCat Bᵐᵒᵖ} :
                  (X ⟶ Y) →ₗ[k] projectiveStableHom X Y

                  The class of an ordinary morphism in projective-stable Hom.

                  Instances For
                    source
                    def MagnitudeConjecture.RightModule.projectiveStablePostcomp {k B : Type u} [Field k] [Ring B] [Algebra k B] [IsNoetherianRing Bᵐᵒᵖ] (X : FGModuleCat Bᵐᵒᵖ) {Y Z : FGModuleCat Bᵐᵒᵖ} (g : Y ⟶ Z) :
                    projectiveStableHom X Y →ₗ[k] projectiveStableHom X Z

                    Postcomposition on projective-stable Hom.

                    Instances For
                      source
                      @[simp]
                      theorem MagnitudeConjecture.RightModule.projectiveStablePostcomp_mk {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (X : FGModuleCat Bᵐᵒᵖ) {Y Z : FGModuleCat Bᵐᵒᵖ} (g : Y ⟶ Z) (f : X ⟶ Y) :
                      (projectiveStablePostcomp X g) (projectiveStableClass f) = projectiveStableClass (CategoryTheory.CategoryStruct.comp f g)
                      source
                      theorem MagnitudeConjecture.RightModule.projective_of_id_factorsThroughProjective {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (X : FGModuleCat Bᵐᵒᵖ) (h : FactorsThroughProjective (CategoryTheory.CategoryStruct.id X)) :
                      CategoryTheory.Projective X

                      If the identity factors through a projective, the module is projective.

                      source
                      theorem MagnitudeConjecture.RightModule.projectiveStableClass_id_ne_zero {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (X : FGModuleCat Bᵐᵒᵖ) (hX : ¬CategoryTheory.Projective X) :
                      projectiveStableClass (CategoryTheory.CategoryStruct.id X) ≠ 0

                      A nonprojective module has a nonzero stable identity class.