Uniqueness of the Cartan decomposition

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₁ * diag * k₂, where kᵢ ∈ GL(n,R) and diag is a diagonal matrix with entries decreasing powers of the uniformizer.

In this file we show that the diagonal matrix diag is unique, independently of the choice of a uniformizer ϖ. More precisely, if k₁ * diag(ϖ, f) * k₂ = m₁ * diag(ϖ', f') * m₂ for two uniformizers ϖ, ϖ' and f and f' are antitone, then f = f' (see cartan_decomposition_unique_uniformizer`).

A form more commonly seen in the literature is the following: GL₂(K) admits a decomposition as a disjoint union of double cosets GL₂(R) * diag * GL₂(R) where diag is as above. For completeness, this is stated as iUnion₂_doset_cartanDiag_eq_univ and disjoint_doset_cartanDiag_of_ne below.

theorem cartanDiag_map_mul {K : Type u_1} [Field K] {R : Subring K} {k : ℕ+} {ϖ : ↥R} (hϖ : Irreducible ϖ) {u : (↥R)ˣ} (hϖ' : Irreducible (ϖ * ↑u)) (f : Fin ↑k → ℤ) : cartanDiag (ϖ * ↑u) hϖ' f = «GL».map R.subtype (Matrix.GL.diagonal fun (i : Fin ↑k) => u ^ f i) * cartanDiag ϖ hϖ f

theorem cartan_decomposition_unique'_aux {K : Type u_1} [Field K] {R : Subring K} {k : ℕ+} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {ϖ : ↥R} {hϖ : Irreducible ϖ} (x a : GL (Fin ↑k) ↥R) (f f' : Fin ↑k → ℤ) (hax : cartanDiag ϖ hϖ f * «GL».map R.subtype a * (cartanDiag ϖ hϖ f')⁻¹ = «GL».map R.subtype x) : ∃ (σ : Equiv.Perm (Fin ↑k)), f ∘ ⇑σ = f'

theorem cartan_decomposition_unique' {K : Type u_1} [Field K] {R : Subring K} {k : ℕ+} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {ϖ : ↥R} {hϖ : Irreducible ϖ} {k₁ k₂ k₁' k₂' : GL (Fin ↑k) ↥R} {f f' : Fin ↑k → ℤ} (h : «GL».map R.subtype k₁ * cartanDiag ϖ hϖ f * «GL».map R.subtype k₂ = «GL».map R.subtype k₁' * cartanDiag ϖ hϖ f' * «GL».map R.subtype k₂') : ∃ (σ : Equiv.Perm (Fin ↑k)), f ∘ ⇑σ = f'

theorem eq_of_twist_eq_of_antitone {k : ℕ+} (f g : Fin ↑k → ℤ) (σ : Equiv.Perm (Fin ↑k)) (hf : Antitone f) (hg : Antitone g) (h : f = g ∘ ⇑σ) : f = g

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

The cartan decomposition is unique.

theorem iUnion₂_doset_cartanDiag_eq_univ {K : Type u_1} [Field K] {R : Subring K} {k : ℕ+} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {ϖ : ↥R} {hϖ : Irreducible ϖ} : ⋃ (f : Fin ↑k → ℤ), ⋃ (_ : Antitone f), DoubleCoset.doubleCoset (cartanDiag ϖ hϖ f) (Set.range («GL».map R.subtype)) (Set.range («GL».map R.subtype)) = Set.univ

GL₂ is the union of the double cosets GL₂(R) * D * GL₂(R) where D runs through all diagonal matrices with entries of the form ϖ ^ n with descending n. This is a disjoint union (see disjoint_doset_cartanDiag_of_ne).

theorem disjoint_doset_cartanDiag_of_ne {K : Type u_1} [Field K] {R : Subring K} {k : ℕ+} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {ϖ : ↥R} {hϖ : Irreducible ϖ} : Pairwise (Function.onFun Disjoint fun (f : ↑{f : Fin ↑k → ℤ | Antitone f}) => DoubleCoset.doubleCoset (cartanDiag ϖ hϖ ↑f) (Set.range («GL».map R.subtype)) (Set.range («GL».map R.subtype)))

The double cosets GL₂(R) * D * GL₂(R), where D runs through all diagonal matrices with entries of the form ϖ ^ n with descending n, are pairwise disjoint.

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

The Cartan decomposition is unique, independent of the choice of a uniformizer.