noncomputable def DVRContext.elimMatrix (C : DVRContext) {n : ℕ} (i j : Fin n) (hij : i ≠ j) (c : C.k) : GL (Fin n) C.k

The transvection / elementary matrix $E_{ij}(c) = 1 + c \cdot e_{ij}$ packaged as an element of $\mathrm{GL}_n(k)$, with explicit two-sided inverse $E_{ij}(-c)$.

@[simp]

theorem DVRContext.elimMatrix_val (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (i j : Fin n) (hij : i ≠ j) (c : C.k) : ↑(C.elimMatrix i j hij c) = Matrix.transvection i j c

The underlying matrix of elimMatrix C i j hij c is the transvection $E_{ij}(c)$.

theorem DVRContext.elim_matrix_mul (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (i j : Fin n) (c : C.k) (A : Matrix (Fin n) (Fin n) C.k) (b : Fin n) : (Matrix.transvection i j c * A) i b = A i b + c * A j b

Action of a transvection on a matrix from the left: in row $i$, the transvection adds $c$ times row $j$ to row $i$.

theorem DVRContext.elim_matrix_inv (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (i j : Fin n) (hij : i ≠ j) (c : C.k) : (C.elimMatrix i j hij c)⁻¹ = C.elimMatrix i j hij (-c)

The inverse of the elementary matrix $E_{ij}(c)$ is $E_{ij}(-c)$.

theorem DVRContext.elim_matrix_mul_ne (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (i j : Fin n) (c : C.k) (A : Matrix (Fin n) (Fin n) C.k) (a b : Fin n) (ha : a ≠ i) : (Matrix.transvection i j c * A) a b = A a b

Rows of a matrix other than row $i$ are unchanged by left-multiplication by the transvection $E_{ij}(c)$.

theorem DVRContext.elim_matrix_upper_unitriangular (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (i j : Fin n) (hij : i ≠ j) (hlt : ↑i < ↑j) (c : C.k) : C.elimMatrix i j hij c ∈ C.UpperUnipGLn n

An elementary matrix $E_{ij}(c)$ with $i < j$ is upper unitriangular.

theorem DVRContext.elim_matrix_lower_unitriangular (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (i j : Fin n) (hij : i ≠ j) (hgt : ↑i > ↑j) (c : C.k) : C.elimMatrix i j hij c ∈ C.LowerUnipGLn n

An elementary matrix $E_{ij}(c)$ with $i > j$ is lower unitriangular.

theorem DVRContext.elim_matrix_iwahori_upper (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (i j : Fin n) (hij : i ≠ j) (hlt : ↑i < ↑j) (c : C.k) (hc : C.isInO c) : C.elimMatrix i j hij c ∈ C.IwahoriGLn n

An upper elementary matrix $E_{ij}(c)$ with $i < j$ lies in the Iwahori subgroup whenever $c \in \mathcal O$.

theorem DVRContext.elim_matrix_iwahori_lower (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (i j : Fin n) (hij : i ≠ j) (hgt : ↑i > ↑j) (c : C.k) (hc : C.isInMaxIdeal c) : C.elimMatrix i j hij c ∈ C.IwahoriGLn n

A lower elementary matrix $E_{ij}(c)$ with $i > j$ lies in the Iwahori subgroup whenever $c \in \mathfrak m$.

noncomputable def DVRContext.finBlockEquiv (n : ℕ) : Fin 1 ⊕ Fin n ≃ Fin (n + 1)

Equivalence $\mathrm{Fin}\,1 \oplus \mathrm{Fin}\,n \simeq \mathrm{Fin}(n + 1)$ obtained by composing finSumFinEquiv with the natural cast $\mathrm{Fin}(1 + n) \simeq \mathrm{Fin}(n + 1)$.

theorem DVRContext.finBlockEquiv_inl (n : ℕ) : (finBlockEquiv n) (Sum.inl 0) = 0

finBlockEquiv sends the left summand Sum.inl 0 to $0 \in \mathrm{Fin}(n + 1)$.

theorem DVRContext.finBlockEquiv_inr (n : ℕ) (k : Fin n) : (finBlockEquiv n) (Sum.inr k) = ⟨↑k + 1, ⋯⟩

finBlockEquiv sends the right summand Sum.inr k to $k + 1 \in \mathrm{Fin}(n + 1)$.

theorem DVRContext.finBlockEquiv_symm_zero (n : ℕ) : (finBlockEquiv n).symm 0 = Sum.inl 0

The inverse of finBlockEquiv sends $0 \in \mathrm{Fin}(n + 1)$ to the left summand Sum.inl 0.

theorem DVRContext.finBlockEquiv_symm_succ (n : ℕ) (k : Fin n) : (finBlockEquiv n).symm ⟨↑k + 1, ⋯⟩ = Sum.inr k

The inverse of finBlockEquiv sends $k + 1 \in \mathrm{Fin}(n + 1)$ to the right summand Sum.inr k.

theorem DVRContext.fin_succ_cases {n : ℕ} (p : Fin (n + 1)) : p = 0 ∨ ∃ (k : Fin n), p = ⟨↑k + 1, ⋯⟩

Case analysis on $\mathrm{Fin}(n + 1)$: every element is either $0$ or of the form $k + 1$ for some $k \in \mathrm{Fin}\,n$.

noncomputable def DVRContext.blockEmbedMatrix (C : DVRContext) {n : ℕ} (A : Matrix (Fin n) (Fin n) C.k) : Matrix (Fin (n + 1)) (Fin (n + 1)) C.k

Block embedding $\mathrm{GL}_n \hookrightarrow \mathrm{GL}_{n+1}$ at the matrix level: place the $n \times n$ matrix $A$ in the lower-right corner of the $(n+1) \times (n+1)$ matrix and put a single $1$ in the upper-left corner.

theorem DVRContext.blockEmbedMatrix_zero_zero (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (A : Matrix (Fin n) (Fin n) C.k) : C.blockEmbedMatrix A 0 0 = 1

The $(0, 0)$-entry of blockEmbedMatrix C A is $1$.

theorem DVRContext.blockEmbedMatrix_zero_succ (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (A : Matrix (Fin n) (Fin n) C.k) (k : Fin n) : C.blockEmbedMatrix A 0 ⟨↑k + 1, ⋯⟩ = 0

The first row of blockEmbedMatrix C A vanishes outside the $(0, 0)$ entry.

theorem DVRContext.blockEmbedMatrix_succ_zero (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (A : Matrix (Fin n) (Fin n) C.k) (k : Fin n) : C.blockEmbedMatrix A ⟨↑k + 1, ⋯⟩ 0 = 0

The first column of blockEmbedMatrix C A vanishes outside the $(0, 0)$ entry.

theorem DVRContext.blockEmbedMatrix_succ_succ (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (A : Matrix (Fin n) (Fin n) C.k) (k l : Fin n) : C.blockEmbedMatrix A ⟨↑k + 1, ⋯⟩ ⟨↑l + 1, ⋯⟩ = A k l

The lower-right $n \times n$ block of blockEmbedMatrix C A is $A$ itself.

noncomputable def DVRContext.blockEmbedGL (C : DVRContext) {n : ℕ} (g : GL (Fin n) C.k) : GL (Fin (n + 1)) C.k

Block embedding $\mathrm{GL}_n(k) \hookrightarrow \mathrm{GL}_{n+1}(k)$ at the group level: upgrade blockEmbedMatrix to a unit by carrying the explicit inverse along.

@[simp]

theorem DVRContext.blockEmbedGL_val (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) : ↑(C.blockEmbedGL g) = C.blockEmbedMatrix ↑g

The underlying matrix of blockEmbedGL C g is blockEmbedMatrix C g.val.

theorem DVRContext.block_embed_preserves_iwahori (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) (hg : g ∈ C.IwahoriGLn n) : C.blockEmbedGL g ∈ C.IwahoriGLn (n + 1)

The block embedding preserves the Iwahori subgroup.

theorem DVRContext.block_embed_preserves_upper_unip (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) (hg : g ∈ C.UpperUnipGLn n) : C.blockEmbedGL g ∈ C.UpperUnipGLn (n + 1)

The block embedding preserves upper unitriangular matrices.

theorem DVRContext.block_embed_preserves_lower_unip (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) (hg : g ∈ C.LowerUnipGLn n) : C.blockEmbedGL g ∈ C.LowerUnipGLn (n + 1)

The block embedding preserves lower unitriangular matrices.

theorem DVRContext.isInMaxIdeal_add (C : DVRContext) [C.DVRClosureGL2] {x y : C.k} (hx : C.isInMaxIdeal x) (hy : C.isInMaxIdeal y) : C.isInMaxIdeal (x + y)

The maximal ideal $\mathfrak m$ is closed under addition.

theorem DVRContext.isInO_mul_isInMaxIdeal (C : DVRContext) [C.DVRClosureGL2] {x y : C.k} (hx : C.isInO x) (hy : C.isInMaxIdeal y) : C.isInMaxIdeal (x * y)

If $x \in \mathcal O$ and $y \in \mathfrak m$, then $xy \in \mathfrak m$ (the maximal ideal is an $\mathcal O$-module).

theorem DVRContext.isUnitInO_mul (C : DVRContext) [C.DVRClosureGL2] {x y : C.k} (hx : C.isUnitInO x) (hy : C.isUnitInO y) : C.isUnitInO (x * y)

The set of units of $\mathcal O$ is closed under multiplication.

theorem DVRContext.isUnitInO_add_isInMaxIdeal (C : DVRContext) [C.DVRClosureGL2] {x y : C.k} (hx : C.isUnitInO x) (hy : C.isInMaxIdeal y) : C.isUnitInO (x + y)

Adding an element of the maximal ideal to a unit of $\mathcal O$ still gives a unit of $\mathcal O$ (a unit plus a non-unit is a unit in a local ring).

theorem DVRContext.isInMaxIdeal_finset_sum (C : DVRContext) [C.DVRClosureGL2] {ι : Type u_1} {s : Finset ι} {f : ι → C.k} (hf : ∀ i ∈ s, C.isInMaxIdeal (f i)) : C.isInMaxIdeal (∑ i ∈ s, f i)

A finite sum of elements of the maximal ideal lies in the maximal ideal.

theorem DVRContext.isInO_finset_sum (C : DVRContext) [C.DVRClosureGL2] {ι : Type u_1} {s : Finset ι} {f : ι → C.k} (hf : ∀ i ∈ s, C.isInO (f i)) : C.isInO (∑ i ∈ s, f i)

A finite sum of elements of $\mathcal O$ lies in $\mathcal O$.

theorem DVRContext.iwahori_entry_isInO' (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) (hg : g ∈ C.IwahoriGLn n) (i j : Fin n) : C.isInO (↑g i j)

Every entry of an Iwahori matrix lies in $\mathcal O$: diagonal entries are units, above- diagonal entries are in $\mathcal O$ by definition, and below-diagonal entries are in $\mathfrak m \subseteq \mathcal O$.

theorem DVRContext.iwahori_entry_below' (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g : GL (Fin n) C.k) (hg : g ∈ C.IwahoriGLn n) {i j : Fin n} (hij : ↑i > ↑j) : C.isInMaxIdeal (↑g i j)

Re-extraction lemma: strictly-below-diagonal entries of an Iwahori matrix lie in $\mathfrak m$.

theorem DVRContext.IwahoriGLn_mul_mem (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (g h : GL (Fin n) C.k) (hg : g ∈ C.IwahoriGLn n) (hh : h ∈ C.IwahoriGLn n) : g * h ∈ C.IwahoriGLn n

The Iwahori subgroup of $\mathrm{GL}_n(k)$ is closed under multiplication.