theorem DVRContext.sum_lower_row (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : Matrix (Fin n) (Fin n) C.k) (h : Fin n → C.k) (i : Fin n) (hdiag : g i i = 1) (hzero : ∀ (k : Fin n), ↑k > ↑i → g i k = 0) : ∑ k : Fin n, g i k * h k = h i + ∑ k : Fin n with ↑k < ↑i, g i k * h k

Decomposition of a dot-product when row $i$ of $g$ is lower-triangular with $1$ on the diagonal: $\sum_k g_{ik} h_k = h_i + \sum_{k < i} g_{ik} h_k$.

theorem DVRContext.inv_lower_unip_above (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) (hdiag : ∀ (i : Fin n), ↑g i i = 1) (habove : ∀ (i j : Fin n), ↑i < ↑j → ↑g i j = 0) (i j : Fin n) (hij : ↑i < ↑j) : ↑g⁻¹ i j = 0

Inverse of a lower unitriangular matrix vanishes strictly above the diagonal (recomputed inside this file for the clearing-algorithm proofs).

theorem DVRContext.inv_lower_unip_diag (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) (hdiag : ∀ (i : Fin n), ↑g i i = 1) (habove : ∀ (i j : Fin n), ↑i < ↑j → ↑g i j = 0) (i : Fin n) : ↑g⁻¹ i i = 1

Diagonal entries of the inverse of a lower unitriangular matrix are $1$ (local recomputation).

theorem DVRContext.inv_lower_unip_below_in_maxideal (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) (hg_lower : g ∈ C.LowerUnipGLn n) (hg_iwahori : g ∈ C.IwahoriGLn n) (i j : Fin n) (hij : ↑i > ↑j) : C.isInMaxIdeal (↑g⁻¹ i j)

For a lower unitriangular Iwahori matrix $g$, the strictly-below-diagonal entries of $g^{-1}$ lie in the maximal ideal $\mathfrak m$.

theorem DVRContext.lower_unip_iwahori_inv_mem (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) (hg_lower : g ∈ C.LowerUnipGLn n) (hg_iwahori : g ∈ C.IwahoriGLn n) : g⁻¹ ∈ C.LowerUnipGLn n ∧ g⁻¹ ∈ C.IwahoriGLn n

The inverse of a lower unitriangular Iwahori matrix is again lower unitriangular and Iwahori: the lower-unipotent Iwahori subgroup is closed under taking inverses.

theorem DVRContext.sum_upper_col (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : Matrix (Fin n) (Fin n) C.k) (h : Fin n → C.k) (j : Fin n) (hdiag : g j j = 1) (hzero : ∀ (k : Fin n), ↑k > ↑j → g k j = 0) : ∑ k : Fin n, h k * g k j = h j + ∑ k : Fin n with ↑k < ↑j, h k * g k j

Decomposition of a dot-product when column $j$ of $g$ is upper-triangular with $1$ on the diagonal: $\sum_k h_k g_{kj} = h_j + \sum_{k < j} h_k g_{kj}$.

theorem DVRContext.inv_upper_unip_below (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) (hdiag : ∀ (i : Fin n), ↑g i i = 1) (hbelow : ∀ (i j : Fin n), ↑i > ↑j → ↑g i j = 0) (i j : Fin n) (hij : ↑i > ↑j) : ↑g⁻¹ i j = 0

Inverse of an upper unitriangular matrix vanishes strictly below the diagonal (recomputed inside this file for the clearing-algorithm proofs).

theorem DVRContext.inv_upper_unip_diag (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) (hdiag : ∀ (i : Fin n), ↑g i i = 1) (hbelow : ∀ (i j : Fin n), ↑i > ↑j → ↑g i j = 0) (i : Fin n) : ↑g⁻¹ i i = 1

Diagonal entries of the inverse of an upper unitriangular matrix are $1$ (local recomputation).

theorem DVRContext.inv_upper_unip_above_in_O (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) (hg_upper : g ∈ C.UpperUnipGLn n) (hg_iwahori : g ∈ C.IwahoriGLn n) (i j : Fin n) (hij : ↑i < ↑j) : C.isInO (↑g⁻¹ i j)

