The quadratic bound on preprojective relations

Every local preprojective relation is a linear combination of length-two backtracks. Thus the preprojective relation ideal lies in the square of the arrow ideal of the doubled path algebra. This is the upper bound in admissibility; finite-dimensional Dynkin cases also need a lower bound by some arrow-ideal power.

theorem TauCeti.preprojectiveIdeal_le_arrowIdeal_sq (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : TwoSidedIdeal.asIdeal (preprojectiveIdeal k Q) ≤ arrowIdeal k (Quiver.Symmetrify Q) ^ 2

The preprojective relation ideal is contained in the square of the arrow ideal. Every term of the global relator is a backtrack of length two.

theorem TauCeti.preprojectiveMk_vertexIdempotent_ne_zero (k : Type w) {Q : Type u} [CommRing k] [Nontrivial k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Quiver.Symmetrify Q) : (preprojectiveMk k Q) (PathAlgebra.vertexIdempotent k i) ≠ 0

The vertex idempotents survive in the preprojective algebra: over a nontrivial ring the class of a vertex idempotent is nonzero, since the relation ideal lies in the square of the arrow ideal, which contains no vertex idempotent.