Naturality of the reverse coherent-defect comparison

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantRepresentableToCoherentCodual {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.FiniteCovariantFunctor] {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) : S.finiteContravariantFunctorInclusion.obj (S.finiteRestrictedContravariantRepresentable K.X₃) ⟶ S.coherentCodualObj (S.finiteCovariantDefect K)

The unquotiented reverse comparison is a natural transformation.