DVRCartan106.lean

1 import PaperXI.FractionMatrix106
2 import PaperXI.CuspidalCartan105
3 import Mathlib.RingTheory.DiscreteValuationRing.Basic
4 import Mathlib.Data.Finset.Max
5 
6 /-! Normalized Cartan decomposition over the fraction field of a DVR. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.DVRCartan106
10 open Matrix
11 variable {ι R F : Type*} [Fintype ι] [DecidableEq ι]
12   [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
13   [Field F] [Algebra R F] [IsFractionRing R F]
14 
15 def unitsDiagonal (u : ι → Rˣ) : GL ι R where
16   val := diagonal (fun i => (u i : R))
17   inv := diagonal (fun i => ((u i)⁻¹ : Rˣ))
18   val_inv := by simp [diagonal_mul_diagonal]
19   inv_val := by simp [diagonal_mul_diagonal]
20 
21 theorem normalize_diagonal [Nonempty ι] (π : R) (hπ : Irreducible π)
22     (d : ι → R) (hd : ∀ i, algebraMap R F (d i) ≠ 0) :
23     ∃ c : Fˣ, ∃ U : GL ι R, ∃ a : ι → ℕ,
24       (∃ i, a i = 0) ∧
25       SplitRadical105.diagonalGL (fun i => algebraMap R F (d i)) hd =
26         GeneralLinearGroup.scalar ι c * (GeneralLinearGroup.map (algebraMap R F) U *
27           SplitRadical105.cartan (algebraMap R F π)
28             (fun h => hπ.ne_zero ((IsFractionRing.injective R F) (h.trans (map_zero _).symm))) a) := by
29   have hdR : ∀ i, d i ≠ 0 := fun i h => hd i (by rw [h, map_zero])
30   choose n u hu using fun i => IsDiscreteValuationRing.eq_unit_mul_pow_irreducible (hdR i) hπ
31   obtain ⟨j, _, hj⟩ := Finset.exists_max_image Finset.univ n Finset.univ_nonempty
32   have hn : ∀ i, n i ≤ n j := fun i => hj i (Finset.mem_univ i)
33   have hpF : algebraMap R F π ≠ 0 :=
34     fun h => hπ.ne_zero ((IsFractionRing.injective R F) (h.trans (map_zero _).symm))
35   refine ⟨Units.mk0 ((algebraMap R F π) ^ n j) (pow_ne_zero _ hpF),
36     unitsDiagonal u, fun i => n j - n i, ⟨j, Nat.sub_self _⟩, ?_⟩
37   apply Units.ext
38   ext i k
39   change diagonal (fun i => algebraMap R F (d i)) i k =
40     (Matrix.scalar ι ((algebraMap R F π) ^ n j) *
41       ((diagonal (fun i => (u i : R))).map (algebraMap R F) *
42         diagonal (fun i => ((algebraMap R F π) ^ (n j - n i))⁻¹))) i k
43   rw [Matrix.diagonal_map (map_zero _), Matrix.diagonal_mul_diagonal, Matrix.scalar_apply, ← Matrix.smul_eq_diagonal_mul]
44   by_cases hik : i = k
45   · subst k
46     simp only [Matrix.diagonal_apply_eq, Matrix.smul_apply, smul_eq_mul]
47     rw [hu i, map_mul, map_pow]
48     have hpow : (algebraMap R F π) ^ n j =
49         (algebraMap R F π) ^ n i * (algebraMap R F π) ^ (n j - n i) := by
50       rw [← pow_add, Nat.add_sub_of_le (hn i)]
51     rw [hpow]
52     field_simp
53   · simp [Matrix.smul_apply, hik]
54 
55 theorem hasCartan [Nonempty ι] (π : R) (hπ : Irreducible π) :
56     CuspidalCartan105.HasCartan (ι := ι) (algebraMap R F) π
57       (fun h => hπ.ne_zero ((IsFractionRing.injective R F) (h.trans (map_zero _).symm))) := by
58   intro g
59   obtain ⟨c, P, Q, d, hd, he⟩ := FractionMatrix106.exists_integral_diagonal (R := R) g
60   obtain ⟨z, U, a, ha, hdiag⟩ := normalize_diagonal π hπ d hd
61   refine ⟨c * z, P * U, Q, a, ha, ?_⟩
62   rw [he, hdiag, map_mul, map_mul]
63   have hc := GeneralLinearGroup.scalar_commute z (GeneralLinearGroup.map (algebraMap R F) P)
64   simp only [mul_assoc]
65   rw [← mul_assoc (GeneralLinearGroup.map (algebraMap R F) P)
66     (GeneralLinearGroup.scalar ι z), ← hc, mul_assoc]
67 
68 end PaperXI.DVRCartan106

Back to source controls