The represented factor in the standard mesh-simple resolution

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshHomCoordinateFactorMapQuiver {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.standardFormMeshHomCoordinateFactorMapArrowFintype {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)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSimpleResolutionYonedaFactor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hP : S.standardFormRightMeshData.FiniteContravariantRepresentables) (z x : Fin S.n) (t : MeshCategory.obj S.standardFormRightMeshData z ⟶ MeshCategory.obj S.standardFormRightMeshData x) : S.standardFormRightMeshData.contravariantRepresentableFiniteModule hP z ⟶ S.standardFormRightMeshData.contravariantRepresentableFiniteModule hP x

The finite representable morphism induced by a morphism between the corresponding vertices of the mesh category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSimpleResolutionYonedaFactor_hom_hom {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hP : S.standardFormRightMeshData.FiniteContravariantRepresentables) (z x : Fin S.n) (t : MeshCategory.obj S.standardFormRightMeshData z ⟶ MeshCategory.obj S.standardFormRightMeshData x) : (S.standardFormSimpleResolutionYonedaFactor hP z x t).hom.hom = (CategoryTheory.linearYoneda k S.standardFormRightMeshData.VertexCategory).map (CategoryTheory.InducedCategory.homMk t)

The underlying natural transformation of the represented factor is the Yoneda image of its mesh-category morphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSimpleResolutionYonedaCoefficient_eq_comp_factor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hP : S.standardFormRightMeshData.FiniteContravariantRepresentables) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) (x : Fin S.n) (h : S.standardFormRightMeshData.incomingCoefficientFiniteModule hP ↑z ⟶ S.standardFormRightMeshData.contravariantRepresentableFiniteModule hP x) (t : MeshCategory.obj S.standardFormRightMeshData ↑z ⟶ MeshCategory.obj S.standardFormRightMeshData x) (ht : ∀ (a : MeshCategory.RightMeshData.IncomingArrow ↑z), (S.standardFormSimpleResolutionYonedaCoefficient hP z x h a).hom = CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.incomingArrowHom a) t) (a : MeshCategory.RightMeshData.IncomingArrow ↑z) : S.standardFormSimpleResolutionYonedaCoefficient hP z x h a = CategoryTheory.CategoryStruct.comp (CategoryTheory.InducedCategory.homMk (S.standardFormRightMeshData.incomingArrowHom a)) (CategoryTheory.InducedCategory.homMk t)

A lifted raw mesh factor gives the corresponding equality in the induced vertex category.