Naturality of the coherent-defect comparison

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantRepresentableToCoherentDualLinear_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) (f : K.X₁.obj ⟶ (S.fgObj X).obj) : (S.finiteCovariantRepresentableToCoherentDualLinear hK Y) (CategoryTheory.CategoryStruct.comp f (S.fgMap a).hom) = ((CategoryTheory.Abelian.Ext.mk₀ (S.finiteContravariantRepresentableOnSkeleton.map a)).postcompOfLinear k (S.finiteContravariantDefect K) ⋯) ((S.finiteCovariantRepresentableToCoherentDualLinear hK X) f)

Naturality of the unquotiented comparison.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantRepresentableToCoherentDual {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) : S.finiteCovariantFunctorInclusion.obj (S.finiteRestrictedCovariantRepresentable K.X₁) ⟶ S.coherentDualObj (S.finiteContravariantDefect K)

The unquotiented comparison is a natural transformation.