Proof of `Homomorphism polynomials span matrix-symmetric polynomials`
groundedproofs/Lax461425Proofs/HomomorphismSpanning.lean · lax-461425
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Partition the monomial support into distinct orbits. Each orbit sum is an embedding polynomial divided by its nonzero automorphism factor; partition Möbius inversion expresses it in the bounded-vertex homomorphism span, as in DPS, Lemma 4 and Corollary A.3.