ActualLocalUnitDecomposition.lean

1 import PaperXI.ActualLocalUnitTopology
2 import Mathlib.RingTheory.DiscreteValuationRing.Basic
3 import Mathlib.Topology.Algebra.Group.Neighborhood
4 import Mathlib.Topology.Instances.Int
5 
6 /-!
7 # Actual local-field unit and uniformizer coordinates
8 
9 The uniformizer is chosen from the proved DVR structure of the actual ring of
10 integers. Existence of coordinates comes from fraction-field factorization;
11 uniqueness comes from the actual valuation. No split group is supplied.
12 -/
13 set_option autoImplicit false
14 noncomputable section
15 namespace PaperXI.ActualLocalUnitDecomposition
16 open ValuativeRel ActualLocalUnitTopology
17 
18 variable (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
19   [IsNonarchimedeanLocalField K]
20 
21 /-- A uniformizer chosen inside the actual local-field integer ring. -/
22 def uniformizer : 𝒪[K] := Classical.choose (IsDiscreteValuationRing.exists_irreducible 𝒪[K])
23 
24 theorem uniformizer_irreducible : Irreducible (uniformizer K) :=
25   Classical.choose_spec (IsDiscreteValuationRing.exists_irreducible 𝒪[K])
26 
27 theorem uniformizer_ne_zero : (uniformizer K : K) ≠ 0 := by
28   exact_mod_cast (uniformizer_irreducible K).ne_zero
29 
30 /-- The chosen uniformizer as an actual element of `Kˣ`. -/
31 def uniformizerUnit : Kˣ := Units.mk0 (uniformizer K : K) (uniformizer_ne_zero K)
32 
33 @[simp] theorem uniformizerUnit_coe : (uniformizerUnit K : K) = (uniformizer K : K) := rfl
34 
35 theorem uniformizer_value_pos : 0 < valuation K (uniformizer K : K) :=
36   Valuation.integer.v_irreducible_pos (uniformizer_irreducible K)
37 
38 theorem uniformizer_value_lt_one : valuation K (uniformizer K : K) < 1 :=
39   Valuation.integer.v_irreducible_lt_one (uniformizer_irreducible K)
40 
41 /-- Multiplication of an actual integer-ring unit by an integral uniformizer power. -/
42 def normalFormHom : 𝒪[K]ˣ × Multiplicative ℤ →* Kˣ where
43   toFun p := unitEmbedding K p.1 * uniformizerUnit K ^ p.2.toAdd
44   map_one' := by simp
45   map_mul' := by
46     rintro ⟨u, m⟩ ⟨v, n⟩
47     change unitEmbedding K (u * v) * uniformizerUnit K ^ (m.toAdd + n.toAdd) = _
48     simp [map_mul, zpow_add, mul_mul_mul_comm]
49 
50 @[simp] theorem normalFormHom_apply (u : 𝒪[K]ˣ) (n : Multiplicative ℤ) :
51     normalFormHom K (u, n) = unitEmbedding K u * uniformizerUnit K ^ n.toAdd := rfl
52 
53 /-- Existence is a theorem about the actual fraction field of the actual DVR. -/
54 theorem normalForm_surjective : Function.Surjective (normalFormHom K) := by
55   intro x
56   obtain ⟨n, u, hu⟩ := IsDiscreteValuationRing.exists_units_eq_smul_zpow_of_irreducible
57     (K := K) (uniformizer_irreducible K) x.ne_zero
58   refine ⟨(u, Multiplicative.ofAdd n), ?_⟩
59   apply Units.ext
60   have hmap (a : 𝒪[K]) : algebraMap 𝒪[K] K a = (a : K) := rfl
61   simpa [normalFormHom, unitEmbedding, uniformizerUnit, Units.smul_def, Algebra.smul_def, hmap]
62     using hu.symm
63 
64 /-- The integer exponent and the residual actual unit are both unique. -/
65 theorem normalForm_injective : Function.Injective (normalFormHom K) := by
66   apply (injective_iff_map_eq_one _).mpr
67   rintro ⟨u, n⟩ h
68   have huval : valuation K (algebraMap 𝒪[K] K (u : 𝒪[K])) = 1 :=
69     (Valuation.integer.integers (valuation K)).valuation_unit u
70   have hv := congrArg (fun x : Kˣ => valuation K (x : K)) h
71   have hnval : valuation K (uniformizer K : K) ^ n.toAdd = 1 := by
72     simpa [normalFormHom, unitEmbedding, uniformizerUnit, map_mul, huval] using hv
73   have hn : n.toAdd = 0 :=
74     (zpow_right_injective₀ (uniformizer_value_pos K) (uniformizer_value_lt_one K).ne)
75       (by simpa using hnval)
76   have hn' : n = 1 := congrArg Multiplicative.ofAdd hn
77   subst n
78   have hu : u = 1 := unitEmbedding_injective K (by simpa using h)
79   simp [hu]
80 
81 /-- Multiplicative coordinates on the actual multiplicative group of the local field. -/
82 def normalFormEquiv : (𝒪[K]ˣ × Multiplicative ℤ) ≃* Kˣ :=
83   MulEquiv.ofBijective (normalFormHom K) ⟨normalForm_injective K, normalForm_surjective K⟩
84 
85 @[simp] theorem normalFormEquiv_apply (u : 𝒪[K]ˣ) (n : Multiplicative ℤ) :
86     normalFormEquiv K (u, n) = unitEmbedding K u * uniformizerUnit K ^ n.toAdd := rfl
87 
88 /-- The actual normalized integer valuation, positive on the chosen uniformizer. -/
89 def degree : Kˣ →* Multiplicative ℤ :=
90   (MonoidHom.snd 𝒪[K]ˣ (Multiplicative ℤ)).comp (normalFormEquiv K).symm.toMonoidHom
91 
92 @[simp] theorem degree_normalForm (u : 𝒪[K]ˣ) (n : Multiplicative ℤ) :
93     degree K (unitEmbedding K u * uniformizerUnit K ^ n.toAdd) = n := by
94   change ((normalFormEquiv K).symm (normalFormEquiv K (u, n))).2 = n
95   rw [MulEquiv.symm_apply_apply]
96 
97 @[simp] theorem degree_unit (u : 𝒪[K]ˣ) : degree K (unitEmbedding K u) = 1 := by
98   simpa using degree_normalForm K u 1
99 
100 theorem degree_unitEmbedding (u : 𝒪[K]ˣ) : degree K (unitEmbedding K u) = 1 :=
101   degree_unit K u
102 
103 @[simp] theorem degree_uniformizer : degree K (uniformizerUnit K) = Multiplicative.ofAdd (1 : ℤ) := by
104   simpa using degree_normalForm K 1 (Multiplicative.ofAdd 1)
105 
106 /-- The degree-zero subgroup is literally the compact open unit subgroup. -/
107 theorem ker_degree : (degree K).ker = compactUnitSubgroup K := by
108   ext x
109   constructor
110   · intro hx
111     obtain ⟨⟨u, n⟩, rfl⟩ := (normalFormEquiv K).surjective x
112     have hn : n = 1 := by simpa using hx
113     subst n
114     exact ⟨u, by simp⟩
115   · rintro ⟨u, rfl⟩
116     exact degree_unit K u
117 
118 /-- Continuity follows from the proved openness of the actual unit subgroup. -/
119 theorem degree_continuous : Continuous (degree K) := by
120   apply continuous_of_tendsto_nhds_one (degree K)
121   have hker : IsOpen ((degree K).ker : Set Kˣ) := by
122     rw [ker_degree]
123     exact isOpen_compactUnitSubgroup K
124   have he : ∀ᶠ x in nhds (1 : Kˣ), (1 : Multiplicative ℤ) = degree K x :=
125     Filter.mem_of_superset (hker.mem_nhds (Subgroup.one_mem _)) fun x hx => hx.symm
126   exact (Filter.tendsto_congr' he).mp tendsto_const_nhds
127 
128 end PaperXI.ActualLocalUnitDecomposition

Back to source controls