Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-07
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.

The Grassmannian is smooth, irreducible, and has dimension r(n-r)

Statement

For 0≤r≤n, Gr⁡(r,V) is smooth in the elementary local-affine-chart sense, irreducible, and has dimension r(n−r).

Facts & Assumptions

Given: An n-dimensional vector space V over the page's algebraically closed field k, and 0≤r≤n.

[F1]

The loci UI={pI≠0} cover the Plucker image and are isomorphic to Akr(n−r) by polynomial minors with regular ratio inverses (Standard affine charts on the Grassmannian).

[F2]

The Plucker image is a closed projective algebraic set (The Plucker image is a closed projective algebraic set).

Proof

1.1F1given

By [F1], each point has an affine-space neighbourhood of dimension r(n−r). This proves smoothness in the stated local-chart sense and the dimension assertion. If r=0 or r=n, there is just one subspace, so all the assertions hold for a point. Assume 0<r<n henceforth.

2.1F1step 1.1construct

Fix I0={1,…,r}. In its chart write a plane as the row space of (Ir∣A). For any r-subset J, retain the identity columns indexed by J∩I0 and assign the columns indexed by J∖I0 bijectively to the remaining standard basis vectors of kr. Complete the other columns of A arbitrarily. The minor indexed by J is then 1 or −1. Thus UJ∩UI0 is a nonempty open subset of both irreducible affine charts.

3.1F1F2step 2.1∎

Each intersection in step 2.1 is dense in UJ, since UJ is irreducible. Hence the closure of the irreducible set UI0 contains every UJ, and so is the whole Grassmannian. A closure of an irreducible set is irreducible. The chart isomorphisms in [F1] are for the Plucker-image topology itself (their maps are polynomial minors with regular inverses), so this proves irreducibility in that topology. Together with [F2], it makes the image a projective subvariety.

Depends on

Used by

Dependency tree · two levels

6 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