From 19ecff8b533cf85a63f10d7ca1c90d67f6289336 Mon Sep 17 00:00:00 2001 From: ashwiniyengar Date: Sun, 14 Mar 2021 00:42:52 +0000 Subject: [PATCH] feat(topology/algebra/nonarchimedean): added nonarchimedean groups and rings (#6551) Adding nonarchimedean topological groups and rings. --- .../algebra/nonarchimedean/basic.lean | 136 ++++++++++++++++++ src/topology/algebra/open_subgroup.lean | 25 ++++ src/topology/algebra/ring.lean | 30 ++-- 3 files changed, 183 insertions(+), 8 deletions(-) create mode 100644 src/topology/algebra/nonarchimedean/basic.lean diff --git a/src/topology/algebra/nonarchimedean/basic.lean b/src/topology/algebra/nonarchimedean/basic.lean new file mode 100644 index 0000000000000..af8df909f0e85 --- /dev/null +++ b/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 diff --git a/src/topology/algebra/open_subgroup.lean b/src/topology/algebra/open_subgroup.lean index ef5a7bd7b4319..153dcb5dc50aa 100644 --- a/src/topology/algebra/open_subgroup.lean +++ b/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 diff --git a/src/topology/algebra/ring.lean b/src/topology/algebra/ring.lean index d7dc880c85d58..22acff075b588 100644 --- a/src/topology/algebra/ring.lean +++ b/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) :=