ActualELatticeFieldJoin59.lean

1 import PaperXI.ActualELatticeQuotient59
2 import PaperXI.ActualELatticeFreeness59
3 
4 /-!
5 # The literal field-times-lattice inducing subgroup
6 
7 Integral extension-field units already lie in the actual integral matrix
8 factor. The unit/uniformizer decomposition of E× therefore identifies the
9 subgroup generated by J and pi_E with the subgroup generated by J and E×.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.ActualELatticeFieldJoin59
14 open Matrix ValuativeRel
15 open ActualELatticeResidue59 ActualELatticeTypeGroup59 ActualELatticeQuotient59
16 open ActualELatticeFreeness59 NormalizerExtensionInducing58
17 
18 variable (K E : Type*) [Field K] [Field E] [Algebra K E]
19 variable (n : Type*) [Fintype n] [DecidableEq n]
20 variable [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E]
21 
22 omit [TopologicalSpace E] [IsNonarchimedeanLocalField E] in
23 /-- An integral scalar matrix acts by the actual extension-field unit. -/
24 theorem integralMatrix_scalar (u : 𝒪[E]ˣ) :
25     integralMatrix K E n (GeneralLinearGroup.scalar n u) =
26       scalarAction K E n (ActualLocalUnitTopology.unitEmbedding E u) := by
27   ext v i
28   simp [integralMatrix, restrictScalarMatrix, ActualIntegralGeneralLinear.embedding,
29     GeneralLinearGroup.map_scalar, Matrix.mulVec, dotProduct, Matrix.scalar_apply,
30     scalarAction_apply, ActualLocalUnitTopology.unitEmbedding, Matrix.diagonal_apply]
31   exact Or.inl rfl
32 
33 /-- Every actual integral E-unit lies in the literal product group. -/
34 theorem integralUnit_mem_typeGroup (u : 𝒪[E]ˣ) :
35     scalarAction K E n (ActualLocalUnitTopology.unitEmbedding E u) ∈ typeGroup K E n := by
36   exact (show integralImage K E n ≤ typeGroup K E n from le_sup_left)
37     ⟨GeneralLinearGroup.scalar n u, integralMatrix_scalar K E n u⟩
38 
39 /-- Exact identification of the extension domain with the actual E×-join. -/
40 theorem extendedSubgroup_eq_field_join :
41     extendedSubgroup (typeGroup K E n) (uniformizerAction K E n)
42       (uniformizer_normalizes K E n) =
43       typeGroup K E n ⊔ (scalarAction K E n).range := by
44   apply le_antisymm
45   · rw [extendedSubgroup_eq_sup]
46     apply sup_le le_sup_left
47     apply Subgroup.zpowers_le.mpr
48     exact (show (scalarAction K E n).range ≤
49       typeGroup K E n ⊔ (scalarAction K E n).range from le_sup_right)
50       ⟨ActualLocalUnitDecomposition.uniformizerUnit E, rfl⟩
51   · apply sup_le (le_extendedSubgroup _ _ _)
52     rintro g ⟨a, rfl⟩
53     obtain ⟨⟨u, r⟩, ha⟩ := (ActualLocalUnitDecomposition.normalFormEquiv E).surjective a
54     rw [← ha, ActualLocalUnitDecomposition.normalFormEquiv_apply, map_mul, map_zpow]
55     apply Subgroup.mul_mem
56     · exact le_extendedSubgroup _ _ _ (integralUnit_mem_typeGroup K E n u)
57     · exact Subgroup.zpow_mem _ (generator_mem _ _ _) r.toAdd
58 
59 /-- The entire actual field group normalizes the literal lattice-product group. -/
60 theorem field_normalizes_typeGroup : (scalarAction K E n).range ≤
61     Subgroup.normalizer (typeGroup K E n : Set ((n → E) ≃ₗ[K] (n → E))) := by
62   rintro g ⟨a, rfl⟩
63   obtain ⟨⟨u, r⟩, ha⟩ := (ActualLocalUnitDecomposition.normalFormEquiv E).surjective a
64   rw [← ha, ActualLocalUnitDecomposition.normalFormEquiv_apply, map_mul, map_zpow]
65   apply Subgroup.mul_mem
66   · exact (typeGroup K E n).le_normalizer (integralUnit_mem_typeGroup K E n u)
67   · exact Subgroup.zpow_mem _ (uniformizer_normalizes K E n) r.toAdd
68 
69 open scoped Pointwise
70 /-- Setwise, the actual extension domain is exactly E× times J. -/
71 theorem extendedSubgroup_coe_eq_field_mul :
72     (extendedSubgroup (typeGroup K E n) (uniformizerAction K E n)
73       (uniformizer_normalizes K E n) : Set ((n → E) ≃ₗ[K] (n → E))) =
74       ((scalarAction K E n).range : Set ((n → E) ≃ₗ[K] (n → E))) *
75         (typeGroup K E n : Set ((n → E) ≃ₗ[K] (n → E))) := by
76   rw [extendedSubgroup_eq_field_join, sup_comm]
77   exact Subgroup.coe_mul_of_left_le_normalizer_right
78     (scalarAction K E n).range (typeGroup K E n) (field_normalizes_typeGroup K E n)
79 
80 end PaperXI.ActualELatticeFieldJoin59

Back to source controls