Naturality of coherent-defect dimension shifting

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectDimensionShiftLinearEquiv_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) (x : CategoryTheory.Abelian.Ext (S.finiteContravariantDefectSyzygy K) (S.finiteContravariantRepresentableOnSkeleton.obj X) 1) : (S.finiteContravariantDefectDimensionShiftLinearEquiv hK Y) (x.comp (CategoryTheory.Abelian.Ext.mk₀ (S.finiteContravariantRepresentableOnSkeleton.map a)) ⋯) = ((S.finiteContravariantDefectDimensionShiftLinearEquiv hK X) x).comp (CategoryTheory.Abelian.Ext.mk₀ (S.finiteContravariantRepresentableOnSkeleton.map a)) ⋯

The specialized dimension shift commutes with postcomposition in the restricted representable target.