ActualCharacterIdentification61.lean

1 import PaperXI.ActualCharacterType61
2 
3 /-!
4 # Identification with the supplied genuine compact type group
5 
6 The exact standard-theory input is the actual full character-normalizer
7 formula N(theta)=E^× J0, together with integral E-units in J0 and preservation
8 of the lattice chain. These imply that the constructed compact intersection
9 is literally J0. No equality J1=U_a1 is used or concluded.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.ActualCharacterIdentification61
14 open Matrix ValuativeRel
15 open ActualCharacterType61 ActualELatticeTopology60 ActualEmbeddedUniformizer58
16 open NormalizerExtensionInducing58 ActualLocalUnitTopology
17 
18 variable (K E : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
19   [IsNonarchimedeanLocalField K] [Field E] [ValuativeRel E] [TopologicalSpace E]
20   [IsNonarchimedeanLocalField E] [Algebra K E]
21 variable (n d : Type*) [Fintype n] [DecidableEq n] [Fintype d] [DecidableEq d]
22   [Nonempty d] (e : (n → E) ≃L[K] (d → K))
23 variable (H : Subgroup (GeneralLinearGroup d K)) (θ : H →* ℂˣ)
24 variable (J0 : Subgroup (GeneralLinearGroup d K))
25 
26 /-- The exact full-normalizer formula identifies the actual compact intersection with genuine J0. -/
27 theorem compactGroup_eq_of_full_normalizer (hK : Continuous (algebraMap K E))
28     (hJ : J0 ≤ chainGroup K E n d e)
29     (hu : ∀ u : 𝒪[E]ˣ,
30       unitsEmbedding K E d (scalarMatrixEmbedding K E n d e) (unitEmbedding E u) ∈ J0)
31     (hfull : ∀ g : GeneralLinearGroup d K,
32       g ∈ CharacterNormalizer61.normalizer H θ ↔
33         ∃ a : Eˣ, ∃ j : J0,
34           unitsEmbedding K E d (scalarMatrixEmbedding K E n d e) a * (j : GeneralLinearGroup d K) = g) :
35     compactGroup K E n d e H θ = J0 := by
36   apply le_antisymm
37   · intro g hg
38     obtain ⟨a, j, he⟩ := (hfull g).mp hg.1
39     obtain ⟨r, k, hr⟩ := field_product_normalForm K E d
40       (scalarMatrixEmbedding K E n d e) J0 hu a j
41     have hgk : embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e) ^ r =
42         g * (k : GeneralLinearGroup d K)⁻¹ := by
43       rw [← he, hr]
44       group
45     have hm : embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e) ^ r ∈
46         chainGroup K E n d e := by
47       rw [hgk]
48       exact (chainGroup K E n d e).mul_mem hg.2 ((chainGroup K E n d e).inv_mem (hJ k.property))
49     have hz := embeddedUniformizer_free_of_algebraMap K E d
50       (scalarMatrixEmbedding K E n d e) hK (chainGroup K E n d e)
51       (chainGroup_compact K E n d e hK) r hm
52     have hg' : g = k := by rw [← he, hr, hz, zpow_zero, one_mul]
53     exact hg' ▸ k.property
54   · intro j hj
55     exact ⟨(hfull j).mpr ⟨1, ⟨j, hj⟩, by simp⟩, hJ hj⟩
56 
57 omit [ValuativeRel K] [IsNonarchimedeanLocalField K] [Fintype n] [DecidableEq n] [Nonempty d] in
58 /-- The same exact formula supplies actual uniformizer covariance of theta. -/
59 theorem uniformizer_mem_full_normalizer
60     (hfull : ∀ g : GeneralLinearGroup d K,
61       g ∈ CharacterNormalizer61.normalizer H θ ↔
62         ∃ a : Eˣ, ∃ j : J0,
63           unitsEmbedding K E d (scalarMatrixEmbedding K E n d e) a * (j : GeneralLinearGroup d K) = g) :
64     embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e) ∈
65       CharacterNormalizer61.normalizer H θ :=
66   (hfull _).mpr ⟨ActualLocalUnitDecomposition.uniformizerUnit E, 1, by simp [embeddedUniformizer]⟩
67 
68 /-- The actual constructed extension domain is the full normalizer of the same theta. -/
69 theorem extendedSubgroup_eq_full_normalizer (hK : Continuous (algebraMap K E))
70     (hJ : J0 ≤ chainGroup K E n d e)
71     (hu : ∀ u : 𝒪[E]ˣ,
72       unitsEmbedding K E d (scalarMatrixEmbedding K E n d e) (unitEmbedding E u) ∈ J0)
73     (hfull : ∀ g : GeneralLinearGroup d K,
74       g ∈ CharacterNormalizer61.normalizer H θ ↔
75         ∃ a : Eˣ, ∃ j : J0,
76           unitsEmbedding K E d (scalarMatrixEmbedding K E n d e) a * (j : GeneralLinearGroup d K) = g) :
77     extendedSubgroup (compactGroup K E n d e H θ)
78       (embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e))
79       (uniformizer_normalizes_compactGroup K E n d e H θ
80         (uniformizer_mem_full_normalizer K E n d e H θ J0 hfull)) =
81       CharacterNormalizer61.normalizer H θ := by
82   let C := compactGroup K E n d e H θ
83   let t := embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e)
84   let ht := uniformizer_normalizes_compactGroup K E n d e H θ
85     (uniformizer_mem_full_normalizer K E n d e H θ J0 hfull)
86   have hC := compactGroup_eq_of_full_normalizer K E n d e H θ J0 hK hJ hu hfull
87   apply le_antisymm
88   · rw [extendedSubgroup_eq_sup]
89     exact sup_le inf_le_left (Subgroup.zpowers_le.mpr
90       (uniformizer_mem_full_normalizer K E n d e H θ J0 hfull))
91   · intro g hg
92     obtain ⟨a, j, he⟩ := (hfull g).mp hg
93     obtain ⟨r, k, hr⟩ := field_product_normalForm K E d
94       (scalarMatrixEmbedding K E n d e) J0 hu a j
95     rw [← he, hr]
96     exact (extendedSubgroup C t ht).mul_mem
97       ((extendedSubgroup C t ht).zpow_mem (generator_mem C t ht) r)
98       (le_extendedSubgroup C t ht (hC.symm ▸ k.property))
99 
100 end PaperXI.ActualCharacterIdentification61

Back to source controls