ActualELatticeNormalizer59.lean

1 import PaperXI.ActualIntegralGeneralLinear
2 import PaperXI.ActualLocalUnitDecomposition
3 import PaperXI.NormalizerExtensionInducing58
4 import Mathlib.Algebra.Group.Subgroup.Pointwise
5 
6 /-!
7 # Periodic lattices and their literal first congruence group
8 
9 The chain used below is the actual sequence of scalar-uniformizer translates
10 of the integral lattice in `E^m`, viewed as a vector space over `K`. Its first
11 congruence group consists of automorphisms preserving every lattice and acting
12 as the identity modulo the next lattice. Uniformizer normalization is proved
13 from the coordinate definitions. This is not an identification with the
14 simple-character group of an arbitrary stratum.
15 -/
16 set_option autoImplicit false
17 noncomputable section
18 namespace PaperXI.ActualELatticeNormalizer59
19 
20 section Chain
21 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
22 
23 /-- All automorphisms preserving every additive lattice in a chain. -/
24 def chainStabilizer (L : ℤ → AddSubgroup V) : Subgroup (V ≃ₗ[K] V) where
25   carrier := {g | ∀ i v, g v ∈ L i ↔ v ∈ L i}
26   one_mem' := by intro i v; rfl
27   mul_mem' := by
28     intro g h hg hh i v
29     exact (hg i (h v)).trans (hh i v)
30   inv_mem' := by
31     intro g hg i v
32     exact (hg i (g⁻¹ v)).symm.trans (by simp)
33 
34 /-- The literal first congruence condition on every adjacent lattice pair. -/
35 def firstCongruence (L : ℤ → AddSubgroup V) : Subgroup (V ≃ₗ[K] V) where
36   carrier := {g | g ∈ chainStabilizer L ∧ ∀ i v, v ∈ L i → g v - v ∈ L (i + 1)}
37   one_mem' := by
38     refine ⟨(chainStabilizer L).one_mem, ?_⟩
39     intro i v hv
40     simp
41   mul_mem' := by
42     intro g h hg hh
43     refine ⟨(chainStabilizer L).mul_mem hg.1 hh.1, ?_⟩
44     intro i v hv
45     have ha := (hg.1 (i + 1) (h v - v)).mpr (hh.2 i v hv)
46     have hb := hg.2 i v hv
47     convert (L (i + 1)).add_mem ha hb using 1
48     simp only [LinearEquiv.mul_apply, map_sub]
49     abel
50   inv_mem' := by
51     intro g hg
52     refine ⟨(chainStabilizer L).inv_mem hg.1, ?_⟩
53     intro i v hv
54     have h := hg.2 i (g⁻¹ v) ((hg.1 i (g⁻¹ v)).mp (by simpa using hv))
55     have hn := (L (i + 1)).neg_mem h
56     simpa using hn
57 
58 /-- Congruence automorphisms preserve the chain by definition. -/
59 theorem firstCongruence_le (L : ℤ → AddSubgroup V) :
60     firstCongruence (K := K) L ≤ chainStabilizer L := fun _ h => h.1
61 
62 /-- Every chain stabilizer normalizes the actual first congruence group. -/
63 theorem stabilizer_normalizes_firstCongruence (L : ℤ → AddSubgroup V) :
64     chainStabilizer L ≤ Subgroup.normalizer (firstCongruence (K := K) L : Set (V ≃ₗ[K] V)) := by
65   intro h hh
66   apply Subgroup.mem_normalizer_iff.mpr
67   intro g
68   have step (h : V ≃ₗ[K] V) (hh : h ∈ chainStabilizer L)
69       (g : V ≃ₗ[K] V) (hg : g ∈ firstCongruence L) :
70       h * g * h⁻¹ ∈ firstCongruence L := by
71     refine ⟨(chainStabilizer L).mul_mem
72       ((chainStabilizer L).mul_mem hh hg.1) ((chainStabilizer L).inv_mem hh), ?_⟩
73     intro i v hv
74     have hi : h⁻¹ v ∈ L i := (hh i (h⁻¹ v)).mp (by simpa using hv)
75     have hx := (hh (i + 1) (g (h⁻¹ v) - h⁻¹ v)).mpr (hg.2 i _ hi)
76     simpa using hx
77   constructor
78   · exact step h hh g
79   · intro hg
80     have hi := step h⁻¹ ((chainStabilizer L).inv_mem hh) (h * g * h⁻¹) hg
81     simpa [mul_assoc] using hi
82 
83 /-- Integer translates of one lattice by an actual linear automorphism. -/
84 def periodicChain (t : V ≃ₗ[K] V) (L : AddSubgroup V) (i : ℤ) : AddSubgroup V :=
85   L.comap (t ^ (-i)).toAddMonoidHom
86 
87 /-- Translation of the chain is proved for every positive and negative power. -/
88 theorem periodicChain_shift (t : V ≃ₗ[K] V) (L : AddSubgroup V)
89     (r i : ℤ) (v : V) :
90     (t ^ r) v ∈ periodicChain t L (i + r) ↔ v ∈ periodicChain t L i := by
91   change (t ^ (-(i + r))) ((t ^ r) v) ∈ L ↔ (t ^ (-i)) v ∈ L
92   rw [← LinearEquiv.mul_apply, ← zpow_add]
93   rw [show -(i + r) + r = -i by omega]
94 
95 /-- All translates of the chosen generator normalize first congruence. -/
96 theorem power_normalizes_firstCongruence (t : V ≃ₗ[K] V) (L : AddSubgroup V)
97     (r : ℤ) : t ^ r ∈ Subgroup.normalizer
98       (firstCongruence (K := K) (periodicChain t L) : Set (V ≃ₗ[K] V)) := by
99   have shift (r i : ℤ) (v : V) :
100       (t ^ r) v ∈ periodicChain t L i ↔ v ∈ periodicChain t L (i - r) := by
101     have h := periodicChain_shift t L r (i - r) v
102     rwa [show i - r + r = i by omega] at h
103   have step (r : ℤ) (g : V ≃ₗ[K] V)
104       (hg : g ∈ firstCongruence (periodicChain t L)) :
105       t ^ r * g * (t ^ r)⁻¹ ∈ firstCongruence (periodicChain t L) := by
106     refine ⟨?_, ?_⟩
107     · intro i v
108       change (t ^ r) (g ((t ^ r)⁻¹ v)) ∈ periodicChain t L i ↔ _
109       rw [shift, hg.1 (i - r)]
110       simpa [zpow_neg, sub_eq_add_neg] using shift (-r) (i - r) v
111     · intro i v hv
112       have hi : (t ^ r)⁻¹ v ∈ periodicChain t L (i - r) := by
113         rw [← zpow_neg]
114         apply (shift (-r) (i - r) v).mpr
115         simpa [sub_eq_add_neg] using hv
116       have hx := hg.2 (i - r) _ hi
117       have hy := (shift r (i + 1) (g ((t ^ r)⁻¹ v) - (t ^ r)⁻¹ v)).mpr
118         (by rwa [show i + 1 - r = i - r + 1 by omega])
119       simpa using hy
120   apply Subgroup.mem_normalizer_iff.mpr
121   intro g
122   constructor
123   · exact step r g
124   · intro hg
125     have hi := step (-r) (t ^ r * g * (t ^ r)⁻¹) hg
126     simpa [zpow_neg, mul_assoc] using hi
127 end Chain
128 
129 end PaperXI.ActualELatticeNormalizer59

Back to source controls