Reassembly from incoming biproduct coordinates

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshHomCoordinateAssemblyQuiver {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.standardFormMeshHomCoordinateAssemblyArrowFintype {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.standardFormSimpleResolution_hom_eq_of_coordinates {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) (b : S.standardFormRightMeshData.contravariantRepresentableFiniteModule hP ↑z ⟶ S.standardFormRightMeshData.contravariantRepresentableFiniteModule hP x) (hcoordinate : ∀ (a : MeshCategory.RightMeshData.IncomingArrow ↑z), CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.incomingSummandInclusionFinite hP (↑z) a) (CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.incomingMapFinite hP ↑z) b) = CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.incomingSummandInclusionFinite hP (↑z) a) h) : CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.incomingMapFinite hP ↑z) b = h

Equality on every incoming biproduct coordinate determines the whole morphism.