Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleNakayamaEmbedding

Finite Nakayama evaluation embeddings #

Let P be a finite projective right module and Y a finite right module. Finite-dimensional Nakayama--Hom duality identifies maps

Y ⟶ νP

with linear functionals on Hom(P,Y). Choosing the coordinate functionals of a basis therefore gives a canonical finite family of maps from Y to copies of the injective module νP. Its kernel is the largest submodule of Y invisible to P.

This is the finite, explicit replacement for an arbitrary injective-envelope construction in Iyama's saturation argument.

source
@[reducible, inline]
noncomputable abbrev MagnitudeConjecture.RightModule.nakayamaEmbeddingHomBasis {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P Y : FGModuleCat Bᵐᵒᵖ) :
Module.Basis (Fin (Module.finrank k (P ⟶ Y))) k (P ⟶ Y)

The chosen finite basis of Hom(P,Y).

Instances For
    source
    noncomputable def MagnitudeConjecture.RightModule.nakayamaEmbeddingCoordinateMap {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] (i : Fin (Module.finrank k (P ⟶ Y))) :
    Y ⟶ projectiveNakayamaFGObj P

    The map Y ⟶ νP corresponding to one coordinate functional on Hom(P,Y).

    Instances For
      source
      noncomputable def MagnitudeConjecture.RightModule.nakayamaEmbeddingMap {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] :
      ↑Y →ₗ[Bᵐᵒᵖ] Fin (Module.finrank k (P ⟶ Y)) → ↑(projectiveNakayamaFGObj P)

      The simultaneous evaluation map into a finite product of copies of νP.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.RightModule.nakayamaEmbeddingMap_apply {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] (y : ↑Y) (i : Fin (Module.finrank k (P ⟶ Y))) :
        (nakayamaEmbeddingMap P Y) y i = (ModuleCat.Hom.hom (nakayamaEmbeddingCoordinateMap P Y i).hom) y
        source
        theorem MagnitudeConjecture.RightModule.hom_to_nakayamaEmbeddingKernel_eq_zero {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] (f : P ⟶ FGModuleCat.of Bᵐᵒᵖ ↥(nakayamaEmbeddingMap P Y).ker) :
        f = 0

        Every map from P to the kernel of simultaneous Nakayama evaluation is zero.

        source
        theorem MagnitudeConjecture.RightModule.nakayamaEmbeddingMap_injective {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] (hvisible : ∀ (N : Submodule Bᵐᵒᵖ ↑Y), (∀ (f : P ⟶ FGModuleCat.of Bᵐᵒᵖ ↥N), f = 0) → N = ⊥) :
        Function.Injective ⇑(nakayamaEmbeddingMap P Y)

        If Y has no nonzero submodule invisible to P, simultaneous Nakayama evaluation embeds Y into a finite product of copies of νP.

        source
        theorem MagnitudeConjecture.RightModule.nakayamaEmbeddingTarget_projectiveDimensionLE_one {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P Y : FGModuleCat Bᵐᵒᵖ) (hnu : CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of Bᵐᵒᵖ ↑(projectiveNakayamaFGObj P)) 1) :
        CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of Bᵐᵒᵖ (Fin (Module.finrank k (P ⟶ Y)) → ↑(projectiveNakayamaFGObj P))) 1

        A finite product of copies of νP has projective dimension at most one whenever νP does.