Restricted-covariant-representable precomposition

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableMap_precomp {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} {X Y : S.IndecCategoryᵒᵖ} (a : X ⟶ Y) (f : (S.fgObj (Opposite.unop X)).obj ⟶ K.X₃.obj) : S.finiteRestrictedCovariantRepresentableMap (CategoryTheory.ObjectProperty.homMk (CategoryTheory.CategoryStruct.comp (S.fgMap a.unop).hom f)) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedCovariantRepresentableMap (CategoryTheory.ObjectProperty.homMk f)) (S.finiteCovariantRepresentableOnSkeleton.map a)

Restricted covariant Yoneda converts precomposition of module maps into postcomposition of natural transformations.