ActualCharacterType61.lean

1 import PaperXI.CharacterNormalizer61
2 import PaperXI.ActualELatticeTopology60
3 
4 /-!
5 # The compact lattice part of an actual character normalizer
6 
7 This group depends on the actual subgroup-character pair. It is not the larger
8 literal lattice-product group from Block59. Its first subgroup is its actual
9 intersection with adjacent-lattice congruence, never an equality with all U1.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.ActualCharacterType61
14 open Matrix ValuativeRel Topology
15 open ActualELatticeNormalizer59 ActualELatticeResidue59 ActualELatticeTypeGroup59
16 open ActualELatticeQuotient59 ActualELatticeTopology60 LatticeMatrixTopology60
17 open LatticeCongruenceTopology60 ActualEmbeddedUniformizer58
18 
19 section Chain
20 variable {F V : Type*} [Field F] [AddCommGroup V] [Module F V]
21 
22 /-- The chain shift normalizes the full chain stabilizer, for positive and negative powers. -/
23 theorem power_normalizes_chainStabilizer (t : V ≃ₗ[F] V) (L : AddSubgroup V) (r : ℤ) :
24     t ^ r ∈ Subgroup.normalizer (chainStabilizer (K := F) (periodicChain t L) : Set (V ≃ₗ[F] V)) := by
25   have shift (r i : ℤ) (v : V) :
26       (t ^ r) v ∈ periodicChain t L i ↔ v ∈ periodicChain t L (i - r) := by
27     simpa only [sub_add_cancel] using periodicChain_shift t L r (i - r) v
28   have step (r : ℤ) (g : V ≃ₗ[F] V) (hg : g ∈ chainStabilizer (K := F) (periodicChain t L)) :
29       t ^ r * g * (t ^ r)⁻¹ ∈ chainStabilizer (K := F) (periodicChain t L) := by
30     intro i v
31     change (t ^ r) (g ((t ^ r)⁻¹ v)) ∈ periodicChain t L i ↔ _
32     rw [shift, hg (i - r)]
33     simpa [zpow_neg, sub_eq_add_neg] using shift (-r) (i - r) v
34   apply Subgroup.mem_normalizer_iff.mpr
35   intro g
36   constructor
37   · exact step r g
38   · intro hg
39     have h := step (-r) (t ^ r * g * (t ^ r)⁻¹) hg
40     simpa [zpow_neg, mul_assoc] using h
41 end Chain
42 
43 variable (K E : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
44   [IsNonarchimedeanLocalField K] [Field E] [ValuativeRel E] [TopologicalSpace E]
45   [IsNonarchimedeanLocalField E] [Algebra K E]
46 variable (n d : Type*) [Fintype n] [DecidableEq n] [Fintype d] [DecidableEq d]
47   [Nonempty d] (e : (n → E) ≃L[K] (d → K))
48 
49 local instance : T2Space K := ActualIntegralGeneralLinear.field_t2Space K
50 local instance : T2Space E := ActualIntegralGeneralLinear.field_t2Space E
51 
52 /-- The full actual lattice-chain stabilizer in matrix coordinates. -/
53 def chainGroup : Subgroup (GeneralLinearGroup d K) :=
54   (chainStabilizer (latticeChain K E n)).comap (coordinateAut e).toMonoidHom
55 
56 omit [ValuativeRel K] [IsNonarchimedeanLocalField K] [Fintype n] [DecidableEq n] [Nonempty d] in
57 /-- Full-chain congruence lies in the full-chain stabilizer. -/
58 theorem matrixCongruence_le_chainGroup : matrixCongruence K E n d e ≤ chainGroup K E n d e :=
59   fun _ h => h.1
60 
61 /-- The full chain stabilizer is open. -/
62 theorem chainGroup_open (hK : Continuous (algebraMap K E)) :
63     IsOpen (chainGroup K E n d e : Set (GeneralLinearGroup d K)) :=
64   Subgroup.isOpen_mono (matrixCongruence_le_chainGroup K E n d e)
65     (matrixCongruence_open K E n d e hK)
66 
67 /-- The full chain stabilizer is compact, inside the zero-lattice stabilizer. -/
68 theorem chainGroup_compact (hK : Continuous (algebraMap K E)) :
69     IsCompact (chainGroup K E n d e : Set (GeneralLinearGroup d K)) := by
70   let : ContinuousSMul K E := continuousSMul_of_algebraMap K E hK
71   let : Filter.NeBot (nhdsWithin (0 : K) {0}ᶜ) := field_nhdsNE_neBot K
72   apply (stabilizer_compact_of_open e (integralLattice E n)
73     (integralLattice_compact E n) (integralLattice_open E n)).of_isClosed_subset
74     ((chainGroup K E n d e).isClosed_of_isOpen (chainGroup_open K E n d e hK))
75   intro g hg
76   apply (mem_stabilizer_iff e (integralLattice E n) g).mpr
77   have h : coordinateAut e g ∈ chainStabilizer (latticeChain K E n) := hg
78   simpa only [latticeChain_zero] using h 0
79 
80 omit [ValuativeRel K] [IsNonarchimedeanLocalField K] [ValuativeRel E] [IsNonarchimedeanLocalField E]
81   [Fintype n] [DecidableEq n] [Nonempty d] in
82 /-- Every embedded extension-field unit acts by its literal scalar linear operator. -/
83 theorem coordinateAut_unitsEmbedding (a : Eˣ) :
84     coordinateAut e (unitsEmbedding K E d (scalarMatrixEmbedding K E n d e) a) =
85       ActualELatticeFreeness59.scalarAction K E n a := by
86   apply LinearEquiv.ext
87   intro v
88   change e.symm ((LinearMap.toMatrix' ((e.toLinearEquiv.conjAlgEquiv K)
89     ((Algebra.lsmul K K (n → E)) (a : E)))) *ᵥ e v) = _
90   rw [LinearMap.toMatrix'_mulVec]
91   change e.symm (e ((a : E) • e.symm (e v))) = (a : E) • v
92   simp only [ContinuousLinearEquiv.symm_apply_apply]
93 
94 omit [ValuativeRel K] [IsNonarchimedeanLocalField K] [Fintype n] [DecidableEq n] [Nonempty d] in
95 /-- The embedded extension uniformizer acts by the exact inherited scalar operator. -/
96 theorem coordinateAut_embeddedUniformizer :
97     coordinateAut e (embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e)) =
98       uniformizerAction K E n := by
99   apply LinearEquiv.ext
100   intro v
101   change e.symm ((LinearMap.toMatrix' ((e.toLinearEquiv.conjAlgEquiv K)
102     ((Algebra.lsmul K K (n → E)) (ActualLocalUnitDecomposition.uniformizer E : E)))) *ᵥ e v) = _
103   rw [LinearMap.toMatrix'_mulVec]
104   change e.symm (e ((ActualLocalUnitDecomposition.uniformizer E : E) • e.symm (e v))) =
105     (ActualLocalUnitDecomposition.uniformizer E : E) • v
106   simp only [ContinuousLinearEquiv.symm_apply_apply]
107 
108 omit [ValuativeRel K] [IsNonarchimedeanLocalField K] [Fintype n] [DecidableEq n] [Nonempty d] in
109 /-- The actual embedded uniformizer normalizes the full chain stabilizer. -/
110 theorem uniformizer_normalizes_chainGroup :
111     embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e) ∈
112       Subgroup.normalizer (chainGroup K E n d e : Set (GeneralLinearGroup d K)) := by
113   apply Subgroup.mem_normalizer_iff.mpr
114   intro g
115   change coordinateAut e g ∈ chainStabilizer (latticeChain K E n) ↔
116     coordinateAut e (_ * g * _) ∈ chainStabilizer (latticeChain K E n)
117   rw [map_mul, map_mul, map_inv, coordinateAut_embeddedUniformizer]
118   exact Subgroup.mem_normalizer_iff.mp
119     (by simpa only [zpow_one, latticeChain] using
120       power_normalizes_chainStabilizer (uniformizerAction K E n) (integralLattice E n) 1)
121     (coordinateAut e g)
122 
123 variable (H : Subgroup (GeneralLinearGroup d K)) (θ : H →* ℂˣ)
124 
125 /-- The actual theta-dependent compact group, using the graph normalizer. -/
126 def compactGroup : Subgroup (GeneralLinearGroup d K) :=
127   CharacterNormalizer61.compactPart H θ (chainGroup K E n d e)
128 
129 /-- Its first subgroup is the literal intersection, not the whole adjacent-lattice group. -/
130 def firstSubgroup : Subgroup (compactGroup K E n d e H θ) :=
131   (matrixCongruence K E n d e).subgroupOf (compactGroup K E n d e H θ)
132 
133 omit [ValuativeRel K] [IsNonarchimedeanLocalField K] [Fintype n] [DecidableEq n] [Nonempty d] in
134 /-- The actual character domain lies in its compact group when it preserves the chain. -/
135 theorem domain_le_compactGroup (hH : H ≤ chainGroup K E n d e) :
136     H ≤ compactGroup K E n d e H θ :=
137   le_inf (CharacterNormalizer61.domain_le_normalizer H θ) hH
138 
139 /-- Compactness and openness now refer to the actual character-normalizer intersection. -/
140 theorem compactGroup_compact_open (hK : Continuous (algebraMap K E))
141     (hH : IsOpen (H : Set (GeneralLinearGroup d K))) :
142     IsCompact (compactGroup K E n d e H θ : Set (GeneralLinearGroup d K)) ∧
143     IsOpen (compactGroup K E n d e H θ : Set (GeneralLinearGroup d K)) :=
144   CharacterNormalizer61.compactPart_compact_open H θ (chainGroup K E n d e) hH
145     (chainGroup_compact K E n d e hK) (chainGroup_open K E n d e hK)
146 
147 /-- The genuine intersection subgroup is open inside the compact group. -/
148 theorem firstSubgroup_open (hK : Continuous (algebraMap K E)) :
149     IsOpen (firstSubgroup K E n d e H θ : Set (compactGroup K E n d e H θ)) :=
150   (matrixCongruence_open K E n d e hK).preimage continuous_subtype_val
151 
152 omit [ValuativeRel K] [IsNonarchimedeanLocalField K] [Fintype n] [DecidableEq n] [Nonempty d] in
153 /-- Pair-normalization of theta makes the same embedded uniformizer normalize its compact part. -/
154 theorem uniformizer_normalizes_compactGroup
155     (hθ : embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e) ∈
156       CharacterNormalizer61.normalizer H θ) :
157     embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e) ∈
158       Subgroup.normalizer (compactGroup K E n d e H θ : Set (GeneralLinearGroup d K)) :=
159   Subgroup.inf_normalizer_le_normalizer_inf
160     ⟨(CharacterNormalizer61.normalizer H θ).le_normalizer hθ,
161       uniformizer_normalizes_chainGroup K E n d e⟩
162 
163 end PaperXI.ActualCharacterType61

Back to source controls