Yoneda coefficient data for the standard-form mesh resolution

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshYonedaDataQuiver {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.standardFormMeshYonedaDataArrowFintype {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.standardFormSimpleResolutionYonedaCoefficient {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) : (have this := a.fst; this) ⟶ have this := x; this

The mesh-category morphism represented by one coordinate of a morphism out of the incoming coefficient module.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSimpleResolutionPairedIncoming {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) (a : MeshCategory.RightMeshData.IncomingArrow ↑z) : (have this := S.standardFormRightMeshData.tau z; this) ⟶ have this := a.fst; this

The polarized partner of an incoming arrow in the induced vertex category.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.linearYoneda_map_standardFormSimpleResolutionYonedaCoefficient {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).map (S.standardFormSimpleResolutionYonedaCoefficient hP z x h a) = (CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.incomingSummandInclusionFinite hP (↑z) a) h).hom.hom