theorem DVRContext.one_mem_IwahoriGLn (C : DVRContext) [C.DVRClosureGL2] (n : ℕ) : 1 ∈ C.IwahoriGLn n

The identity matrix lies in the Iwahori subgroup of $\mathrm{GL}_n(k)$.

theorem DVRContext.one_mem_LowerUnipGLn (C : DVRContext) [C.DVRClosureGL2] (n : ℕ) : 1 ∈ C.LowerUnipGLn n

The identity matrix is lower unitriangular.

theorem DVRContext.one_mem_UpperUnipGLn (C : DVRContext) [C.DVRClosureGL2] (n : ℕ) : 1 ∈ C.UpperUnipGLn n

The identity matrix is upper unitriangular.

theorem DVRContext.iwahoriDecompositionGLn (C : DVRContext) [C.DVRClosureGL2] (n : ℕ) (b : GL (Fin n) C.k) : b ∈ C.IwahoriGLn n → ∃! triple : GL (Fin n) C.k × GL (Fin n) C.k × GL (Fin n) C.k, match triple with | (u', m, u) => u' ∈ C.LowerUnipGLn n ∩ C.IwahoriGLn n ∧ m ∈ C.DiagGLn n ∩ C.IwahoriGLn n ∧ u ∈ C.UpperUnipGLn n ∩ C.IwahoriGLn n ∧ b = u' * m * u

Iwahori decomposition for $\mathrm{GL}_n(k)$: every element of the Iwahori subgroup $I$ admits a unique factorisation $b = u' \cdot m \cdot u$ as a product of a lower unitriangular matrix $u' \in N^{\mathrm{op}} \cap I$, a diagonal matrix $m \in M \cap I$, and an upper unitriangular matrix $u \in N \cap I$.