Restricted Yoneda and the presentation quotient of a coherent defect

Restricted Yoneda identifies maps between the representables in Auslander's four-term resolution with ordinary module maps. This file proves that the identification carries the presentation coboundaries onto one another and therefore descends to the corresponding quotients.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectPresentationRange_map_yoneda {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] (K : CategoryTheory.ShortComplex FG) (X : S.IndecCategory) : Submodule.map (↑(S.ambientFiniteRestrictedContravariantRepresentableHomLinearEquiv K.X₁ X)) (S.finiteCovariantPresentationRange K X) = ProjectivePresentationExt.presentationRange (S.finiteContravariantDefectLeftShortComplex K) (S.finiteContravariantRepresentableOnSkeleton.obj X)

Restricted Yoneda carries the ordinary module-presentation coboundaries exactly onto the functor-presentation coboundaries.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectPresentationYonedaLinearEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] (K : CategoryTheory.ShortComplex FG) (X : S.IndecCategory) : ((K.X₁.obj ⟶ (S.fgObj X).obj) ⧸ S.finiteCovariantPresentationRange K X) ≃ₗ[k] ((S.finiteContravariantDefectLeftShortComplex K).X₁ ⟶ S.finiteContravariantRepresentableOnSkeleton.obj X) ⧸ ProjectivePresentationExt.presentationRange (S.finiteContravariantDefectLeftShortComplex K) (S.finiteContravariantRepresentableOnSkeleton.obj X)

The ordinary module-presentation quotient and the corresponding quotient of natural-transformation spaces are canonically linearly equivalent.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectPresentationYonedaLinearEquiv_mk {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] (K : CategoryTheory.ShortComplex FG) (X : S.IndecCategory) (f : K.X₁.obj ⟶ (S.fgObj X).obj) : (S.finiteContravariantDefectPresentationYonedaLinearEquiv K X) (Submodule.Quotient.mk f) = Submodule.Quotient.mk (S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.ObjectProperty.homMk f))