feat(topology/algebra/nonarchimedean): added nonarchimedean groups and rings (#6551)

Adding nonarchimedean topological groups and rings.

Author: ashwiniyengar

src/topology/algebra/nonarchimedean/basic.lean

@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2021 Ashwin Iyengar. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Kevin Buzzard, Johan Commelin, Ashwin Iyengar, Patrick Massot.
+-/
+import topology.algebra.ring
+import topology.algebra.open_subgroup
+import data.set.basic
+import group_theory.subgroup
+
+/-!
+# Nonarchimedean Topology
+
+In this file we set up the theory of nonarchimedean topological groups and rings.
+
+A nonarchimedean group is a topological group whose topology admits a basis of
+open neighborhoods of the identity element in the group consisting of open subgroups.
+A nonarchimedean ring is a topological ring whose underlying topological (additive)
+group is nonarchimedean.
+
+## Definitions
+
+- `nonarchimedean_add_group`: nonarchimedean additive group.
+- `nonarchimedean_group`: nonarchimedean multiplicative group.
+- `nonarchimedean_ring`: nonarchimedean ring.
+
+-/
+
+/-- An topological additive group is nonarchimedean if every neighborhood of 0
+  contains an open subgroup. -/
+class nonarchimedean_add_group (G : Type*)
+  [add_group G] [topological_space G] extends topological_add_group G : Prop :=
+(is_nonarchimedean : ∀ U ∈ nhds (0 : G), ∃ V : open_add_subgroup G, (V : set G) ⊆ U)
+
+/-- A topological group is nonarchimedean if every neighborhood of 1 contains an open subgroup. -/
+@[to_additive]
+class nonarchimedean_group (G : Type*)
+  [group G] [topological_space G] extends topological_group G : Prop :=
+(is_nonarchimedean : ∀ U ∈ nhds (1 : G), ∃ V : open_subgroup G, (V : set G) ⊆ U)
+
+/-- An topological ring is nonarchimedean if its underlying topological additive
+  group is nonarchimedean. -/
+class nonarchimedean_ring (R : Type*)
+  [ring R] [topological_space R] extends topological_ring R : Prop :=
+(is_nonarchimedean : ∀ U ∈ nhds (0 : R), ∃ V : open_add_subgroup R, (V : set R) ⊆ U)
+
+/-- Every nonarchimedean ring is naturally a nonarchimedean additive group. -/
+@[priority 100] -- see Note [lower instance priority]
+instance nonarchimedean_ring.to_nonarchimedean_add_group
+  (R : Type*) [ring R] [topological_space R] [t: nonarchimedean_ring R] :
+nonarchimedean_add_group R := {..t}
+
+namespace nonarchimedean_group
+
+variables {G : Type*} [group G] [topological_space G] [nonarchimedean_group G]
+variables {H : Type*} [group H] [topological_space H] [topological_group H]
+variables {K : Type*} [group K] [topological_space K] [nonarchimedean_group K]
+
+/-- If a topological group embeds into a nonarchimedean group, then it
+  is nonarchimedean. -/
+@[to_additive nonarchimedean_add_group.nonarchimedean_of_emb]
+lemma nonarchimedean_of_emb (f : G →* H) (emb : open_embedding f) : nonarchimedean_group H :=
+{ is_nonarchimedean := λ U hU, have h₁ : (f ⁻¹' U) ∈ nhds (1 : G), from
+    by {apply emb.continuous.tendsto, rwa is_group_hom.map_one f},
+  let ⟨V, hV⟩ := is_nonarchimedean (f ⁻¹' U) h₁ in
+    ⟨{is_open' := emb.is_open_map _ V.is_open, ..subgroup.map f V},
+      set.image_subset_iff.2 hV⟩ }
+
+/-- An open neighborhood of the identity in the cartesian product of two nonarchimedean groups
+  contains the cartesian product of an open neighborhood in each group. -/
+@[to_additive nonarchimedean_add_group.prod_subset]
+lemma prod_subset {U} (hU : U ∈ nhds (1 : G × K)) :
+  ∃ (V : open_subgroup G) (W : open_subgroup K), (V : set G).prod (W : set K) ⊆ U :=
+begin
+  erw [nhds_prod_eq, filter.mem_prod_iff] at hU,
+  rcases hU with ⟨U₁, hU₁, U₂, hU₂, h⟩,
+  cases is_nonarchimedean _ hU₁ with V hV,
+  cases is_nonarchimedean _ hU₂ with W hW,
+  use V, use W,
+  rw set.prod_subset_iff,
+  intros x hX y hY,
+  exact set.subset.trans (set.prod_mono hV hW) h (set.mem_sep hX hY),
+end
+
+/-- An open neighborhood of the identity in the cartesian square of a nonarchimedean group
+  contains the cartesian square of an open neighborhood in the group. -/
+@[to_additive nonarchimedean_add_group.prod_self_subset]
+lemma prod_self_subset {U} (hU : U ∈ nhds (1 : G × G)) :
+  ∃ (V : open_subgroup G), (V : set G).prod (V : set G) ⊆ U :=
+let ⟨V, W, h⟩ := prod_subset hU in
+  ⟨V ⊓ W, by {refine set.subset.trans (set.prod_mono _ _) ‹_›; simp}⟩
+
+/-- The cartesian product of two nonarchimedean groups is nonarchimedean. -/
+@[to_additive]
+instance : nonarchimedean_group (G × K) :=
+{ is_nonarchimedean := λ U hU, let ⟨V, W, h⟩ := prod_subset hU in ⟨V.prod W, ‹_›⟩ }
+
+end nonarchimedean_group
+
+namespace nonarchimedean_ring
+
+open nonarchimedean_ring
+open nonarchimedean_add_group
+
+variables {R S : Type*}
+variables [ring R] [topological_space R] [nonarchimedean_ring R]
+variables [ring S] [topological_space S] [nonarchimedean_ring S]
+
+/-- The cartesian product of two nonarchimedean rings is nonarchimedean. -/
+instance : nonarchimedean_ring (R × S) :=
+{ is_nonarchimedean := nonarchimedean_add_group.is_nonarchimedean }
+
+/-- Given an open subgroup `U` and an element `r` of a nonarchimedean ring, there is an open
+  subgroup `V` such that `r • V` is contained in `U`. -/
+lemma left_mul_subset (U : open_add_subgroup R) (r : R) :
+  ∃ V : open_add_subgroup R, r • (V : set R) ⊆ U :=
+⟨U.comap (add_monoid_hom.mul_left r) (continuous_mul_left r),
+  (U : set R).image_preimage_subset _⟩
+
+/-- An open subgroup of a nonarchimedean ring contains the square of another one. -/
+lemma mul_subset (U : open_add_subgroup R) :
+  ∃ V : open_add_subgroup R, (V : set R) * V ⊆ U :=
+let ⟨V, H⟩ := prod_self_subset (mem_nhds_sets (is_open.preimage continuous_mul U.is_open)
+  begin
+    simpa only [set.mem_preimage, open_add_subgroup.mem_coe, prod.snd_zero, mul_zero]
+      using U.zero_mem,
+  end) in
+begin
+  use V,
+  rintros v ⟨a, b, ha, hb, hv⟩,
+  have hy := H (set.mk_mem_prod ha hb),
+  simp only [set.mem_preimage, open_add_subgroup.mem_coe] at hy,
+  rwa hv at hy
+end
+
+end nonarchimedean_ring

src/topology/algebra/open_subgroup.lean

@@ -141,6 +141,31 @@ instance : semilattice_inf_top (open_subgroup G) :=
 attribute [norm_cast] coe_inf coe_subset coe_subgroup_le open_add_subgroup.coe_inf
   open_add_subgroup.coe_subset open_add_subgroup.coe_add_subgroup_le
 
+variables {N : Type*} [group N] [topological_space N]
+
+/-- The preimage of an `open_subgroup` along a continuous `monoid` homomorphism
+  is an `open_subgroup`. -/
+@[to_additive "The preimage of an `open_add_subgroup` along a continuous `add_monoid` homomorphism
+is an `open_add_subgroup`."]
+def comap (f : G →* N)
+  (hf : continuous f) (H : open_subgroup N) : open_subgroup G :=
+{ is_open' := H.is_open.preimage hf,
+  .. (H : subgroup N).comap f }
+
+@[simp, to_additive]
+lemma coe_comap (H : open_subgroup N) (f : G →* N) (hf : continuous f) :
+  (H.comap f hf : set G) = f ⁻¹' H := rfl
+
+@[simp, to_additive]
+lemma mem_comap {H : open_subgroup N} {f : G →* N} {hf : continuous f} {x : G} :
+  x ∈ H.comap f hf ↔ f x ∈ H := iff.rfl
+
+@[to_additive]
+lemma comap_comap {P : Type*} [group P] [topological_space P]
+  (K : open_subgroup P) (f₂ : N →* P) (hf₂ : continuous f₂) (f₁ : G →* N) (hf₁ : continuous f₁) :
+  (K.comap f₂ hf₂).comap f₁ hf₁ = K.comap (f₂.comp f₁) (hf₂.comp hf₁) :=
+rfl
+
 end open_subgroup
 
 namespace subgroup

src/topology/algebra/ring.lean

@@ -7,32 +7,46 @@ Theory of topological rings.
 -/
 import topology.algebra.group
 import ring_theory.ideal.basic
+import algebra.ring.prod
 
 open classical set filter topological_space
 open_locale classical
 
 section topological_ring
-universes u v w
-variables (α : Type u) [topological_space α]
+variables (α : Type*)
 
 /-- A topological semiring is a semiring where addition and multiplication are continuous. -/
-class topological_semiring [semiring α]
+class topological_semiring [topological_space α] [semiring α]
   extends has_continuous_add α, has_continuous_mul α : Prop
 
-variables [ring α]
-
 /-- A topological ring is a ring where the ring operations are continuous. -/
-class topological_ring extends has_continuous_add α, has_continuous_mul α : Prop :=
+class topological_ring [topological_space α] [ring α]
+  extends has_continuous_add α, has_continuous_mul α : Prop :=
 (continuous_neg : continuous (λa:α, -a))
 
-variables [t : topological_ring α]
+variables {α}
+
+/-- The product topology on the cartesian product of two topological semirings
+  makes the product into a topological semiring. -/
+instance prod_semiring {β : Type*}
+  [semiring α] [topological_space α] [topological_semiring α]
+  [semiring β] [topological_space β] [topological_semiring β] : topological_semiring (α × β) :=
+{}
+
+variables [ring α] [topological_space α] [t : topological_ring α]
 @[priority 100] -- see Note [lower instance priority]
 instance topological_ring.to_topological_semiring : topological_semiring α := {..t}
 
 @[priority 100] -- see Note [lower instance priority]
 instance topological_ring.to_topological_add_group : topological_add_group α := {..t}
 
-variables {α} [topological_ring α]
+variables [topological_ring α]
+
+/-- The product topology on the cartesian product of two topological rings
+  makes the product into a topological ring. -/
+instance prod_ring {β : Type*}
+  [ring β] [topological_space β] [topological_ring β] : topological_ring (α × β) :=
+{ continuous_neg := continuous_neg }
 
 /-- In a topological ring, the left-multiplication `add_monoid_hom` is continuous. -/
 lemma mul_left_continuous (x : α) : continuous (add_monoid_hom.mul_left x) :=