Finite trace-coordinate model on the stated loci

By [F2], choose a finite algebra generating list $f_1,\dots ,f_s$ for the character coordinate algebra. Each $f_j$ is a polynomial in finitely many word traces by [F1]. The union of these finitely many word lists is finite; denote it by $w_1,\dots ,w_N$. Their traces generate an algebra containing all $f_j$, hence the entire coordinate algebra. This establishes one fixed finite list for the quotient, rather than just a separate list for each function.

Send $z_i$ to $t_{w_i}$. Step 1.1 makes this polynomial-ring map onto the reduced invariant coordinate algebra. Its kernel is therefore radical. The actual affine coordinate-ring construction in [F2] identifies the quotient with the closed zero locus of that kernel in ${\mathbb{C}}^N$ and its point map with the displayed trace-coordinate map. Thus this is the asserted closed embedding with exactly the stated defining ideal.

Equal listed coordinates give equal values of every element of the coordinate algebra by step 1.1. In particular they give equal traces on every group word. The irreducible claim follows from [F3], including preservation of irreducibility. A reducible representation is triangular in an invariant-line basis, and [F3] gives its diagonal semisimplification with identical traces. Since the listed traces are the quotient coordinates, both have exactly the same quotient point. This records the semisimplified character and does not assert conjugacy of a nonsemisimple triangular representation to that diagonal one. All full-AC hypotheses are retained from [F1] and [F2]; the pointwise conjugacy argument adds no choice axiom.