The Cartan Decomposition of GL(n,K) for K a discretely valued field

We establish the Cartan decomposition of GL(n,K) for K a discretely valued field.

Given K as the fraction field of a DVR R with uniformizer ϖ, the Cartan decomposition says that any matrix g ∈ GL(n,K) can be written as a product k_1 * diag * k_2, where k_i ∈ GL(n,R) and diag is a diagonal matrix with entries increasing powers of the uniformizer.

There is an analogue where one uses decreasing powers instead, both versions are used in mathematics. We only show the "increasing" version.

Most of the linear algebra preparations below are for arbitrary valuation rings. Only from line 628 onwards we specialize to DVRs.

Implementation details

This is inspired by the file https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/Transvection.html.

theorem exists_normalization0 {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) : ∃ (k₁ : GL (Fin ↑k ⊕ Unit) ↥R) (k₂ : GL (Fin ↑k ⊕ Unit) ↥R), (ValuationRing.valuation (↥R) K) (((↑k₁).map ⇑R.subtype * g * (↑k₂).map ⇑R.subtype) (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g

We can normalize any g : Matrix (Fin k) (Fin k) K such that the coefficient on the bottom right has maximal valuation.

theorem exists_normalization0' {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) : ∃ (k₁ : GL (Fin ↑k ⊕ Unit) ↥R) (k₂ : GL (Fin ↑k ⊕ Unit) ↥R), (ValuationRing.valuation (↥R) K) (((↑k₁).map ⇑R.subtype * g * (↑k₂).map ⇑R.subtype) (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) ((↑k₁).map ⇑R.subtype * g * (↑k₂).map ⇑R.subtype) ∧ Matrix.coeffsSup (ValuationRing.valuation (↥R) K) ((↑k₁).map ⇑R.subtype * g * (↑k₂).map ⇑R.subtype) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g

We can normalize any g : Matrix (Fin k) (Fin k) K such that the coefficient on the bottom right has maximal valuation and the maximal valuation is unchanged.

theorem sup_val_non_zero {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : GL (Fin ↑k) K) : Matrix.coeffsSup (ValuationRing.valuation (↥R) K) ↑g ≠ 0

The maximal valuation of the coefficients of any element of GL (Fin k) K is non-zero.

noncomputable def multFactor {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k l : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑l ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑l) : ↥R

The element of R used to eliminate the last row and column of g if the coefficient in the bottom-right has maximal valuation.

Equations

• multFactor g h j = if hn : g (Sum.inr ()) (Sum.inr ()) = 0 then 0 else ⟨-g (Sum.inr ()) (Sum.inl j) * (g (Sum.inr ()) (Sum.inr ()))⁻¹, ⋯⟩

theorem multFactor_mul {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k l : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑l ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑l) : g (Sum.inr ()) (Sum.inl j) + ↑(multFactor g h j) * g (Sum.inr ()) (Sum.inr ()) = 0

noncomputable def rowEliminationTransvection {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k l : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑l ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑l) : Matrix.TransvectionStruct (Fin ↑l ⊕ Unit) ↥R

The transvection struct in R for the transvection eliminating the j-th entry in the last row of g, where the bottom-right element of g has maximal valuation.

Equations

• rowEliminationTransvection g h j = { i := Sum.inr (), j := Sum.inl j, hij := ⋯, c := multFactor g h j }

theorem rowEliminationTransvection_mul_same {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {l : ℕ+} (g : Matrix (Fin ↑l ⊕ Unit) (Fin ↑l ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑l) (a : Fin ↑l ⊕ Unit) : (g * (rowEliminationTransvection g h j).toMatrix.map ⇑R.subtype) a (Sum.inl j) = g a (Sum.inl j) + ↑(multFactor g h j) * g a (Sum.inr ())

theorem rowEliminationTransvection_mul_neq {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {l : ℕ+} {g : Matrix (Fin ↑l ⊕ Unit) (Fin ↑l ⊕ Unit) K} (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑l) (a b : Fin ↑l ⊕ Unit) (hb : b ≠ Sum.inl j) : (g * (rowEliminationTransvection g h j).toMatrix.map ⇑R.subtype) a b = g a b

theorem rowEliminationTransvection_mul {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {l : ℕ+} (g : Matrix (Fin ↑l ⊕ Unit) (Fin ↑l ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑l) : (g * (rowEliminationTransvection g h j).toMatrix.map ⇑R.subtype) (Sum.inr ()) (Sum.inl j) = 0

Multiplying on the right with rowEliminationTransvection kills all elements in the first row but the first.

theorem rowEliminationTransvection_mul_coeffs_sup' {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑k) (c : ↥R) : (ValuationRing.valuation (↥R) K) ((g * Matrix.transvection (Sum.inr ()) (Sum.inl j) ↑c) (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) (g * Matrix.transvection (Sum.inr ()) (Sum.inl j) ↑c)

theorem rowEliminationTransvection_mul_coeffs_sup {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑k) : Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) (g * (rowEliminationTransvection g h j).toMatrix.map ⇑R.subtype)

After multiplying on the right with rowEliminationTransvection, the maximal valuation of the coefficients does not change.

noncomputable def rowEliminationList {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) : List (Matrix.TransvectionStruct (Fin ↑k ⊕ Unit) ↥R)

The row transvections used to eliminate the last row away from the diagonal.

Equations

• rowEliminationList g h = List.ofFn fun (j : Fin ↑k) => rowEliminationTransvection g h j

noncomputable def rowEliminationListMatrix {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) : List (Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K)

The matrix form of rowEliminationList.

Equations

• rowEliminationListMatrix g h = List.ofFn fun (j : Fin ↑k) => (rowEliminationTransvection g h j).toMatrix.map ⇑R.subtype

theorem rowEliminationList_get {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (n : Fin ↑k) : (rowEliminationListMatrix g h)[n]? = do let a ← some (Matrix.transvection (Sum.inr ()) (Sum.inl n) (multFactor g h n)) pure (a.map ⇑R.subtype)

theorem mul_rowEliminationListMatrix_prod_apply_lastCol_aux {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑k ⊕ Unit) {r : ℕ} (hr : r ≤ ↑k) : (g * (List.take r (rowEliminationListMatrix g h)).prod) j (Sum.inr ()) = g j (Sum.inr ())

theorem mul_rowEliminationListMatrix_prod_apply_lastCol {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑k ⊕ Unit) : (g * (rowEliminationListMatrix g h).prod) j (Sum.inr ()) = g j (Sum.inr ())

theorem mul_rowEliminationListMatrix_prod_apply_aux {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑k) (r : ℕ) (hrk : r ≤ ↑k) : (g * (List.take r (rowEliminationListMatrix g h)).prod) (Sum.inr ()) (Sum.inl j) = if r ≤ ↑j then g (Sum.inr ()) (Sum.inl j) else 0

theorem mul_rowEliminationListMatrix_prod_apply {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑k) : (g * (rowEliminationListMatrix g h).prod) (Sum.inr ()) (Sum.inl j) = 0

noncomputable def rowEliminator {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) : GL (Fin ↑k ⊕ Unit) ↥R

The product of row transvections eliminating the last row away from the diagonal.

Equations

• rowEliminator g h = (List.map (fun (t : Matrix.TransvectionStruct (Fin ↑k ⊕ Unit) ↥R) => t.toGL) (rowEliminationList g h)).prod

theorem mul_rowEliminator_lastRow {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑k) : (g * (↑(rowEliminator g h)).map ⇑R.subtype) (Sum.inr ()) (Sum.inl j) = 0

theorem mul_rowEliminator_lastCol {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑k ⊕ Unit) : (g * (↑(rowEliminator g h)).map ⇑R.subtype) j (Sum.inr ()) = g j (Sum.inr ())

noncomputable def colEliminator {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) : GL (Fin ↑k ⊕ Unit) ↥R

The column eliminator, defined by transposing and applying the row eliminator.

Equations

• colEliminator g h = Matrix.GL.transpose (rowEliminator g.transpose ⋯)

theorem colEliminator_mul_lastCol {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ↑↑k) (Sum.inr ↑↑k)) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑k) : ((↑(colEliminator g h)).map ⇑R.subtype * g) (Sum.inl j) (Sum.inr ()) = 0

theorem colEliminator_mul_lastRow {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑k ⊕ Unit) : ((↑(colEliminator g h)).map ⇑R.subtype * g) (Sum.inr ()) j = g (Sum.inr ()) j

theorem mul_rowEliminationListMatrix_coeffs_sup_aux {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (r : ℕ) (hrk : r ≤ ↑k) : (ValuationRing.valuation (↥R) K) ((g * (List.take r (rowEliminationListMatrix g h)).prod) (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) (g * (List.take r (rowEliminationListMatrix g h)).prod)

theorem mul_rowEliminationListMatrix_coeffs_sup {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) : (ValuationRing.valuation (↥R) K) ((g * (rowEliminationListMatrix g h).prod) (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) (g * (rowEliminationListMatrix g h).prod)

theorem mul_rowEliminator_coeffs_sup {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) : (ValuationRing.valuation (↥R) K) ((g * (↑(rowEliminator g h)).map ⇑R.subtype) (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) (g * (↑(rowEliminator g h)).map ⇑R.subtype)

theorem colEliminator_mul_coeffs_sup {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) : (ValuationRing.valuation (↥R) K) (((↑(colEliminator g h)).map ⇑R.subtype * g) (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) ((↑(colEliminator g h)).map ⇑R.subtype * g)

theorem rowEliminator_colEliminator {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) : rowEliminator ((↑(colEliminator g h)).map ⇑R.subtype * g) ⋯ = rowEliminator g h

theorem colEliminator_rowEliminator {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) : colEliminator (g * (↑(rowEliminator g h)).map ⇑R.subtype) ⋯ = colEliminator g h

theorem colEliminator_mul_rowEliminator_lastRow {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑k) : ((↑(colEliminator g h)).map ⇑R.subtype * g * (↑(rowEliminator g h)).map ⇑R.subtype) (Sum.inr ()) (Sum.inl j) = 0

theorem colEliminator_mul_rowEliminator_lastCol {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) (j : Fin ↑k) : ((↑(colEliminator g h)).map ⇑R.subtype * g * (↑(rowEliminator g h)).map ⇑R.subtype) (Sum.inl j) (Sum.inr ()) = 0

theorem colEliminator_mul_rowEliminator_last_last {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) : ((↑(colEliminator g h)).map ⇑R.subtype * g * (↑(rowEliminator g h)).map ⇑R.subtype) (Sum.inr ()) (Sum.inr ()) = g (Sum.inr ()) (Sum.inr ())

theorem colEliminator_mul_rowEliminator_coeffs_sup {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (h : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g) : Matrix.coeffsSup (ValuationRing.valuation (↥R) K) ((↑(colEliminator g h)).map ⇑R.subtype * g * (↑(rowEliminator g h)).map ⇑R.subtype) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g

structure IsNormalBlock {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) : Prop

A (k + 1) × (k + 1) matrix is of normal block form, if it is block diagonal and the bottom-right coefficient has maximal valuation.

• isTwoBlockDiagonal : g.IsTwoBlockDiagonal
• monotone : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g

theorem exists_trafo_isNormalBlock {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) : ∃ (k₁ : GL (Fin ↑k ⊕ Unit) ↥R) (k₂ : GL (Fin ↑k ⊕ Unit) ↥R), IsNormalBlock ((↑k₁).map ⇑R.subtype * g * (↑k₂).map ⇑R.subtype) ∧ Matrix.coeffsSup (ValuationRing.valuation (↥R) K) ((↑k₁).map ⇑R.subtype * g * (↑k₂).map ⇑R.subtype) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g

structure IsMonotoneDiag {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {n : Type u_2} [Fintype n] [Preorder n] (g : Matrix n n K) : Prop

A matrix is monotone diagonal if it is diagonal and the coefficients on the diagonal have monotonically increasing valuations.

• isDiag : g.IsDiag
• monotone : Monotone fun (j : n) => (ValuationRing.valuation (↥R) K) (g j j)

structure IsBlockMonotoneDiag {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) : Prop

An equivalent spelling of IsMonotoneDiag for (k + 1) × (k + 1)-matrices.

• isDiag : g.IsDiag
• monotone : Monotone fun (j : Fin ↑k) => (ValuationRing.valuation (↥R) K) (g (Sum.inl j) (Sum.inl j))
• max_bot_right : (ValuationRing.valuation (↥R) K) (g (Sum.inr ()) (Sum.inr ())) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g

theorem monotone_of_isBlockMonotoneDiag {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (hb : IsBlockMonotoneDiag g) : Monotone fun (j : Fin (↑k + 1)) => (ValuationRing.valuation (↥R) K) (g ((Fin.succEquivUnit ↑k) j) ((Fin.succEquivUnit ↑k) j))

theorem exists_trafo_isDiag_induction_step {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k ⊕ Unit) (Fin ↑k ⊕ Unit) K) (ih : ∀ (h : Matrix (Fin ↑k) (Fin ↑k) K), ∃ (k₁ : GL (Fin ↑k) ↥R) (k₂ : GL (Fin ↑k) ↥R), IsMonotoneDiag ((↑k₁).map ⇑R.subtype * h * (↑k₂).map ⇑R.subtype) ∧ Matrix.coeffsSup (ValuationRing.valuation (↥R) K) ((↑k₁).map ⇑R.subtype * h * (↑k₂).map ⇑R.subtype) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) h) : ∃ (k₁ : GL (Fin ↑k ⊕ Unit) ↥R) (k₂ : GL (Fin ↑k ⊕ Unit) ↥R), IsBlockMonotoneDiag ((↑k₁).map ⇑R.subtype * g * (↑k₂).map ⇑R.subtype) ∧ Matrix.coeffsSup (ValuationRing.valuation (↥R) K) ((↑k₁).map ⇑R.subtype * g * (↑k₂).map ⇑R.subtype) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g

theorem exists_trafo_isDiag {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (g : Matrix (Fin ↑k) (Fin ↑k) K) : ∃ (k₁ : GL (Fin ↑k) ↥R) (k₂ : GL (Fin ↑k) ↥R), IsMonotoneDiag ((↑k₁).map ⇑R.subtype * g * (↑k₂).map ⇑R.subtype) ∧ Matrix.coeffsSup (ValuationRing.valuation (↥R) K) ((↑k₁).map ⇑R.subtype * g * (↑k₂).map ⇑R.subtype) = Matrix.coeffsSup (ValuationRing.valuation (↥R) K) g

def IsNormalDiag {K : Type u_1} [Field K] {R : Subring K} {k : ℕ+} (ϖ : ↥R) (g : Matrix (Fin ↑k) (Fin ↑k) K) : Prop

A matrix is normal diagonal if it is diagonal, the first entries on the diagonal are given by powers of the uniformiser ϖ and the last entries by 0.

Equations

• IsNormalDiag ϖ g = ∃ (r : ℕ) (hr : r ≤ ↑k) (f : Fin r → ℤ), Monotone f ∧ (∀ (j : Fin r), g (Fin.castLE hr j) (Fin.castLE hr j) = ↑ϖ ^ f j) ∧ ∀ (j : Fin ↑k), r ≤ ↑j → g j j = 0

theorem exists_normalization_of_isMonotoneDiag {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (ϖ : ↥R) (hϖ : Irreducible ϖ) [IsDiscreteValuationRing ↥R] (g : GL (Fin ↑k) K) (h : IsMonotoneDiag ↑g) : ∃ (d : Fin ↑k → (↥R)ˣ) (f : Fin ↑k → ℤ), Antitone f ∧ ∀ (j : Fin ↑k), ↑(«GL».map R.subtype (Matrix.GL.diagonal d) * g) j j = ↑ϖ ^ f j

def cartanDiag {K : Type u_1} [Field K] {R : Subring K} (ϖ : ↥R) (hϖ : Irreducible ϖ) {k : ℕ} (f : Fin k → ℤ) : GL (Fin k) K

The cartan diagonal for a tuple of integers f is the diagonal matrix where the diagonal entries are given by ϖ ^ f i.

Equations

• cartanDiag ϖ hϖ f = Matrix.GL.diagonal fun (j : Fin k) => { val := ↑ϖ ^ f j, inv := ↑ϖ ^ (-f j), val_inv := ⋯, inv_val := ⋯ }

theorem val_cartanDiag {K : Type u_1} [Field K] {R : Subring K} (ϖ : ↥R) (hϖ : Irreducible ϖ) {k : ℕ} (f : Fin k → ℤ) : ↑(cartanDiag ϖ hϖ f) = Matrix.diagonal fun (j : Fin k) => ↑ϖ ^ f j

theorem val_inv_cartanDiag {K : Type u_1} [Field K] {R : Subring K} (ϖ : ↥R) (hϖ : Irreducible ϖ) {k : ℕ} (f : Fin k → ℤ) : ↑(cartanDiag ϖ hϖ f)⁻¹ = Matrix.diagonal fun (j : Fin k) => (↑ϖ ^ f j)⁻¹

theorem cartanDiag_inv {K : Type u_1} [Field K] {R : Subring K} (ϖ : ↥R) (hϖ : Irreducible ϖ) {k : ℕ} (f : Fin k → ℤ) : (cartanDiag ϖ hϖ f)⁻¹ = cartanDiag ϖ hϖ fun (i : Fin k) => -f i

@[simp]

theorem cartanDiag_zero {K : Type u_1} [Field K] {R : Subring K} {k : ℕ} {ϖ : ↥R} (hϖ : Irreducible ϖ) : cartanDiag ϖ hϖ 0 = 1

theorem conj_cartanDiag_zero_zero {K : Type u_1} [Field K] {R : Subring K} {ϖ : ↥R} (hϖ : Irreducible ϖ) (g : GL (Fin 2) K) (f : Fin 2 → ℤ) : ↑((MulAut.conj (cartanDiag ϖ hϖ f)) g) 0 0 = ↑g 0 0

theorem conj_cartanDiag_one_one {K : Type u_1} [Field K] {R : Subring K} {ϖ : ↥R} (hϖ : Irreducible ϖ) (g : GL (Fin 2) K) (f : Fin 2 → ℤ) : ↑((MulAut.conj (cartanDiag ϖ hϖ f)) g) 1 1 = ↑g 1 1

theorem conj_cartanDiag_one_zero {K : Type u_1} [Field K] {R : Subring K} {ϖ : ↥R} (hϖ : Irreducible ϖ) (g : GL (Fin 2) K) (f : Fin 2 → ℤ) : ↑((MulAut.conj (cartanDiag ϖ hϖ f)) g) 1 0 = ↑ϖ ^ (f 1 - f 0) * ↑g 1 0

theorem conj_cartanDiag_zero_one {K : Type u_1} [Field K] {R : Subring K} {ϖ : ↥R} (hϖ : Irreducible ϖ) (g : GL (Fin 2) K) (f : Fin 2 → ℤ) : ↑((MulAut.conj (cartanDiag ϖ hϖ f)) g) 0 1 = ↑ϖ ^ (f 0 - f 1) * ↑g 0 1

theorem cartan_decomposition {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (ϖ : ↥R) (hϖ : Irreducible ϖ) [IsDiscreteValuationRing ↥R] (g : GL (Fin ↑k) K) : ∃ (k₁ : GL (Fin ↑k) ↥R) (k₂ : GL (Fin ↑k) ↥R) (f : Fin ↑k → ℤ), Antitone f ∧ «GL».map R.subtype k₁ * g * «GL».map R.subtype k₂ = cartanDiag ϖ hϖ f

Existence part of cartan decomposition: If R is a discrete valuation ring with uniformizer ϖ and g an invertible matrix over K, then there exist invertible matrices k₁ and k₂ over R such that k₁ * g * k₂ is a diagonal matrix with decreasing powers of ϖ on the diagonal. See cartan_decomposition' for a version where instead g is written as a product.

theorem cartan_decomposition' {K : Type u_1} [Field K] {R : Subring K} [ValuationRing ↥R] [IsFractionRing (↥R) K] {k : ℕ+} (ϖ : ↥R) (hϖ : Irreducible ϖ) [IsDiscreteValuationRing ↥R] (g : GL (Fin ↑k) K) : ∃ (k₁ : GL (Fin ↑k) ↥R) (k₂ : GL (Fin ↑k) ↥R) (f : Fin ↑k → ℤ), Antitone f ∧ «GL».map R.subtype k₁ * cartanDiag ϖ hϖ f * «GL».map R.subtype k₂ = g

Variant of cartan_decomposition where g is written as a product.