Named morphisms in the mesh coordinate-factor calculation

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshHomCoordinateFactorMorphismsQuiver {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.standardFormMeshHomCoordinateFactorMorphismsArrowFintype {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.standardFormSimpleResolutionIncomingYonedaFactorComposite {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) (a : MeshCategory.RightMeshData.IncomingArrow z) : (CategoryTheory.linearYoneda k S.standardFormRightMeshData.VertexCategory).obj a.fst ⟶ (CategoryTheory.linearYoneda k S.standardFormRightMeshData.VertexCategory).obj x

The incoming mesh coordinate followed by the represented factor.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSimpleResolutionYonedaFactorComposite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z x : Fin S.n) (t : MeshCategory.obj S.standardFormRightMeshData z ⟶ MeshCategory.obj S.standardFormRightMeshData x) (a : MeshCategory.RightMeshData.IncomingArrow z) : (CategoryTheory.linearYoneda k S.standardFormRightMeshData.VertexCategory).obj a.fst ⟶ (CategoryTheory.linearYoneda k S.standardFormRightMeshData.VertexCategory).obj x

The Yoneda image of the composite defining one lifted coordinate.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSimpleResolutionYonedaCoefficientMap {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) (a : MeshCategory.RightMeshData.IncomingArrow ↑z) : (CategoryTheory.linearYoneda k S.standardFormRightMeshData.VertexCategory).obj (have this := a.fst; this) ⟶ (CategoryTheory.linearYoneda k S.standardFormRightMeshData.VertexCategory).obj (have this := x; this)

The Yoneda image of the coordinate extracted from the finite-module morphism.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSimpleResolutionFiniteCoordinateComposite {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) (a : MeshCategory.RightMeshData.IncomingArrow ↑z) : (S.standardFormRightMeshData.contravariantRepresentableFiniteModule hP a.fst).obj.obj ⟶ (S.standardFormRightMeshData.contravariantRepresentableFiniteModule hP x).obj.obj

The underlying natural transformation of the original finite-module coordinate composite.