Standard affine charts of the quotient Grassmannian (source code)

= Standard affine charts of the quotient Grassmannian
{title2=$U_I\cong\mathbb A^{r(n-r)}$}

Choose $r$ of the $n$ <basis> vectors and require their images in the quotient to be a <basis>. Normalize those columns to the identity; the remaining $r(n-r)$ entries are arbitrary affine coordinates. Between column sets $I,J$, the overlap is the <principal open subset> where $\det A_J$ is a unit, and the new normalized <matrix> is $A_J^{-1}A$. These <matrix> transformations satisfy the cocycle identity. Locally every surjective <matrix> has an invertible maximal minor, so the charts cover all rank-$r$ locally free quotients. The normalized <matrices> glue the universal quotient and give the natural identification with its <functor of points>.

// Target: ringed-space.bigb