ActualFieldTypeQuotient69.lean

1 import PaperXI.ActualNormalizerTypeExtension58
2 import PaperXI.CompactQuotientPeriod69
3 import Mathlib.GroupTheory.Subgroup.Center
4 
5 /-! Compactness modulo the actual base-field scalar matrices for E-times-J. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.ActualFieldTypeQuotient69
9 open Matrix ValuativeRel
10 open ActualLocalUnitTopology ActualLocalUnitDecomposition
11 open ActualEmbeddedUniformizer58 ActualDepthZeroExtension
12 
13 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
14   [IsNonarchimedeanLocalField F]
15   [Field E] [ValuativeRel E] [TopologicalSpace E]
16   [IsNonarchimedeanLocalField E] [Algebra F E]
17 variable (n : Type*) [Fintype n] [DecidableEq n] [Nonempty n]
18   (ι : E →ₐ[F] Matrix n n F) (J : Subgroup (GeneralLinearGroup n F))
19 
20 /-- The actual subgroup generated by J and the embedded E-multiplicative group. -/
21 abbrev fieldGroup : Subgroup (GeneralLinearGroup n F) :=
22   J ⊔ (unitsEmbedding F E n ι).range
23 
24 /-- The actual base-field scalar matrices, as a subgroup of E-times-J. -/
25 def scalarHom : Fˣ →* fieldGroup F E n ι J where
26   toFun a := ⟨GeneralLinearGroup.scalar n a, (show (unitsEmbedding F E n ι).range ≤ fieldGroup F E n ι J from le_sup_right)
27     ⟨Units.map (algebraMap F E).toMonoidHom a, unitsEmbedding_baseScalar F E n ι a⟩⟩
28   map_one' := by ext; simp
29   map_mul' a b := by apply Subtype.ext; exact map_mul (GeneralLinearGroup.scalar n) a b
30 
31 def scalarSubgroup : Subgroup (fieldGroup F E n ι J) :=
32   (scalarHom F E n ι J).range
33 
34 omit [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F]
35   [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] [Nonempty n] in
36 theorem scalar_central (z : scalarSubgroup F E n ι J) (g : GeneralLinearGroup n F) :
37     Commute (((z : fieldGroup F E n ι J) : GeneralLinearGroup n F)) g := by
38   obtain ⟨a, ha⟩ := z.property
39   have hv := congrArg (fun x : fieldGroup F E n ι J => (x : GeneralLinearGroup n F)) ha
40   rw [← hv]
41   exact GeneralLinearGroup.scalar_commute a g
42 
43 instance scalar_normal : (scalarSubgroup F E n ι J).Normal :=
44   Subgroup.normal_of_le_center (by
45     intro z hz
46     apply Subgroup.mem_center_iff.mpr
47     intro g
48     apply Subtype.ext
49     exact (scalar_central F E n ι J ⟨z,hz⟩ g).eq.symm)
50 
51 def compactPart : Subgroup (fieldGroup F E n ι J) :=
52   J.subgroupOf (fieldGroup F E n ι J)
53 
54 /-- Determinant degree detects precisely J inside the field-generated group. -/
55 theorem degree_kernel
56     (hF : Continuous (algebraMap F E))
57     (hJ : IsCompact (J : Set (GeneralLinearGroup n F)))
58     (ht : embeddedUniformizer F E n ι ∈ Subgroup.normalizer (J : Set (GeneralLinearGroup n F)))
59     (hu : ∀ u : 𝒪[E]ˣ, unitsEmbedding F E n ι (unitEmbedding E u) ∈ J)
60     (g : fieldGroup F E n ι J) :
61     determinantDegree F n (g : GeneralLinearGroup n F) = 1 ↔
62       g ∈ compactPart F E n ι J := by
63   have hJker := CompactDegreeSeparation.compact_le_degree_ker J (determinantDegree F n)
64     (determinantDegree_continuous F n) hJ
65   have htn : determinantDegree F n (embeddedUniformizer F E n ι) ≠ 1 :=
66     embeddedUniformizer_degree_ne_one F E n ι (algebraEmbedding_continuous F E n ι hF)
67   constructor
68   · intro hg
69     have hmem : (g : GeneralLinearGroup n F) ∈
70         NormalizerExtensionInducing58.extendedSubgroup J (embeddedUniformizer F E n ι) ht := by
71       rw [ActualNormalizerTypeExtension58.extendedSubgroup_eq_field_join F E n ι J ht hu]
72       exact g.property
73     obtain ⟨p, hp⟩ := hmem
74     have he : determinantDegree F n (embeddedUniformizer F E n ι) ^ p.right.toAdd = 1 := by
75       rw [← hp, NormalizerExtensionInducing58.normalFormHom_apply, map_mul, map_zpow] at hg
76       have hj : determinantDegree F n (p.left : GeneralLinearGroup n F) = 1 :=
77         hJker p.left.property
78       simpa only [hj, one_mul] using hg
79     have hn : p.right.toAdd = 0 := by
80       have hd : (determinantDegree F n (embeddedUniformizer F E n ι)).toAdd ≠ 0 := by
81         intro hz
82         apply htn
83         exact Multiplicative.toAdd.injective hz
84       have hmul : p.right.toAdd *
85           (determinantDegree F n (embeddedUniformizer F E n ι)).toAdd = 0 := by
86         simpa only [toAdd_zpow, zsmul_eq_mul, Int.cast_id, toAdd_one] using congrArg Multiplicative.toAdd he
87       exact (mul_eq_zero.mp hmul).resolve_right hd
88     have hx : (g : GeneralLinearGroup n F) = p.left := by
89       rw [← hp, NormalizerExtensionInducing58.normalFormHom_apply, hn, zpow_zero, mul_one]
90     change (g : GeneralLinearGroup n F) ∈ J
91     rw [hx]
92     exact p.left.property
93   · intro hg
94     exact hJker hg
95 
96 /-- The determinant supplies a finite period in the quotient by genuine F-scalars.
97 The bound is the matrix rank, not a relabeled ramification index. -/
98 theorem quotient_compact
99     (hF : Continuous (algebraMap F E))
100     (hJ : IsCompact (J : Set (GeneralLinearGroup n F)))
101     (ht : embeddedUniformizer F E n ι ∈ Subgroup.normalizer (J : Set (GeneralLinearGroup n F)))
102     (hu : ∀ u : 𝒪[E]ˣ, unitsEmbedding F E n ι (unitEmbedding E u) ∈ J) :
103     CompactSpace (fieldGroup F E n ι J ⧸ scalarSubgroup F E n ι J) := by
104   let H := fieldGroup F E n ι J
105   let Z := scalarSubgroup F E n ι J
106   let C := compactPart F E n ι J
107   let t : H := ⟨embeddedUniformizer F E n ι,
108     (show (unitsEmbedding F E n ι).range ≤ H from le_sup_right) ⟨uniformizerUnit E, rfl⟩⟩
109   let z : H := scalarHom F E n ι J (uniformizerUnit F)
110   let q := QuotientGroup.mk' Z
111   have hC : IsCompact (C : Set H) := by
112     apply Topology.IsEmbedding.isCompact_iff
113       (f := fun x : H => (x : GeneralLinearGroup n F)) Topology.IsEmbedding.subtypeVal |>.mpr
114     convert hJ using 1
115     ext x
116     constructor
117     · rintro ⟨g,hg,rfl⟩
118       exact hg
119     · intro hx
120       exact ⟨⟨x, (show J ≤ H from le_sup_left) hx⟩, hx, rfl⟩
121   have hcover : ∀ g : H, ∃ r : ℤ, ∃ j : C, g = t ^ r * (j : H) := by
122     intro g
123     have hmem : ((g⁻¹ : H) : GeneralLinearGroup n F) ∈
124         NormalizerExtensionInducing58.extendedSubgroup J (embeddedUniformizer F E n ι) ht := by
125       rw [ActualNormalizerTypeExtension58.extendedSubgroup_eq_field_join F E n ι J ht hu]
126       exact (g⁻¹).property
127     obtain ⟨p,hp⟩ := hmem
128     refine ⟨-p.right.toAdd, ⟨⟨(p.left : GeneralLinearGroup n F)⁻¹,
129       (show J ≤ H from le_sup_left) (J.inv_mem p.left.property)⟩, J.inv_mem p.left.property⟩, ?_⟩
130     apply Subtype.ext
131     change (g : GeneralLinearGroup n F) =
132       embeddedUniformizer F E n ι ^ (-p.right.toAdd) * (p.left : GeneralLinearGroup n F)⁻¹
133     have he := congrArg Inv.inv hp
134     change (NormalizerExtensionInducing58.normalFormHom J
135       (embeddedUniformizer F E n ι) ht p)⁻¹ = (g : GeneralLinearGroup n F) at he
136     simpa only [NormalizerExtensionInducing58.normalFormHom_apply, _root_.mul_inv_rev,
137       ← zpow_neg] using he.symm
138   let d : ℤ := (determinantDegree F n (embeddedUniformizer F E n ι)).toAdd
139   have hb : t ^ Fintype.card n * z ^ (-d) ∈ C := by
140     apply (degree_kernel F E n ι J hF hJ ht hu _).mp
141     change determinantDegree F n
142       (embeddedUniformizer F E n ι ^ Fintype.card n *
143         scalarUniformizer F n ^ (-d)) = 1
144     rw [map_mul, map_pow, map_zpow, determinantDegree_scalarUniformizer]
145     apply Multiplicative.toAdd.injective
146     change (Fintype.card n : ℤ) * d + (-d) * (Fintype.card n : ℤ) = 0
147     ring
148   have hz : q z = 1 := (QuotientGroup.eq_one_iff _).mpr
149     ⟨uniformizerUnit F,rfl⟩
150   have hperiod : q t ^ Fintype.card n ∈ C.map q := by
151     have hp : q (t ^ Fintype.card n * z ^ (-d)) ∈ C.map q :=
152       Subgroup.mem_map.mpr ⟨_,hb,rfl⟩
153     simpa only [map_mul, map_pow, map_zpow, hz, one_zpow, mul_one] using hp
154   exact CompactQuotientPeriod69.compact_quotient_of_period C Z t hC hcover
155     (Fintype.card n) Fintype.card_pos hperiod
156 
157 end PaperXI.ActualFieldTypeQuotient69

Back to source controls