The quotient equivalence underlying the coherent-defect comparison

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantPresentationToCoherentDualLinearEquiv {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} (hK : K.ShortExact) (X : S.IndecCategory) : ((K.X₁.obj ⟶ (S.fgObj X).obj) ⧸ S.finiteCovariantPresentationRange K X) ≃ₗ[k] CategoryTheory.Abelian.Ext (S.finiteContravariantDefect K) (S.finiteContravariantRepresentableOnSkeleton.obj X) 2

The ambient module-presentation quotient is canonically the degree-two Ext group defining the coherent dual.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantPresentationToCoherentDualLinearEquiv_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} (hK : K.ShortExact) (X : S.IndecCategory) (f : K.X₁.obj ⟶ (S.fgObj X).obj) : (S.finiteCovariantPresentationToCoherentDualLinearEquiv hK X) (Submodule.Quotient.mk f) = (S.finiteCovariantRepresentableToCoherentDualLinear hK X) f