SplitRadical105.lean

1 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
2 import Mathlib.Algebra.Group.TypeTags.Basic
3 import Mathlib.Tactic.Abel
4 import Mathlib.Tactic.FieldSimp
5 
6 /-! Literal square-zero coordinate radicals, entrywise lifting, and contraction
7 by a normalized Cartan diagonal. Neither a contracting subgroup nor its lifts
8 are supplied to the matrix theorem. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.SplitRadical105
12 open Matrix
13 variable {ι R F k : Type*} [Fintype ι] [DecidableEq ι]
14   [CommRing R] [Field F] [Field k]
15 
16 /-- Matrix supported in the rectangle S times its complement. -/
17 def rect (S : Finset ι) (X : Matrix ι ι R) : Matrix ι ι R :=
18   fun i j => if i ∈ S ∧ j ∉ S then X i j else 0
19 
20 theorem rect_mul (S : Finset ι) (X Y : Matrix ι ι R) :
21     rect S X * rect S Y = 0 := by
22   ext i j
23   apply Finset.sum_eq_zero
24   intro t _
25   by_cases ht : t ∈ S <;> simp [rect, ht]
26 
27 omit [Fintype ι] in
28 theorem rect_add (S : Finset ι) (X Y : Matrix ι ι R) :
29     rect S (X + Y) = rect S X + rect S Y := by
30   ext i j
31   by_cases h : i ∈ S ∧ j ∉ S <;> simp [rect, h]
32 
33 /-- The inverse is supplied by square-zero, not by a determinant certificate. -/
34 def unip (S : Finset ι) (X : Matrix ι ι R) : GL ι R where
35   val := 1 + rect S X
36   inv := 1 - rect S X
37   val_inv := by simp [mul_sub, add_mul, rect_mul]
38   inv_val := by simp [sub_mul, mul_add, rect_mul]
39 
40 theorem unip_add (S : Finset ι) (X Y : Matrix ι ι R) :
41     unip S (X + Y) = unip S X * unip S Y := by
42   apply Units.ext
43   change 1 + rect S (X + Y) = (1 + rect S X) * (1 + rect S Y)
44   rw [rect_add]
45   simp only [add_mul, mul_add, one_mul, mul_one, rect_mul, add_zero]
46   abel
47 
48 theorem unip_zero (S : Finset ι) : unip S (0 : Matrix ι ι R) = 1 := by
49   apply Units.ext
50   ext i j
51   simp [unip, rect]
52 
53 def radicalMap (S : Finset ι) : Multiplicative (Matrix ι ι R) →* GL ι R where
54   toFun X := unip S X.toAdd
55   map_one' := unip_zero S
56   map_mul' X Y := unip_add S X.toAdd Y.toAdd
57 
58 theorem map_unip {R' : Type*} [CommRing R'] (f : R →+* R')
59     (S : Finset ι) (X : Matrix ι ι R) :
60     GeneralLinearGroup.map f (unip S X) = unip S (X.map f) := by
61   apply Units.ext
62   ext i j
63   by_cases h : i ∈ S ∧ j ∉ S <;> by_cases hij : i = j <;>
64     simp [unip, rect, h, hij]
65 
66 /-- Invertible diagonal with literal entries and reciprocal inverse. -/
67 def diagonalGL (c : ι → F) (hc : ∀ i, c i ≠ 0) : GL ι F where
68   val := diagonal c
69   inv := diagonal (fun i => (c i)⁻¹)
70   val_inv := by
71     rw [diagonal_mul_diagonal]
72     ext i j
73     by_cases h : i = j <;> simp [diagonal, Matrix.one_apply, h, hc]
74   inv_val := by
75     rw [diagonal_mul_diagonal]
76     ext i j
77     by_cases h : i = j <;> simp [diagonal, Matrix.one_apply, h, hc]
78 
79 def cartan (π : F) (hπ : π ≠ 0) (a : ι → ℕ) : GL ι F :=
80   diagonalGL (fun i => (π ^ a i)⁻¹) (fun _ => inv_ne_zero (pow_ne_zero _ hπ))
81 
82 def zeroSet (a : ι → ℕ) : Finset ι := Finset.univ.filter (fun i => a i = 0)
83 
84 omit [DecidableEq ι] in
85 @[simp] theorem mem_zeroSet (a : ι → ℕ) (i : ι) : i ∈ zeroSet a ↔ a i = 0 := by
86   simp [zeroSet]
87 
88 /-- Conjugation by diag(pi^(-a_i)) contracts the radical at the zero/positive cut. -/
89 theorem cartan_conjugation (f : R →+* F) (π : R) (hπ : f π ≠ 0)
90     (a : ι → ℕ) (X : Matrix ι ι R) :
91     cartan (f π) hπ a * GeneralLinearGroup.map f (unip (zeroSet a) X) *
92       (cartan (f π) hπ a)⁻¹ =
93     GeneralLinearGroup.map f (unip (zeroSet a) (fun i j => π ^ a j * X i j)) := by
94   have hc : cartan (f π) hπ a * GeneralLinearGroup.map f (unip (zeroSet a) X) =
95       GeneralLinearGroup.map f (unip (zeroSet a) (fun i j => π ^ a j * X i j)) *
96         cartan (f π) hπ a := by
97     apply Units.ext
98     ext i j
99     change (diagonal (fun i => ((f π) ^ a i)⁻¹) *
100       (1 + rect (zeroSet a) X).map f) i j =
101       ((1 + rect (zeroSet a) (fun i j => π ^ a j * X i j)).map f *
102         diagonal (fun i => ((f π) ^ a i)⁻¹)) i j
103     rw [diagonal_mul, mul_diagonal]
104     by_cases hij : i = j
105     · subst j
106       simp [rect]
107     · by_cases hi : a i = 0
108       · by_cases hj : a j = 0
109         · simp [rect, hij, hi, hj]
110         · simp [rect, hij, hi, hj, map_mul, map_pow]
111           field_simp
112       · simp [rect, hij, hi]
113   rw [hc, mul_assoc, mul_inv_cancel, mul_one]
114 
115 theorem contracted_reduction (red : R →+* k) (π : R) (hπ : red π = 0)
116     (a : ι → ℕ) (X : Matrix ι ι R) :
117     GeneralLinearGroup.map red
118       (unip (zeroSet a) (fun i j => π ^ a j * X i j)) = 1 := by
119   apply Units.ext
120   ext i j
121   change red ((1 + rect (zeroSet a) (fun i j => π ^ a j * X i j)) i j) = (1 : Matrix ι ι k) i j
122   by_cases hi : a i = 0
123   · by_cases hj : a j = 0
124     · simp [Matrix.one_apply, rect, hi, hj]
125     · simp [Matrix.one_apply, rect, hi, hj, map_mul, map_pow, hπ, zero_pow hj]
126   · simp [Matrix.one_apply, rect, hi]
127 
128 /-- Surjective residue reduction constructs every radical lift and a contracted partner. -/
129 theorem exists_contracted_lift (f : R →+* F) (red : R →+* k)
130     (hred : Function.Surjective red) (π : R) (hπ : f π ≠ 0) (hπred : red π = 0)
131     (a : ι → ℕ) (X : Matrix ι ι k) :
132     ∃ u v : GL ι R,
133       GeneralLinearGroup.map red u = unip (zeroSet a) X ∧
134       GeneralLinearGroup.map red v = 1 ∧
135       cartan (f π) hπ a * GeneralLinearGroup.map f u * (cartan (f π) hπ a)⁻¹ =
136         GeneralLinearGroup.map f v := by
137   let Y : Matrix ι ι R := fun i j => Classical.choose (hred (X i j))
138   have hY : Y.map red = X := by
139     ext i j
140     exact Classical.choose_spec (hred (X i j))
141   refine ⟨unip (zeroSet a) Y,
142     unip (zeroSet a) (fun i j => π ^ a j * Y i j), ?_,
143     contracted_reduction red π hπred a Y, cartan_conjugation f π hπ a Y⟩
144   rw [map_unip, hY]
145 
146 theorem cartan_zero (π : F) (hπ : π ≠ 0) (a : ι → ℕ) (ha : ∀ i, a i = 0) :
147     cartan π hπ a = 1 := by
148   apply Units.ext
149   ext i j
150   simp [cartan, diagonalGL, ha]
151 
152 end PaperXI.SplitRadical105

Back to source controls