Naturality of the coherent-defect Ext² calculation

The presentation-quotient calculation of Ext² commutes with postcomposition in the restricted representable target.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectPresentationLinearEquiv_postcomp {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 Y : S.IndecCategory} (a : X ⟶ Y) (q : ((S.finiteContravariantDefectLeftShortComplex K).X₁ ⟶ S.finiteContravariantRepresentableOnSkeleton.obj X) ⧸ ProjectivePresentationExt.presentationRange (S.finiteContravariantDefectLeftShortComplex K) (S.finiteContravariantRepresentableOnSkeleton.obj X)) : (S.finiteContravariantDefectPresentationLinearEquiv hK Y) ((ProjectivePresentationExt.postcompQuotient (S.finiteContravariantDefectLeftShortComplex K) (S.finiteContravariantRepresentableOnSkeleton.map a)) q) = ((CategoryTheory.Abelian.Ext.mk₀ (S.finiteContravariantRepresentableOnSkeleton.map a)).postcompOfLinear k (S.finiteContravariantDefect K) ⋯) ((S.finiteContravariantDefectPresentationLinearEquiv hK X) q)

Naturality of the quotient model for Ext² along a skeleton morphism.