English
Let G be a nonarchimedean additive group. Then its completion is again a nonarchimedean additive group.
Русский
Пусть G — неархимедова аддитивная группа. Тогда её завершение снова является неархимедовой аддитивной группой.
LaTeX
$$$\operatorname{NonarchimedeanAddGroup}(G) \Rightarrow \operatorname{NonarchimedeanAddGroup}(\mathrm{Completion}(G))$$$
Lean4
/-- The completion of a nonarchimedean additive group is a nonarchimedean additive group. -/
instance {G : Type*} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] [NonarchimedeanAddGroup G] :
NonarchimedeanAddGroup (Completion G) where
is_nonarchimedean := by
/- Let `U` be a neighborhood of `0` in `Completion G`. We wish to show that `U` contains an open
additive subgroup of `Completion G`. -/
intro U hU
obtain ⟨C, ⟨hC, C_closed⟩, C_subset_U⟩ := (closed_nhds_basis 0).mem_iff.mp hU
have : toCompl ⁻¹' C ∈ 𝓝 0 :=
continuous_toCompl.continuousAt.preimage_mem_nhds
(by rwa [map_zero])
/- Therefore, since `G` is nonarchimedean, there exists an open subgroup `W` of `G` that is
contained within `toCompl ⁻¹' C`. -/
obtain ⟨W, hCW⟩ := NonarchimedeanAddGroup.is_nonarchimedean (toCompl ⁻¹' C) this
let V : Set (Completion G) := (W.map toCompl).topologicalClosure
have : IsOpen V := by
/- Since `V` is a subgroup of `Completion G`, it suffices to show that it is a neighborhood of
`0` in `Completion G`. This follows from the fact that `toCompl : G → Completion G` is dense
inducing and `W` is a neighborhood of `0` in `G`. -/
apply isOpen_of_mem_nhds (g := 0)
apply (isDenseInducing_toCompl _).closure_image_mem_nhds
exact mem_nhds_zero W
use
⟨_, this⟩
/- Finally, it remains to show that `V ⊆ U`. It suffices to show that `V ⊆ C`, which
follows from the fact that `W ⊆ toCompl ⁻¹' C` and `C` is closed. -/
suffices V ⊆ C from this.trans C_subset_U
exact closure_minimal (Set.image_subset_iff.mpr hCW) C_closed
