Dimension shifting for a coherent defect

This leaf specializes the generic projective-middle dimension shift to the right half of the four-term representable resolution of a coherent defect.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectDimensionShiftLinearEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt S.FiniteContravariantFunctor] {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) (X : S.IndecCategory) : CategoryTheory.Abelian.Ext (S.finiteContravariantDefectSyzygy K) (S.finiteContravariantRepresentableOnSkeleton.obj X) 1 ≃ₗ[k] CategoryTheory.Abelian.Ext (S.finiteContravariantDefect K) (S.finiteContravariantRepresentableOnSkeleton.obj X) 2

Dimension shifting across the right half of the four-term representable resolution.