The degree-two Ext calculation for a coherent defect

The two short exact halves of the representable resolution identify the intrinsic degree-two Ext group with the quotient computed from the left representable presentation.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectPresentationLinearEquiv {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) : (((S.finiteContravariantDefectLeftShortComplex K).X₁ ⟶ S.finiteContravariantRepresentableOnSkeleton.obj X) ⧸ ProjectivePresentationExt.presentationRange (S.finiteContravariantDefectLeftShortComplex K) (S.finiteContravariantRepresentableOnSkeleton.obj X)) ≃ₗ[k] CategoryTheory.Abelian.Ext (S.finiteContravariantDefect K) (S.finiteContravariantRepresentableOnSkeleton.obj X) 2

The two short exact halves compute the intrinsic degree-two Ext group as the quotient attached to the left representable presentation.