PrescribedFieldType70.lean

1 import PaperXI.ActualCompactTypeCompletion58
2 import PaperXI.ActualFieldTypeQuotient69
3 
4 /-! Construction of the full inducing representation from the same compact
5 first factor and actual finite quotient. The full-H locus is a later condition
6 on this exact constructed extension, not on an unrelated supplied Lambda. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.PrescribedFieldType70
10 open Matrix ValuativeRel Representation
11 open scoped TensorProduct
12 open ActualEmbeddedUniformizer58 ActualFieldTypeQuotient69 NormalizerExtensionInducing58
13 
14 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
15   [IsNonarchimedeanLocalField F] [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   (ht : embeddedUniformizer F E n ι ∈ Subgroup.normalizer (J : Set (GeneralLinearGroup n F)))
20   (hu : ∀ u : 𝒪[E]ˣ, unitsEmbedding F E n ι (ActualLocalUnitTopology.unitEmbedding E u) ∈ J)
21 variable {Q W U : Type*} [Group Q] [Finite Q]
22   [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
23   [AddCommGroup U] [Module ℂ U]
24 variable (N : Subgroup J) (q : J →* Q) (hN : N ≤ q.ker)
25   (κ : Representation ℂ J W) (σ : Representation ℂ Q U)
26 
27 /-- Literal inclusion of the compact group into the field-generated subgroup. -/
28 def compactInclusion : J →* fieldGroup F E n ι J := Subgroup.inclusion le_sup_left
29 
30 /-- The actual extension-field uniformizer in the field-generated subgroup. -/
31 def fieldGenerator : fieldGroup F E n ι J :=
32   ⟨embeddedUniformizer F E n ι, (show (unitsEmbedding F E n ι).range ≤ fieldGroup F E n ι J from le_sup_right)
33     ⟨ActualLocalUnitDecomposition.uniformizerUnit E, rfl⟩⟩
34 
35 /-- Identifies the previously constructed normalizer coordinates with the
36 literal arithmetic field join. Its underlying ambient map is the identity. -/
37 def domainEquiv : extendedSubgroup J (embeddedUniformizer F E n ι) ht ≃*
38     fieldGroup F E n ι J := MulEquiv.subgroupCongr
39   (ActualNormalizerTypeExtension58.extendedSubgroup_eq_field_join F E n ι J ht hu)
40 
41 include hu hN in
42 /-- On the actual arithmetic group, construct the extension and retain both
43 its compact action and its exact first-factor uniformizer operator. -/
44 theorem exists_prescribed_extension
45     (hF : Continuous (algebraMap F E))
46     (hJc : IsCompact (J : Set (GeneralLinearGroup n F)))
47     (hJo : IsOpen (J : Set (GeneralLinearGroup n F)))
48     (hNo : IsOpen (N : Set J)) (hq : Function.Surjective q)
49     (hqa : ∀ j, q (conjugation J (embeddedUniformizer F E n ι) ht j) = q j)
50     [IsIrreducible (κ.comp N.subtype)] [IsIrreducible σ]
51     (hκ : SmoothDegreeQuotient.IsSmooth κ)
52     (T : IntertwiningMap κ (κ.comp (conjugation J (embeddedUniformizer F E n ι) ht).toMonoidHom))
53     (hT : T ≠ 0) :
54     FiniteDimensional ℂ (W ⊗[ℂ] U) ∧
55     ∃ Λ : Representation ℂ (fieldGroup F E n ι J) (W ⊗[ℂ] U),
56       (∀ j : J, Λ (compactInclusion F E n ι J j) = CompactTypeTensor58.action q κ σ j) ∧
57       (∀ w u, Λ (fieldGenerator F E n ι J) (w ⊗ₜ[ℂ] u) = T w ⊗ₜ[ℂ] u) ∧
58       IsIrreducible Λ ∧ SmoothDegreeQuotient.IsSmooth Λ := by
59   obtain ⟨hf, _, _, _, L, hr, hg, hi, hs⟩ :=
60     ActualCompactTypeCompletion58.completed F E n ι J ht N q hN κ σ
61       hF hJc hJo hNo hq hqa hκ T hT
62   let e := domainEquiv F E n ι J ht hu
63   let Λ := L.comp e.symm.toMonoidHom
64   have hei (j : J) : e.symm (compactInclusion F E n ι J j) =
65       subgroupInclusion J (embeddedUniformizer F E n ι) ht j := Subtype.ext rfl
66   have heg : e.symm (fieldGenerator F E n ι J) =
67       generator J (embeddedUniformizer F E n ι) ht := Subtype.ext rfl
68   have hLs : SmoothDegreeQuotient.IsSmooth Λ := by
69     intro x
70     have he : (SmoothDegreeQuotient.vectorStabilizer Λ x : Set (fieldGroup F E n ι J)) =
71         e.symm ⁻¹' (SmoothDegreeQuotient.vectorStabilizer L x : Set _) := rfl
72     rw [he]
73     have hc : Continuous e.symm := continuous_subtype_val.subtype_mk _
74     exact (hs x).preimage hc
75   let : IsIrreducible L := hi
76   have hLi : IsIrreducible Λ :=
77     (QuotientRepresentation.irreducible_comp_iff e.symm.toMonoidHom e.symm.surjective L).mpr hi
78   refine ⟨hf, Λ, ?_, ?_, hLi, hLs⟩
79   · intro j
80     change L (e.symm (compactInclusion F E n ι J j)) = _
81     rw [hei, hr]
82   · intro w u
83     change L (e.symm (fieldGenerator F E n ι J)) (w ⊗ₜ[ℂ] u) = _
84     rw [heg]
85     exact hg w u
86 
87 end PaperXI.PrescribedFieldType70

Back to source controls