ActualLocalUnitTopology.lean

1 import Mathlib.NumberTheory.LocalField.Basic
2 import Mathlib.Topology.Algebra.Group.Units
3 import Mathlib.Topology.Homeomorph.Lemmas
4 
5 /-!
6 # The actual compact open unit subgroup of a nonarchimedean local field
7 
8 The subgroup is the image of the unit group of the valuation ring under its
9 canonical embedding in the field. Its topological properties are derived from
10 the local-field hypotheses; they are not assumptions on an abstract subgroup.
11 No characteristic-zero hypothesis is used.
12 -/
13 
14 namespace PaperXI.ActualLocalUnitTopology
15 
16 open ValuativeRel
17 
18 noncomputable section
19 
20 variable (K : Type*) [Field K] [ValuativeRel K]
21 
22 /-- The canonical homomorphism from integral units to nonzero field elements. -/
23 def unitEmbedding : 𝒪[K]ˣ →* Kˣ :=
24   Units.map (algebraMap 𝒪[K] K).toMonoidHom
25 
26 /-- The actual integral-unit subgroup of the multiplicative group of the field. -/
27 def compactUnitSubgroup : Subgroup Kˣ := (unitEmbedding K).range
28 
29 @[simp] theorem coe_unitEmbedding (u : 𝒪[K]ˣ) :
30     ((unitEmbedding K u : Kˣ) : K) = algebraMap 𝒪[K] K (u : 𝒪[K]) := rfl
31 
32 theorem unitEmbedding_injective : Function.Injective (unitEmbedding K) :=
33   Units.map_injective Subtype.val_injective
34 
35 theorem mem_compactUnitSubgroup_iff (u : Kˣ) :
36     u ∈ compactUnitSubgroup K ↔ valuation K (u : K) = 1 := by
37   constructor
38   · rintro ⟨v, rfl⟩
39     exact (Valuation.integer.integers (valuation K)).valuation_unit v
40   · intro hu
41     let x : 𝒪[K] := ⟨u, hu.le⟩
42     have hx : IsUnit x :=
43       (Valuation.integer.integers (valuation K)).isUnit_iff_valuation_eq_one.mpr hu
44     refine ⟨hx.unit, ?_⟩
45     apply Units.ext
46     change algebraMap 𝒪[K] K (hx.unit : 𝒪[K]) = (u : K)
47     rw [hx.unit_spec]
48     rfl
49 
50 theorem compactUnitSubgroup_eq_units :
51     compactUnitSubgroup K = (𝒪[K]).toSubmonoid.units := by
52   ext u
53   rw [mem_compactUnitSubgroup_iff]
54   change valuation K (u : K) = 1 ↔
55     valuation K (u : K) ≤ 1 ∧ valuation K ((u⁻¹ : Kˣ) : K) ≤ 1
56   rw [Units.val_inv_eq_inv_val, map_inv₀,
57     inv_le_one₀ (by simp [zero_lt_iff])]
58   exact le_antisymm_iff
59 
60 variable [TopologicalSpace K]
61 
62 theorem continuous_unitEmbedding : Continuous (unitEmbedding K) :=
63   (continuous_subtype_val : Continuous (algebraMap 𝒪[K] K)).units_map _
64 
65 variable [IsNonarchimedeanLocalField K]
66 
67 instance localFieldT2Space : T2Space K := by
68   let := IsTopologicalAddGroup.rightUniformSpace K
69   have := isUniformAddGroup_of_addCommGroup (G := K)
70   infer_instance
71 
72 /-- Compactness is inherited from the compact valuation ring via its unit group. -/
73 theorem isCompact_compactUnitSubgroup : IsCompact (compactUnitSubgroup K : Set Kˣ) := by
74   rw [compactUnitSubgroup_eq_units]
75   exact Submonoid.units_isCompact (IsNonarchimedeanLocalField.isCompact_closedBall K 1)
76 
77 /-- The actual integral-unit subgroup is open in the field unit group. -/
78 theorem isOpen_compactUnitSubgroup : IsOpen (compactUnitSubgroup K : Set Kˣ) := by
79   rw [compactUnitSubgroup_eq_units]
80   apply Submonoid.isOpen_units
81   exact (valuation K).isOpen_integer
82 
83 /-- Integral units and their image subgroup agree as topological groups. -/
84 def unitEmbeddingEquiv : 𝒪[K]ˣ ≃ₜ* compactUnitSubgroup K where
85   __ := MonoidHom.ofInjective (unitEmbedding_injective K)
86   continuous_toFun := (continuous_unitEmbedding K).subtype_mk _
87   continuous_invFun :=
88     Continuous.continuous_symm_of_equiv_compact_to_t2
89       (f := (MonoidHom.ofInjective (unitEmbedding_injective K)).toEquiv)
90       ((continuous_unitEmbedding K).subtype_mk _)
91 
92 @[simp] theorem coe_unitEmbeddingEquiv (u : 𝒪[K]ˣ) :
93     ((unitEmbeddingEquiv K u : compactUnitSubgroup K) : Kˣ) = unitEmbedding K u := rfl
94 
95 /-- An open set of integral units remains open in the field unit group. -/
96 theorem unitEmbedding_isOpenMap : IsOpenMap (unitEmbedding K) :=
97   (isOpen_compactUnitSubgroup K).isOpenMap_subtype_val.comp
98     (unitEmbeddingEquiv K).toHomeomorph.isOpenMap
99 
100 end
101 
102 end PaperXI.ActualLocalUnitTopology

Back to source controls