Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStableHomExt

Stable Hom--Ext duality for the Nakayama kernel #

For a chosen two-step minimal projective presentation

P₁ ⟶ P₀ ⟶ X,

this file proves the presentation-dependent Auslander--Reiten formula

Ext¹(Y, ker(νP₁ ⟶ νP₀)) ≃ Dₖ stableHom(X,Y).

The proof uses the concrete finite-projective Nakayama--Hom equivalence and only the one-sided stable Hom quotient needed here.

source
theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.instInjective {k : Type u} [Field k] :
Module.Injective k k
source
noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.ordinaryBoundaryLinear {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) :
(Y ⟶ P.nakayamaCokernel) →ₗ[k] (X ⟶ Y) →ₗ[k] k

The Nakayama boundary pairing before either variable is quotiented.

Instances For
    source
    @[simp]
    theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.ordinaryBoundaryLinear_apply {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) (c : Y ⟶ P.nakayamaCokernel) (f : X ⟶ Y) :
    ((P.ordinaryBoundaryLinear Y) c) f = ((RightModule.fieldNakayamaHomEquiv P.augmentation.p Y) (CategoryTheory.CategoryStruct.comp c P.nakayamaCokernelι)) (CategoryTheory.CategoryStruct.comp P.augmentation.f f)
    source
    theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.fieldNakayamaHomEquiv_differential {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) (a : Y ⟶ RightModule.projectiveNakayamaFGObj P.syzygyPresentation.p) (f : P.augmentation.p ⟶ Y) :
    ((RightModule.fieldNakayamaHomEquiv P.augmentation.p Y) (CategoryTheory.CategoryStruct.comp a P.nakayamaDifferential)) f = ((RightModule.fieldNakayamaHomEquiv P.syzygyPresentation.p Y) a) (CategoryTheory.CategoryStruct.comp P.differential f)

    The Nakayama--Hom comparison intertwines the presentation differential.

    source
    theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.ordinaryBoundaryLinear_naturality {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) {Y Z : FGModuleCat Bᵐᵒᵖ} (g : Y ⟶ Z) (c : Z ⟶ P.nakayamaCokernel) (f : X ⟶ Y) :
    ((P.ordinaryBoundaryLinear Y) (CategoryTheory.CategoryStruct.comp g c)) f = ((P.ordinaryBoundaryLinear Z) c) (CategoryTheory.CategoryStruct.comp f g)

    Naturality of the unquotiented pairing in its variable module.

    source
    theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.ordinaryBoundaryLinear_eq_zero_of_mem_presentationRange {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) (c : Y ⟶ P.nakayamaCokernel) (hc : c ∈ P.nakayamaExtPresentationRange Y) :
    (P.ordinaryBoundaryLinear Y) c = 0

    The pairing kills the displayed injective-presentation coboundaries.

    source
    theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.ordinaryBoundaryLinear_apply_eq_zero_of_factorsThroughProjective {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) (c : Y ⟶ P.nakayamaCokernel) {f : X ⟶ Y} (hf : RightModule.FactorsThroughProjective f) :
    ((P.ordinaryBoundaryLinear Y) c) f = 0

    The pairing kills maps from X which factor through a projective.

    source
    noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.stableBoundary {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) (c : Y ⟶ P.nakayamaCokernel) :
    RightModule.projectiveStableHom X Y →ₗ[k] k

    The boundary functional descended to projective-stable Hom.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.stableBoundary_mk {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) (c : Y ⟶ P.nakayamaCokernel) (f : X ⟶ Y) :
      (P.stableBoundary Y c) (RightModule.projectiveStableClass f) = ((P.ordinaryBoundaryLinear Y) c) f
      source
      noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.stableBoundaryLinear {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) :
      (Y ⟶ P.nakayamaCokernel) →ₗ[k] RightModule.projectiveStableHom X Y →ₗ[k] k

      The stable boundary, linear in its presentation representative.

      Instances For
        source
        noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.boundaryQuotientLinear {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) :
        (Y ⟶ P.nakayamaCokernel) ⧸ P.nakayamaExtPresentationRange Y →ₗ[k] RightModule.projectiveStableHom X Y →ₗ[k] k

        The pairing after quotienting its presentation variable.

        Instances For
          source
          @[simp]
          theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.boundaryQuotientLinear_mk_mk {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) (c : Y ⟶ P.nakayamaCokernel) (f : X ⟶ Y) :
          ((P.boundaryQuotientLinear Y) (Submodule.Quotient.mk c)) (RightModule.projectiveStableClass f) = ((P.ordinaryBoundaryLinear Y) c) f
          source
          theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.ker_ordinaryBoundaryLinear {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) :
          (P.ordinaryBoundaryLinear Y).ker = P.nakayamaExtPresentationRange Y

          The kernel of the unquotiented boundary is precisely the displayed injective-presentation range.

          source
          theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.boundaryQuotientLinear_injective {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) :
          Function.Injective ⇑(P.boundaryQuotientLinear Y)

          The descended boundary is injective.

          source
          theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.boundaryQuotientLinear_surjective {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) :
          Function.Surjective ⇑(P.boundaryQuotientLinear Y)

          Every functional on projective-stable Hom is a boundary functional.

          source
          noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.boundaryQuotientLinearEquiv {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) :
          ((Y ⟶ P.nakayamaCokernel) ⧸ P.nakayamaExtPresentationRange Y) ≃ₗ[k] RightModule.projectiveStableHom X Y →ₗ[k] k

          The presentation quotient is the coefficient dual of stable Hom.

          Instances For
            source
            noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.stableHomExtLinearEquiv {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) :
            CategoryTheory.Abelian.Ext Y P.nakayamaKernel 1 ≃ₗ[k] RightModule.projectiveStableHom X Y →ₗ[k] k

            The fixed-presentation stable Auslander--Reiten formula.

            Instances For
              source
              theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.stableHomExtLinearEquiv_naturality {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) {Y Z : FGModuleCat Bᵐᵒᵖ} (g : Y ⟶ Z) (xi : CategoryTheory.Abelian.Ext Z P.nakayamaKernel 1) (a : RightModule.projectiveStableHom X Y) :
              ((P.stableHomExtLinearEquiv Y) ((CategoryTheory.Abelian.Ext.mk₀ g).comp xi ⋯)) a = ((P.stableHomExtLinearEquiv Z) xi) ((RightModule.projectiveStablePostcomp X g) a)

              Naturality of the stable Auslander--Reiten formula under pullback.