theorem DVRContext.diag_mul_entry {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (d : GL (Fin n) C.k) (hd : d ∈ C.DiagGLn n) (A : Matrix (Fin n) (Fin n) C.k) (i j : Fin n) : (↑d * A) i j = ↑d i i * A i j

Left multiplication by a diagonal matrix scales rows: $(d \cdot A)_{ij} = d_{ii} \cdot A_{ij}$.

theorem DVRContext.mul_diag_entry {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (A : Matrix (Fin n) (Fin n) C.k) (d : GL (Fin n) C.k) (hd : d ∈ C.DiagGLn n) (i j : Fin n) : (A * ↑d) i j = A i j * ↑d j j

Right multiplication by a diagonal matrix scales columns: $(A \cdot d)_{ij} = A_{ij} \cdot d_{jj}$.

theorem DVRContext.diag_entry_ne_zero {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (d : GL (Fin n) C.k) (hd : d ∈ C.DiagGLn n) (i : Fin n) : ↑d i i ≠ 0

A diagonal matrix in $\mathrm{GL}_n$ has nonzero diagonal entries (else it would have a zero row, contradicting invertibility).

theorem DVRContext.diag_inv_mem {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (d : GL (Fin n) C.k) (hd : d ∈ C.DiagGLn n) : d⁻¹ ∈ C.DiagGLn n

The inverse of a diagonal matrix is diagonal.

theorem DVRContext.diag_inv_entry {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (d : GL (Fin n) C.k) (hd : d ∈ C.DiagGLn n) (i : Fin n) : ↑d⁻¹ i i = (↑d i i)⁻¹

The diagonal entries of the inverse of a diagonal matrix are the inverses of the corresponding entries: $(d^{-1})_{ii} = (d_{ii})^{-1}$.

theorem DVRContext.lower_unip_inv_above_aux {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (L : GL (Fin n) C.k) (hL : L ∈ C.LowerUnipGLn n) (hIL : ↑L⁻¹ * ↑L = 1) (d : ℕ) (j : Fin n) : n - ↑j ≤ d + 1 → ∀ (i : Fin n), ↑i < ↑j → ↑L⁻¹ i j = 0

Auxiliary induction on the descending distance $n - j$: for a lower unitriangular $L$, the inverse $L^{-1}$ has zero strictly-above-diagonal entries.

theorem DVRContext.lower_unip_inv_above {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (L : GL (Fin n) C.k) (hL : L ∈ C.LowerUnipGLn n) (i j : Fin n) (hij : ↑i < ↑j) : ↑L⁻¹ i j = 0

The inverse of a lower unitriangular matrix has zero strictly-above-diagonal entries.

theorem DVRContext.lower_unip_inv_diag {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (L : GL (Fin n) C.k) (hL : L ∈ C.LowerUnipGLn n) (i : Fin n) : ↑L⁻¹ i i = 1

The diagonal entries of the inverse of a lower unitriangular matrix are $1$.

theorem DVRContext.lower_unip_mul_diag {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (L1 L2 : GL (Fin n) C.k) (hL1 : L1 ∈ C.LowerUnipGLn n) (hL2 : L2 ∈ C.LowerUnipGLn n) (i : Fin n) : (↑L1 * ↑L2) i i = 1

The product of two lower unitriangular matrices has $1$ on the diagonal.

theorem DVRContext.lower_unip_mul_above {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (L1 L2 : GL (Fin n) C.k) (hL1 : L1 ∈ C.LowerUnipGLn n) (hL2 : L2 ∈ C.LowerUnipGLn n) (i j : Fin n) (hij : ↑i < ↑j) : (↑L1 * ↑L2) i j = 0

The product of two lower unitriangular matrices has zero strictly-above-diagonal entries.

theorem DVRContext.upper_unip_inv_below_aux {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (U : GL (Fin n) C.k) (hU : U ∈ C.UpperUnipGLn n) (hIU : ↑U⁻¹ * ↑U = 1) (d : ℕ) (j : Fin n) : ↑j ≤ d → ∀ (i : Fin n), ↑i > ↑j → ↑U⁻¹ i j = 0

Auxiliary induction on the column index $j$: for an upper unitriangular $U$, the inverse $U^{-1}$ has zero strictly-below-diagonal entries.

theorem DVRContext.upper_unip_inv_below {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (U : GL (Fin n) C.k) (hU : U ∈ C.UpperUnipGLn n) (i j : Fin n) (hij : ↑i > ↑j) : ↑U⁻¹ i j = 0

The inverse of an upper unitriangular matrix has zero strictly-below-diagonal entries.

theorem DVRContext.upper_unip_inv_diag {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (U : GL (Fin n) C.k) (hU : U ∈ C.UpperUnipGLn n) (i : Fin n) : ↑U⁻¹ i i = 1

The diagonal entries of the inverse of an upper unitriangular matrix are $1$.

theorem DVRContext.upper_unip_mul_diag {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (U1 U2 : GL (Fin n) C.k) (hU1 : U1 ∈ C.UpperUnipGLn n) (hU2 : U2 ∈ C.UpperUnipGLn n) (i : Fin n) : (↑U1 * ↑U2) i i = 1

The product of two upper unitriangular matrices has $1$ on the diagonal.

theorem DVRContext.upper_unip_mul_below {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (U1 U2 : GL (Fin n) C.k) (hU1 : U1 ∈ C.UpperUnipGLn n) (hU2 : U2 ∈ C.UpperUnipGLn n) (i j : Fin n) (hij : ↑i > ↑j) : (↑U1 * ↑U2) i j = 0

The product of two upper unitriangular matrices has zero strictly-below-diagonal entries.

theorem DVRContext.iwahori_decomp_unique {C : DVRContext} [C.DVRClosureGL2] {n : ℕ} (u_lo d_diag u_up v_lo e_diag v_up : GL (Fin n) C.k) (hu_lo : u_lo ∈ C.LowerUnipGLn n ∩ C.IwahoriGLn n) (hd : d_diag ∈ C.DiagGLn n ∩ C.IwahoriGLn n) (hu_up : u_up ∈ C.UpperUnipGLn n ∩ C.IwahoriGLn n) (hv_lo : v_lo ∈ C.LowerUnipGLn n ∩ C.IwahoriGLn n) (he : e_diag ∈ C.DiagGLn n ∩ C.IwahoriGLn n) (hv_up : v_up ∈ C.UpperUnipGLn n ∩ C.IwahoriGLn n) (heq : u_lo * d_diag * u_up = v_lo * e_diag * v_up) : u_lo = v_lo ∧ d_diag = e_diag ∧ u_up = v_up

Uniqueness of the Iwahori decomposition: if $u_\ell \cdot d \cdot u_u = v_\ell \cdot e \cdot v_u$ where both triples lie in the lower-unipotent / diagonal / upper-unipotent components of the Iwahori subgroup, then $u_\ell = v_\ell$, $d = e$, and $u_u = v_u$.