ActualNormalizerTypeExtension58.lean

1 import PaperXI.ActualEmbeddedUniformizer58
2 import PaperXI.NormalizerExtensionInducing58
3 
4 /-!
5 # Actual embedded-field normalizer extension
6 
7 The noncentral matrix uniformizer's freeness is proved from compactness and
8 actual local-field arithmetic. Given its actual normalization of the compact
9 subgroup and one nonzero intertwiner, the literal representation is extended.
10 Simple-character normalization and beta-extension intertwining are explicit
11 remaining arithmetic inputs; no claim that they have been constructed is made.
12 -/
13 set_option autoImplicit false
14 noncomputable section
15 namespace PaperXI.ActualNormalizerTypeExtension58
16 
17 open Matrix ValuativeRel Representation
18 open ActualEmbeddedUniformizer58 NormalizerExtensionInducing58
19 
20 variable (K E : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
21   [IsNonarchimedeanLocalField K]
22   [Field E] [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E]
23   [Algebra K E]
24 variable (n : Type*) [Fintype n] [DecidableEq n] [Nonempty n]
25   (ι : E →ₐ[K] Matrix n n K)
26 variable (J : Subgroup (GeneralLinearGroup n K))
27   (ht : embeddedUniformizer K E n ι ∈ Subgroup.normalizer (J : Set (GeneralLinearGroup n K)))
28 
29 omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Nonempty n] in
30 /-- With integral E-units in J, the generated subgroup is exactly the join
31 of J and the actual embedded multiplicative group of E. -/
32 theorem extendedSubgroup_eq_field_join
33     (hunits : ∀ u : 𝒪[E]ˣ,
34       unitsEmbedding K E n ι (ActualLocalUnitTopology.unitEmbedding E u) ∈ J) :
35     extendedSubgroup J (embeddedUniformizer K E n ι) ht =
36       J ⊔ (unitsEmbedding K E n ι).range := by
37   apply le_antisymm
38   · rw [extendedSubgroup_eq_sup]
39     apply sup_le le_sup_left
40     apply Subgroup.zpowers_le.mpr
41     exact (show (unitsEmbedding K E n ι).range ≤ J ⊔ (unitsEmbedding K E n ι).range from
42       le_sup_right) ⟨ActualLocalUnitDecomposition.uniformizerUnit E, rfl⟩
43   · apply sup_le (le_extendedSubgroup J (embeddedUniformizer K E n ι) ht)
44     rintro g ⟨a, rfl⟩
45     obtain ⟨r, j, hj⟩ := field_product_normalForm K E n ι J hunits a 1
46     have he : unitsEmbedding K E n ι a = embeddedUniformizer K E n ι ^ r * j := by
47       simpa using hj
48     rw [he]
49     exact Subgroup.mul_mem _
50       (Subgroup.zpow_mem _ (generator_mem J (embeddedUniformizer K E n ι) ht) r)
51       (le_extendedSubgroup J (embeddedUniformizer K E n ι) ht j.property)
52 
53 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
54   (σ : Representation ℂ J V)
55 
56 /-- Actual matrix-field freeness discharges the cyclic extension obstruction.
57 One nonzero actual intertwiner produces a smooth irreducible extension on the
58 literal ambient subgroup. Neither centrality nor induced-category conclusions
59 are assumed. -/
60 theorem exists_smooth_irreducible_extension
61     (hK : Continuous (algebraMap K E))
62     (hcompact : IsCompact (J : Set (GeneralLinearGroup n K)))
63     (hopen : IsOpen (J : Set (GeneralLinearGroup n K)))
64     [IsIrreducible σ] (hsmooth : SmoothDegreeQuotient.IsSmooth σ)
65     (T : IntertwiningMap σ
66       (σ.comp (conjugation J (embeddedUniformizer K E n ι) ht).toMonoidHom))
67     (hT : T ≠ 0) :
68     ∃ Λ : Representation ℂ (extendedSubgroup J (embeddedUniformizer K E n ι) ht) V,
69       (∀ j : J, Λ (subgroupInclusion J (embeddedUniformizer K E n ι) ht j) = σ j) ∧
70       Λ (generator J (embeddedUniformizer K E n ι) ht) = T.toLinearMap ∧
71       IsIrreducible Λ ∧ SmoothDegreeQuotient.IsSmooth Λ := by
72   let t := embeddedUniformizer K E n ι
73   have hfree := embeddedUniformizer_free_of_algebraMap K E n ι hK J hcompact
74   let e := T.ofBijective (intertwiner_bijective J t ht σ T hT)
75   refine ⟨extensionOfEquiv J t ht σ e hfree, ?_, ?_, ?_, ?_⟩
76   · intro j
77     exact extensionOfEquiv_restrict J t ht σ e hfree j
78   · exact extensionOfEquiv_generator J t ht σ e hfree
79   · exact extendedRepresentation_irreducible J t ht σ _ _ hfree
80   · exact extendedRepresentation_smooth J t ht σ _ _ hfree hopen hsmooth
81 
82 end PaperXI.ActualNormalizerTypeExtension58

Back to source controls