For an upper unitriangular Iwahori matrix $g$, the strictly-above-diagonal entries of $g^{-1}$ lie in the integers $\mathcal O$.

theorem DVRContext.upper_unip_iwahori_inv_mem (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) (hg_upper : g ∈ C.UpperUnipGLn n) (hg_iwahori : g ∈ C.IwahoriGLn n) : g⁻¹ ∈ C.UpperUnipGLn n ∧ g⁻¹ ∈ C.IwahoriGLn n

The inverse of an upper unitriangular Iwahori matrix is again upper unitriangular and Iwahori: the upper-unipotent Iwahori subgroup is closed under taking inverses.

theorem DVRContext.lower_unip_iwahori_mul_mem (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g h : GL (Fin n) C.k) (hg_lower : g ∈ C.LowerUnipGLn n) (hg_iwahori : g ∈ C.IwahoriGLn n) (hh_lower : h ∈ C.LowerUnipGLn n) (hh_iwahori : h ∈ C.IwahoriGLn n) : g * h ∈ C.LowerUnipGLn n ∧ g * h ∈ C.IwahoriGLn n

The product of two lower unitriangular Iwahori matrices is again lower unitriangular and Iwahori: the lower-unipotent Iwahori subgroup is closed under multiplication.

theorem DVRContext.upper_unip_iwahori_mul_mem (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g h : GL (Fin n) C.k) (hg_upper : g ∈ C.UpperUnipGLn n) (hg_iwahori : g ∈ C.IwahoriGLn n) (hh_upper : h ∈ C.UpperUnipGLn n) (hh_iwahori : h ∈ C.IwahoriGLn n) : g * h ∈ C.UpperUnipGLn n ∧ g * h ∈ C.IwahoriGLn n

The product of two upper unitriangular Iwahori matrices is again upper unitriangular and Iwahori: the upper-unipotent Iwahori subgroup is closed under multiplication.

theorem DVRContext.clear_first_column_aux (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin (n + 1)) C.k) (hg : g ∈ C.IwahoriGLn (n + 1)) (m : ℕ) (hm : m ≤ n) : ∃ L ∈ C.LowerUnipGLn (n + 1), L ∈ C.IwahoriGLn (n + 1) ∧ (∀ (i : Fin (n + 1)), 0 < ↑i ∧ ↑i ≤ m → ↑(L * g) i 0 = 0) ∧ ↑(L * g) 0 0 = ↑g 0 0

Inductive auxiliary for the first-column clearing step: there exists a lower unitriangular Iwahori matrix $L$ such that $(L \cdot g)_{i, 0} = 0$ for all $0 < i \le m$ while preserving the $(0, 0)$-entry of $g$.

