Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleProjectivePresentationHom

Hom exactness for the chosen right-module presentation #

This file packages precomposition by the two arrows of a two-step minimal projective presentation as linear maps. Exactness of the presentation gives the exact Hom sequence used in the stable Hom--Ext pairing.

source
def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.augmentationPrecompLinear {k B : Type u} [Field k] [Ring B] [Algebra k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) :
(X ⟶ Y) →ₗ[k] P.augmentation.p ⟶ Y

Precomposition with the augmentation P₀ ⟶ X.

Instances For
    source
    noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.differentialPrecompLinear {k B : Type u} [Field k] [Ring B] [Algebra k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) :
    (P.augmentation.p ⟶ Y) →ₗ[k] P.syzygyPresentation.p ⟶ Y

    Precomposition with the differential P₁ ⟶ P₀.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.augmentationPrecompLinear_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ᵐᵒᵖ) (f : X ⟶ Y) :
      (P.augmentationPrecompLinear Y) f = CategoryTheory.CategoryStruct.comp P.augmentation.f f
      source
      @[simp]
      theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.differentialPrecompLinear_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ᵐᵒᵖ) (f : P.augmentation.p ⟶ Y) :
      (P.differentialPrecompLinear Y) f = CategoryTheory.CategoryStruct.comp P.differential f
      source
      theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.augmentationPrecompLinear_injective {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ᵐᵒᵖ) :
      Function.Injective ⇑(P.augmentationPrecompLinear Y)

      Precomposition with the epimorphic augmentation is injective.

      source
      theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.range_augmentationPrecompLinear {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ᵐᵒᵖ) :
      (P.augmentationPrecompLinear Y).range = (P.differentialPrecompLinear Y).ker

      Applying Hom(-,Y) to the presentation is exact at Hom(P₀,Y).