TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Polynomial invariants of the full orthogonal and symplectic groups

Statement

Assume the Axiom of Choice (The Axiom of Choice).

Let $k$ be algebraically closed of characteristic zero. For the full orthogonal group $O (V, B)$ of a nondegenerate symmetric $m$ -dimensional space, the invariant ring $k [V^{t}]^{O (V, B)}$ is generated by $q_{i j} = B (v_{i}, v_{j})$ and the kernel of $k [z_{i j} : i \leq j] \to k [V^{t}]$ , $z_{i j} \mapsto q_{i j}$ , is the ideal of all $(m + 1)$ -minors of the generic symmetric Gram matrix. For the full symplectic group $S p (V, ω)$ of a nondegenerate alternating $2 n$ -dimensional space, $k [V^{t}]^{S p (V, ω)}$ is generated by $q_{i j} = ω (v_{i}, v_{j})$ for $i < j$ , and the kernel of $k [a_{i j} : i < j] \to k [V^{t}]$ is generated by all principal Pfaffians of size $2 n + 2$ of the generic alternating Gram matrix. In both branches the claims concern the algebraic-group coaction invariants defined in Polynomial invariants of a rational algebraic-group action, not invariants under a finite subgroup of $G (k)$ .

Facts & Assumptions

Given: The Axiom of Choice and the algebraic-group invariant convention in Polynomial invariants of a rational algebraic-group action, the Gram-map range in Gram-map image, full-rank fibers, and rank-stratum dimensions, and the local rank-ring and torsor/descent obligations in Exact symmetric-minor and alternating-Pfaffian rank ideals and Full-rank Gram torsor descent and extension across lower-rank strata.

[F1]

Exact symmetric-minor and alternating-Pfaffian rank ideals: the Gram rank varieties have precisely the stated prime, normal minor/Pfaffian coordinate rings.

[F2]

Gram-map image, full-rank fibers, and rank-stratum dimensions: the Gram map has image exactly the stated rank-bounded variety.

[F3]

Full-rank Gram torsor descent and extension across lower-rank strata: full-rank invariant regular functions descend and extend uniquely.

[F4]

Strong Nullstellensatz: I(V(I)) equals the radical of I: under AC, for an ideal $I$ of a finite-variable polynomial ring over algebraically closed $k$ , its closed-point vanishing ideal is $I (V (I)) = \sqrt{I}$ .

Proof

1.1givenF1F3algebra

If $V = 0$ , its tuple space has coordinate ring $k$ and both groups are trivial. The kernel of the Gram-coordinate map is the ideal of all entries, namely the $1$ -minor ideal in the symmetric case and the $2$ -Pfaffian ideal in the alternating case, so the result holds directly. Assume now $m = \dim V > 0$ and first take $t \geq m + 1$ . Every Gram coordinate is invariant under the full isometry group, by its defining equation. Conversely an invariant polynomial $f$ on $V^{t}$ restricts to an invariant regular function on the open set of spanning tuples. The Gram-torsor descent in [F3] gives a regular function on the rank- $m$ Gram locus; [F1] and the codimension-extension assertion of [F3] extend it to a unique element $h$ of the Gram rank ring. Choose a polynomial representative $H$ for $h$ . Then $f = H (q_{i j})$ on the spanning-tuples open set. This open is nonempty and dense in the affine space $V^{t}$ (some $m$ columns can be chosen as a basis), so the two polynomials agree everywhere. This proves generation in this range, by regular descent and extension rather than orbit separation alone.

2.1step 1.1algebra

For $0 \leq t < m + 1$ , add $m + 1 - t$ extra vector slots and view $f$ as a polynomial independent of them. It is still invariant for the diagonal action on the enlarged tuple. By step 1.1 it is a polynomial in all enlarged Gram coordinates. Set the extra vectors equal to zero. Every Gram coordinate using an added slot vanishes, and the remaining ones are the original $q_{i j}$ , proving generation for the original $t$ . This includes $t = 0$ , when the result is the scalar ring.

3.1F1F2F4step 1.1step 2.1algebra∎

A polynomial in formal Gram coordinates pulls back to zero exactly when it vanishes on all Gram matrices: surjectivity onto the rank-bounded set is proved in Gram-map image, full-rank fibers, and rank-stratum dimensions. By [F1] that set has the displayed prime minor or Pfaffian ideal. The strong Nullstellensatz in [F4] therefore makes its vanishing ideal that very ideal, since a prime ideal is radical. Thus the kernel is precisely the asserted ideal. When the rank bound exceeds the matrix size this is the zero ideal, as [F1] states. The descent in step 1.1 used the algebraic-group invariance equation, so the conclusion has exactly the coaction convention in the Statement.

Depends on

Used by

Multilinear orthogonal and symplectic FFT/SFT Theorem

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Lehrer and Zhang, The Brauer Category and Invariant Theory, Theorems 4.1 and 4.6 (standard reference, not scraped)
Goodman, Multiplicity-Free Spaces and Schur-Weyl-Howe Duality, §§6.4–6.5 (standard reference, not scraped)
Lakshmibai, Raghavan, Sankaran, and Shukla, Standard Monomial Bases, Moduli Spaces of Vector Bundles & Invariant Theory, §2 (standard reference, not scraped)