theorem DVRContext.clear_first_column (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (hn : n ≥ 1) (g : GL (Fin (n + 1)) C.k) (hg : g ∈ C.IwahoriGLn (n + 1)) : ∃ L ∈ C.LowerUnipGLn (n + 1), L ∈ C.IwahoriGLn (n + 1) ∧ (∀ (i : Fin (n + 1)), ↑i > 0 → ↑(L * g) i 0 = 0) ∧ ↑(L * g) 0 0 = ↑g 0 0

First-column clearing: for any Iwahori matrix $g$, there exists a lower unitriangular Iwahori matrix $L$ such that $L \cdot g$ has zeros in every entry of the first column below the $(0,0)$ position, while preserving the $(0, 0)$-entry.

theorem DVRContext.clear_first_row (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (hn : n ≥ 1) (g : GL (Fin (n + 1)) C.k) (hg : g ∈ C.IwahoriGLn (n + 1)) (hcol : ∀ (i : Fin (n + 1)), ↑i > 0 → ↑g i 0 = 0) : ∃ U ∈ C.UpperUnipGLn (n + 1), U ∈ C.IwahoriGLn (n + 1) ∧ (∀ (j : Fin (n + 1)), ↑j > 0 → ↑(g * U) 0 j = 0) ∧ (∀ (i : Fin (n + 1)), ↑i > 0 → ↑(g * U) i 0 = 0) ∧ ↑(g * U) 0 0 = ↑g 0 0

First-row clearing: given an Iwahori matrix $g$ whose first column is already cleared, there exists an upper unitriangular Iwahori matrix $U$ such that $g \cdot U$ has zeros in the first row to the right of the $(0,0)$ position, while preserving the first column and the $(0, 0)$-entry.

theorem DVRContext.extract_lower_right_block (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (hn : n ≥ 1) (g : GL (Fin (n + 1)) C.k) (hg : g ∈ C.IwahoriGLn (n + 1)) (hcol : ∀ (i : Fin (n + 1)), ↑i > 0 → ↑g i 0 = 0) (hrow : ∀ (j : Fin (n + 1)), ↑j > 0 → ↑g 0 j = 0) : ∃ D ∈ C.IwahoriGLn n, ∀ (i j : Fin n), ↑D i j = ↑g ⟨↑i + 1, ⋯⟩ ⟨↑j + 1, ⋯⟩

Extract the lower-right $n \times n$ block of a cleared $(n+1) \times (n+1)$ Iwahori matrix: given that $g$ has zero first column and first row off the diagonal, the lower-right block is an Iwahori element of $\mathrm{GL}_n(k)$.

theorem DVRContext.block_diag_decomp (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (hn : n ≥ 1) (g : GL (Fin (n + 1)) C.k) (hg : g ∈ C.IwahoriGLn (n + 1)) (hcol : ∀ (i : Fin (n + 1)), ↑i > 0 → ↑g i 0 = 0) (hrow : ∀ (j : Fin (n + 1)), ↑j > 0 → ↑g 0 j = 0) (D : GL (Fin n) C.k) (hD : D ∈ C.IwahoriGLn n) (hD_entries : ∀ (i j : Fin n), ↑D i j = ↑g ⟨↑i + 1, ⋯⟩ ⟨↑j + 1, ⋯⟩) (u'_n m_n u_n : GL (Fin n) C.k) (hu'_n : u'_n ∈ C.LowerUnipGLn n ∩ C.IwahoriGLn n) (hm_n : m_n ∈ C.DiagGLn n ∩ C.IwahoriGLn n) (hu_n : u_n ∈ C.UpperUnipGLn n ∩ C.IwahoriGLn n) (hD_eq : D = u'_n * m_n * u_n) : ∃ (u'_big : GL (Fin (n + 1)) C.k) (m_big : GL (Fin (n + 1)) C.k) (u_big : GL (Fin (n + 1)) C.k), u'_big ∈ C.LowerUnipGLn (n + 1) ∩ C.IwahoriGLn (n + 1) ∧ m_big ∈ C.DiagGLn (n + 1) ∩ C.IwahoriGLn (n + 1) ∧ u_big ∈ C.UpperUnipGLn (n + 1) ∩ C.IwahoriGLn (n + 1) ∧ g = u'_big * m_big * u_big

Lift an $n \times n$ Iwahori decomposition of the lower-right block $D$ of a cleared $(n + 1) \times (n + 1)$ Iwahori matrix $g$ back to an Iwahori decomposition of $g$ itself via the block embedding.

theorem DVRContext.iwahori_inductive_step (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (hn : n ≥ 1) (g : GL (Fin (n + 1)) C.k) (hg : g ∈ C.IwahoriGLn (n + 1)) (ih : ∀ 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) : ∃ (triple : GL (Fin (n + 1)) C.k × GL (Fin (n + 1)) C.k × GL (Fin (n + 1)) C.k), match triple with | (u', m, u) => u' ∈ C.LowerUnipGLn (n + 1) ∩ C.IwahoriGLn (n + 1) ∧ m ∈ C.DiagGLn (n + 1) ∩ C.IwahoriGLn (n + 1) ∧ u ∈ C.UpperUnipGLn (n + 1) ∩ C.IwahoriGLn (n + 1) ∧ g = u' * m * u

Inductive step of the Iwahori decomposition: assuming existence of the decomposition for $n$, derive existence for $n + 1$ by clearing the first row and column and applying the induction hypothesis to the lower-right block.