noncomputable def DVRContext.scalarMat1 (C : DVRContext) (a : C.k) : Matrix (Fin 1) (Fin 1) C.k

The $1 \times 1$ matrix whose single entry is the scalar $a \in k$.

@[simp]

theorem DVRContext.scalarMat1_apply (C : DVRContext) [C.DVRClosureGL2] (a : C.k) (i j : Fin 1) : C.scalarMat1 a i j = a

Every entry of the $1 \times 1$ scalar matrix equals $a$.

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

The block-diagonal matrix $\mathrm{diag}(a, A)$ of size $(n+1) \times (n+1)$, putting the scalar $a$ in the top-left corner and the matrix $A$ in the bottom-right block.

@[simp]

theorem DVRContext.diagBlockEmbedMatrix_zero_zero (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (a : C.k) (A : Matrix (Fin n) (Fin n) C.k) : C.diagBlockEmbedMatrix a A 0 0 = a

The $(0,0)$ entry of $\mathrm{diag}(a, A)$ is $a$.

@[simp]

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

Top row, non-corner entries of $\mathrm{diag}(a, A)$ are zero.

@[simp]

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

Leftmost column, non-corner entries of $\mathrm{diag}(a, A)$ are zero.

@[simp]

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

The bottom-right $n \times n$ block of $\mathrm{diag}(a, A)$ is $A$.

noncomputable def DVRContext.diagBlockEmbedGL (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (a : C.kˣ) (M : GL (Fin n) C.k) : GL (Fin (n + 1)) C.k

The diagonal block embedding $\mathrm{GL}_n(k) \hookrightarrow \mathrm{GL}_{n+1}(k)$ sending $M$ to $\mathrm{diag}(a, M)$, with $a \in k^\times$ in the leading slot.

@[simp]

theorem DVRContext.diagBlockEmbedGL_val (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (a : C.kˣ) (M : GL (Fin n) C.k) : ↑(C.diagBlockEmbedGL a M) = C.diagBlockEmbedMatrix ↑a ↑M

The underlying matrix of $\mathrm{diag}(a, M)$ as a $\mathrm{GL}_{n+1}$ element coincides with the matrix-level diagonal block embedding.

theorem DVRContext.diagBlockEmbed_preserves_diag (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (a : C.kˣ) (M : GL (Fin n) C.k) (hM : M ∈ C.DiagGLn n) : C.diagBlockEmbedGL a M ∈ C.DiagGLn (n + 1)

The diagonal block embedding sends diagonal matrices to diagonal matrices.

theorem DVRContext.diagBlockEmbed_preserves_iwahori (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (a : C.kˣ) (M : GL (Fin n) C.k) (ha : C.isUnitInO ↑a) (hM : M ∈ C.IwahoriGLn n) : C.diagBlockEmbedGL a M ∈ C.IwahoriGLn (n + 1)

The diagonal block embedding sends the Iwahori subgroup $I_n$ into the Iwahori subgroup $I_{n+1}$, provided the leading scalar $a$ is a unit of $\mathcal{O}$.

theorem DVRContext.blockEmbed_diagBlockEmbed_mul (C : DVRContext) [C.DVRClosureGL2] {n : ℕ} (a : C.kˣ) (A M B : GL (Fin n) C.k) : C.blockEmbedGL A * C.diagBlockEmbedGL a M * C.blockEmbedGL B = C.diagBlockEmbedGL a (A * M * B)

Compatibility between the corner $\mathrm{GL}_n \hookrightarrow \mathrm{GL}_{n+1}$ block embedding and the diagonal block embedding: the conjugate of $\mathrm{diag}(a, M)$ by block embeddings of $A$ and $B$ equals $\mathrm{diag}(a, AMB)$.