Restricted Yoneda on singleton additive-hull morphisms

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormARSingletonMapQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Quiver (Fin S.n)

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormARSingletonMapArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) : Fintype (x ⟶ y)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAdditiveRestrictedYoneda_singleton_map {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x z : Fin S.n) (f : MeshCategory.obj S.standardFormRightMeshData x ⟶ MeshCategory.obj S.standardFormRightMeshData z) : CategoryTheory.CategoryStruct.comp (S.standardFormAdditiveRestrictedYonedaSingletonIso x).inv (CategoryTheory.CategoryStruct.comp (S.standardFormAdditiveRestrictedYonedaFunctor.map ((S.standardFormRightMeshData.additiveVertexHomLinearEquiv x z).symm f)) (S.standardFormAdditiveRestrictedYonedaSingletonIso z).hom) = (S.standardFormRestrictedYonedaFunctor ⋯).map f

Mapping a singleton additive-hull matrix and transporting across the two singleton identifications recovers the original restricted-Yoneda map.