Stable Hom--Ext duality for finite linear-module categories

For a literal two-step finite-representable projective presentation

P₁ ⟶ P₀ ⟶ M,

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

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

The proof uses the finite-matrix Nakayama--Hom equivalence and the one-sided categorical projective-stable quotient.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.instInjective {k : Type v} [Field k] : Module.Injective k k

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.augmentationPrecompLinear {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : (M ⟶ Y) →ₗ[k] P.augmentation.source ⟶ Y

Precomposition with the augmentation P₀ ⟶ M.

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.differentialPrecompLinear {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : (P.augmentation.source ⟶ Y) →ₗ[k] P.syzygyPresentation.source ⟶ Y

Precomposition with the first differential P₁ ⟶ P₀.

@[simp]

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.augmentationPrecompLinear_apply {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) (f : M ⟶ Y) : (P.augmentationPrecompLinear Y) f = CategoryTheory.CategoryStruct.comp P.augmentation.f f

@[simp]

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.differentialPrecompLinear_apply {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) (f : P.augmentation.source ⟶ Y) : (P.differentialPrecompLinear Y) f = CategoryTheory.CategoryStruct.comp P.toTwoStepFiniteRepresentablePresentation.differential f

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.augmentationPrecompLinear_injective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : Function.Injective ⇑(P.augmentationPrecompLinear Y)

Precomposition with the epimorphic augmentation is injective.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.range_augmentationPrecompLinear {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : (P.augmentationPrecompLinear Y).range = (P.differentialPrecompLinear Y).ker

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

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.ordinaryBoundaryLinear {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : (Y ⟶ nakayamaCokernel hI P) →ₗ[k] (M ⟶ Y) →ₗ[k] k

The Nakayama boundary pairing before quotienting either variable.

@[simp]

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.ordinaryBoundaryLinear_apply {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) (c : Y ⟶ nakayamaCokernel hI P) (f : M ⟶ Y) : ((ordinaryBoundaryLinear hI P Y) c) f = ((finiteRepresentableSumNakayamaHomEquiv hP hI P.augmentation.matrixObject Y) (CategoryTheory.CategoryStruct.comp c (nakayamaCokernelι hI P))) (CategoryTheory.CategoryStruct.comp P.augmentation.f f)

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.map_representingDifferential {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) : (finiteProjectiveRepresentableSumFunctor hP).map P.representingDifferential = P.toTwoStepFiniteRepresentablePresentation.differential

The projective matrix functor sends the named representing differential to the actual first differential of the presentation.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.map_representingDifferential_comp_augmentation {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) : CategoryTheory.CategoryStruct.comp ((finiteProjectiveRepresentableSumFunctor hP).map P.representingDifferential) P.augmentation.f = 0

The mapped representing differential followed by the augmentation is zero.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.finiteRepresentableSumNakayamaHomEquiv_differential {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) (a : Y ⟶ (finiteNakayamaRepresentableSumFunctor hI).obj P.syzygyPresentation.matrixObject) (f : P.augmentation.source ⟶ Y) : ((finiteRepresentableSumNakayamaHomEquiv hP hI P.augmentation.matrixObject Y) (CategoryTheory.CategoryStruct.comp a (nakayamaDifferential hI P))) f = ((finiteRepresentableSumNakayamaHomEquiv hP hI P.syzygyPresentation.matrixObject Y) a) (CategoryTheory.CategoryStruct.comp ((finiteProjectiveRepresentableSumFunctor hP).map P.representingDifferential) f)

The finite-matrix Nakayama--Hom comparison intertwines the displayed projective and Nakayama differentials.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.ordinaryBoundaryLinear_naturality {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) {Y Z : FiniteDimensionalModuleCategory k} (g : Y ⟶ Z) (c : Z ⟶ nakayamaCokernel hI P) (f : M ⟶ Y) : ((ordinaryBoundaryLinear hI P Y) (CategoryTheory.CategoryStruct.comp g c)) f = ((ordinaryBoundaryLinear hI P Z) c) (CategoryTheory.CategoryStruct.comp f g)

Naturality of the unquotiented boundary pairing in the variable module.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.ordinaryBoundaryLinear_eq_zero_of_mem_presentationRange {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) (c : Y ⟶ nakayamaCokernel hI P) (hc : c ∈ nakayamaExtPresentationRange hI P Y) : (ordinaryBoundaryLinear hI P Y) c = 0

The pairing kills the displayed injective-presentation coboundaries.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.ordinaryBoundaryLinear_apply_eq_zero_of_factorsThroughProjective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) (c : Y ⟶ nakayamaCokernel hI P) {f : M ⟶ Y} (hf : ProjectiveStable.FactorsThroughProjective f) : ((ordinaryBoundaryLinear hI P Y) c) f = 0

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

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.stableBoundary {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) (c : Y ⟶ nakayamaCokernel hI P) : ProjectiveStable.Hom M Y →ₗ[k] k

The boundary functional descended to projective-stable Hom.

@[simp]

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.stableBoundary_mk {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) (c : Y ⟶ nakayamaCokernel hI P) (f : M ⟶ Y) : (stableBoundary hI P Y c) (ProjectiveStable.mk f) = ((ordinaryBoundaryLinear hI P Y) c) f

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.stableBoundaryLinear {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : (Y ⟶ nakayamaCokernel hI P) →ₗ[k] ProjectiveStable.Hom M Y →ₗ[k] k

The stable boundary, linear in its presentation representative.

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.boundaryQuotientLinear {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : (Y ⟶ nakayamaCokernel hI P) ⧸ nakayamaExtPresentationRange hI P Y →ₗ[k] ProjectiveStable.Hom M Y →ₗ[k] k

The pairing after quotienting its presentation variable.

@[simp]

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.boundaryQuotientLinear_mk_mk {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) (c : Y ⟶ nakayamaCokernel hI P) (f : M ⟶ Y) : ((boundaryQuotientLinear hI P Y) (Submodule.Quotient.mk c)) (ProjectiveStable.mk f) = ((ordinaryBoundaryLinear hI P Y) c) f

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.ker_ordinaryBoundaryLinear {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : (ordinaryBoundaryLinear hI P Y).ker = nakayamaExtPresentationRange hI P Y

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

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.boundaryQuotientLinear_injective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : Function.Injective ⇑(boundaryQuotientLinear hI P Y)

The descended boundary is injective.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.boundaryQuotientLinear_surjective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : Function.Surjective ⇑(boundaryQuotientLinear hI P Y)

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

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.boundaryQuotientLinearEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : ((Y ⟶ nakayamaCokernel hI P) ⧸ nakayamaExtPresentationRange hI P Y) ≃ₗ[k] ProjectiveStable.Hom M Y →ₗ[k] k

The concrete Ext presentation quotient is the coefficient dual of projective-stable Hom.

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.stableHomExtLinearEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (Y : FiniteDimensionalModuleCategory k) : CategoryTheory.Abelian.Ext Y (nakayamaKernel hI P) 1 ≃ₗ[k] ProjectiveStable.Hom M Y →ₗ[k] k

The fixed-presentation stable Auslander--Reiten formula in the finite linear-module category.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.stableHomExtLinearEquiv_naturality {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) {Y Z : FiniteDimensionalModuleCategory k} (g : Y ⟶ Z) (xi : CategoryTheory.Abelian.Ext Z (nakayamaKernel hI P) 1) (a : ProjectiveStable.Hom M Y) : ((stableHomExtLinearEquiv hI P Y) ((CategoryTheory.Abelian.Ext.mk₀ g).comp xi ⋯)) a = ((stableHomExtLinearEquiv hI P Z) xi) ((ProjectiveStable.postcomp M g) a)

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