The independent and production bound-quiver presentations agree

The free path categories, generated ideals, and quotient linear structures agree definitionally. Evaluating at a stationary path identifies the path coordinates. Uniqueness of a finite direct sum identifies the category algebras, giving explicit translations in both directions.

theorem MagnitudeConjecture.Statement.QuiverPresentation.coefficients_eq {k Q : Type u} [Field k] [Quiver Q] {X Y : FreeCategory k Q} (f : X ⟶ Y) : coefficients k Q f = (LinearPathCategory.homPathLinearEquiv X Y) f

theorem MagnitudeConjecture.Statement.QuiverPresentation.pathHom_eq {k Q : Type u} [Field k] [Quiver Q] {x y : Q} (p : Quiver.Path x y) : pathHom k Q p = LinearPathCategory.pathHom p

theorem MagnitudeConjecture.Statement.QuiverPresentation.pathMap_eq {k Q : Type u} [Field k] [Quiver Q] (R : BoundQuiver.RelationFamily k Q) {x y : Q} (p : Quiver.Path x y) : pathMap R p = BoundQuiver.pathMap R p

theorem MagnitudeConjecture.Statement.QuiverPresentation.Presentation.admissible {k Q B : Type u} [Field k] [Quiver Q] [Ring B] [Algebra k B] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : Presentation B) : BoundQuiver.IsAdmissible P.relations

The independent ideal conditions are exactly production admissibility.

noncomputable def MagnitudeConjecture.Statement.QuiverPresentation.Presentation.toProduction {k Q B : Type u} [Field k] [Quiver Q] [Ring B] [Algebra k B] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : Presentation B) : BoundQuiver.SpecialBiserialPresentation k B Q

Recover the production presentation using uniqueness of finite direct sums.

noncomputable def MagnitudeConjecture.Statement.QuiverPresentation.ofProduction {k Q B : Type u} [Field k] [Quiver Q] [Ring B] [Algebra k B] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (P : BoundQuiver.SpecialBiserialPresentation k B Q) : Presentation B

Express a production bound-quiver presentation in the independent vocabulary.