While this submission is a draft, it cannot be used by other submissions.

Proof of `The codimension-k Grassmannian as the closed part of the algebraic Grassmannian`

groundedproofs/Lax606786Proofs/GrassmannianComparison.lean · lax-606786

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.

Read the Lean proof on GitLab

Description

A subspace in 𝒱kX𝒱^k X has a finite-dimensional quotient of dimension kk, which over Rℝ is free of rank kk at the only prime; conversely a closed subspace with such a quotient is complemented, since its quotient is finite-dimensional.