def DVRContext.IwahoriGLn (C : DVRContext) (n : ℕ) : Set (GL (Fin n) C.k)

The Iwahori subgroup $I \subseteq \mathrm{GL}_n(k)$: matrices whose diagonal entries are units of $\mathcal O$, strictly-above-diagonal entries lie in $\mathcal O$, and strictly-below-diagonal entries lie in the maximal ideal $\mathfrak m$.

def DVRContext.UpperUnipGLn (C : DVRContext) (n : ℕ) : Set (GL (Fin n) C.k)

The upper unipotent subgroup $N \subseteq \mathrm{GL}_n(k)$: upper unitriangular matrices, i.e. matrices with $1$s on the diagonal and $0$s strictly below it.

def DVRContext.LowerUnipGLn (C : DVRContext) (n : ℕ) : Set (GL (Fin n) C.k)

The lower unipotent subgroup $N^{\mathrm{op}} \subseteq \mathrm{GL}_n(k)$: lower unitriangular matrices, i.e. matrices with $1$s on the diagonal and $0$s strictly above it.

def DVRContext.DiagGLn (C : DVRContext) (n : ℕ) : Set (GL (Fin n) C.k)

The diagonal subgroup $M \subseteq \mathrm{GL}_n(k)$: matrices that vanish off the diagonal.