ActualCharacterResidue61.lean

1 import PaperXI.ActualCharacterType61
2 import PaperXI.ActualELatticeFieldJoin59
3 
4 /-!
5 # Actual residue reduction on the theta-dependent compact group
6 
7 The map is the restriction of the already constructed literal lattice residue
8 map. Its kernel is the actual intersection C(theta)∩U_a1. Containment in the
9 lattice-product group and normalization of theta by integral centralizer
10 matrices are explicit standard-type inputs. They do not assert C(theta)=B U_a1.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 namespace PaperXI.ActualCharacterResidue61
15 open Matrix ValuativeRel
16 open ActualCharacterType61 ActualELatticeTopology60 ActualELatticeResidue59
17 open ActualELatticeTypeGroup59 ActualELatticeQuotient59 LatticeCongruenceTopology60
18 open ActualEmbeddedUniformizer58 NormalizerExtensionInducing58
19 
20 variable (K E : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
21   [IsNonarchimedeanLocalField K] [Field E] [ValuativeRel E] [TopologicalSpace E]
22   [IsNonarchimedeanLocalField E] [Algebra K E]
23 variable (n d : Type*) [Fintype n] [DecidableEq n] [Fintype d] [DecidableEq d]
24   [Nonempty d] (e : (n → E) ≃L[K] (d → K))
25 variable (H : Subgroup (GeneralLinearGroup d K)) (θ : H →* ℂˣ)
26 variable (hmodel : compactGroup K E n d e H θ ≤ matrixType K E n d e)
27 
28 /-- Actual inclusion into the larger lattice-product group through the same coordinates. -/
29 def intoModel : compactGroup K E n d e H θ →* typeGroup K E n where
30   toFun c := ⟨coordinateAut e c, hmodel c.property⟩
31   map_one' := Subtype.ext ((coordinateAut e).map_one)
32   map_mul' x y := Subtype.ext ((coordinateAut e).map_mul x y)
33 
34 /-- Restriction of the actual Block59 residue map, not a newly supplied map. -/
35 def reduction : compactGroup K E n d e H θ →* GeneralLinearGroup n 𝓀[E] :=
36   (ActualELatticeQuotient59.reduction K E n).comp (intoModel K E n d e H θ hmodel)
37 
38 omit [ValuativeRel K] [IsNonarchimedeanLocalField K] [Nonempty d] in
39 /-- The actual theta-dependent first subgroup is exactly the residue kernel. -/
40 theorem reduction_kernel : (reduction K E n d e H θ hmodel).ker = firstSubgroup K E n d e H θ := by
41   ext c
42   change intoModel K E n d e H θ hmodel c ∈ (ActualELatticeQuotient59.reduction K E n).ker ↔ _
43   rw [ActualELatticeQuotient59.reduction_kernel]
44   rfl
45 
46 omit [ValuativeRel K] [IsNonarchimedeanLocalField K] [Nonempty d] in
47 /-- Integral centralizer matrices normalizing theta lie in the constructed compact group. -/
48 theorem integralMatrix_mem_compactGroup
49     (hB : ∀ b : GeneralLinearGroup n 𝒪[E], (coordinateAut e).symm (integralMatrix K E n b) ∈
50       CharacterNormalizer61.normalizer H θ) (b : GeneralLinearGroup n 𝒪[E]) :
51     (coordinateAut e).symm (integralMatrix K E n b) ∈ compactGroup K E n d e H θ := by
52   refine ⟨hB b, ?_⟩
53   change coordinateAut e ((coordinateAut e).symm (integralMatrix K E n b)) ∈
54     ActualELatticeNormalizer59.chainStabilizer (latticeChain K E n)
55   rw [MulEquiv.apply_symm_apply]
56   exact integralMatrix_mem_stabilizer K E n b
57 
58 omit [ValuativeRel K] [IsNonarchimedeanLocalField K] [Nonempty d] in
59 /-- The actual integral E-units belong to the same theta-dependent compact group. -/
60 theorem integralUnit_mem_compactGroup
61     (hB : ∀ b : GeneralLinearGroup n 𝒪[E], (coordinateAut e).symm (integralMatrix K E n b) ∈
62       CharacterNormalizer61.normalizer H θ) (u : 𝒪[E]ˣ) :
63     unitsEmbedding K E d (scalarMatrixEmbedding K E n d e)
64       (ActualLocalUnitTopology.unitEmbedding E u) ∈ compactGroup K E n d e H θ := by
65   have h := integralMatrix_mem_compactGroup K E n d e H θ hB (GeneralLinearGroup.scalar n u)
66   have he : (coordinateAut e).symm (integralMatrix K E n (GeneralLinearGroup.scalar n u)) =
67       unitsEmbedding K E d (scalarMatrixEmbedding K E n d e)
68         (ActualLocalUnitTopology.unitEmbedding E u) := by
69     apply (coordinateAut e).injective
70     rw [MulEquiv.apply_symm_apply, coordinateAut_unitsEmbedding,
71       ActualELatticeFieldJoin59.integralMatrix_scalar]
72   exact he ▸ h
73 
74 omit [ValuativeRel K] [IsNonarchimedeanLocalField K] [Nonempty d] in
75 /-- Surjectivity follows from integral centralizer matrices, while the kernel remains only their actual intersection. -/
76 theorem reduction_surjective
77     (hB : ∀ b : GeneralLinearGroup n 𝒪[E], (coordinateAut e).symm (integralMatrix K E n b) ∈
78       CharacterNormalizer61.normalizer H θ) :
79     Function.Surjective (reduction K E n d e H θ hmodel) := by
80   intro x
81   obtain ⟨g, hg⟩ := ActualELatticeQuotient59.reduction_surjective K E n x
82   have hmem := g.property
83   change (g : (n → E) ≃ₗ[K] (n → E)) ∈
84     integralImage K E n ⊔ ActualELatticeTypeGroup59.congruence K E n at hmem
85   rw [← SetLike.mem_coe,
86     Subgroup.coe_mul_of_left_le_normalizer_right _ _ (integralImage_normalizes K E n)] at hmem
87   obtain ⟨b, hb, u, hu, hbu⟩ := hmem
88   obtain ⟨b0, rfl⟩ := hb
89   let c : compactGroup K E n d e H θ :=
90     ⟨(coordinateAut e).symm (integralMatrix K E n b0),
91       integralMatrix_mem_compactGroup K E n d e H θ hB b0⟩
92   let u0 : typeGroup K E n := ⟨u, (show ActualELatticeTypeGroup59.congruence K E n ≤
93     typeGroup K E n from le_sup_right) hu⟩
94   have hu0 : ActualELatticeQuotient59.reduction K E n u0 = 1 := by
95     change u0 ∈ (ActualELatticeQuotient59.reduction K E n).ker
96     rw [ActualELatticeQuotient59.reduction_kernel]
97     exact hu
98   have hge : g = intoModel K E n d e H θ hmodel c * u0 := by
99     apply Subtype.ext
100     change (g : (n → E) ≃ₗ[K] (n → E)) =
101       coordinateAut e ((coordinateAut e).symm (integralMatrix K E n b0)) * u
102     rw [MulEquiv.apply_symm_apply]
103     exact hbu.symm
104   refine ⟨c, ?_⟩
105   rw [hge, map_mul, hu0, mul_one] at hg
106   exact hg
107 
108 omit [ValuativeRel K] [IsNonarchimedeanLocalField K] [Nonempty d] in
109 /-- Uniformizer conjugation preserves the same actual restricted residue matrix. -/
110 theorem reduction_conjugation
111     (hθ : embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e) ∈
112       CharacterNormalizer61.normalizer H θ)
113     (c : compactGroup K E n d e H θ) :
114     reduction K E n d e H θ hmodel
115       (conjugation (compactGroup K E n d e H θ)
116         (embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e))
117         (uniformizer_normalizes_compactGroup K E n d e H θ hθ) c) =
118       reduction K E n d e H θ hmodel c := by
119   have he : intoModel K E n d e H θ hmodel
120       (conjugation (compactGroup K E n d e H θ)
121         (embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e))
122         (uniformizer_normalizes_compactGroup K E n d e H θ hθ) c) =
123       uniformizerConjugation K E n (intoModel K E n d e H θ hmodel c) := by
124     apply Subtype.ext
125     change coordinateAut e (embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e) *
126       (c : GeneralLinearGroup d K) * (embeddedUniformizer K E d (scalarMatrixEmbedding K E n d e))⁻¹) =
127       uniformizerAction K E n * coordinateAut e c * (uniformizerAction K E n)⁻¹
128     rw [map_mul, map_mul, map_inv, coordinateAut_embeddedUniformizer]
129   change ActualELatticeQuotient59.reduction K E n _ = _
130   rw [he]
131   exact ActualELatticeQuotient59.reduction_conjugation K E n _
132 
133 end PaperXI.ActualCharacterResidue61

Back to source controls