Additive-hull lift of incoming coefficient families

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormARIncomingAdditiveLiftQuiver {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.standardFormARIncomingAdditiveLiftArrowFintype {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.standardFormIncomingCoefficientAdditiveLift {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) (coeff : S.standardFormRightMeshData.IncomingCoefficient x z) : S.standardFormRightMeshData.additiveVertexObj x ⟶ S.standardFormRightMeshData.additiveIncomingObj z

The one-row additive-hull matrix represented by an incoming coefficient family.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIncomingCoefficientAdditiveLift_comp_incomingMap {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) (coeff : S.standardFormRightMeshData.IncomingCoefficient x z) : CategoryTheory.CategoryStruct.comp (S.standardFormIncomingCoefficientAdditiveLift x z coeff) (S.standardFormRightMeshData.additiveIncomingMap z) = (S.standardFormRightMeshData.additiveVertexHomLinearEquiv x z).symm (S.standardFormRightMeshData.incomingSum coeff)

The additive coefficient lift composed with the incoming matrix is the singleton matrix represented by the mesh-category incoming sum.