feat(topology/algebra): more on closure (#6675)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/group_theory/subgroup.lean

@@ -228,6 +228,10 @@ by simpa only [div_eq_mul_inv] using H.mul_mem' hx (H.inv_mem' hy)
 @[simp, to_additive] theorem inv_mem_iff {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
 ⟨λ h, inv_inv x ▸ H.inv_mem h, H.inv_mem⟩
 
+@[simp, to_additive]
+theorem inv_coe_set : (H : set G)⁻¹ = H :=
+by { ext, simp, }
+
 @[to_additive]
 lemma mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H :=
 ⟨λ hba, by simpa using H.mul_mem hba (H.inv_mem h), λ hb, H.mul_mem hb h⟩

src/topology/algebra/algebra.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import algebra.algebra.subalgebra
+import topology.algebra.module
+
+/-!
+# Topological (sub)algebras
+
+A topological algebra over a topological ring `R` is a
+topological ring with a compatible continuous scalar multiplication by elements of `R`.
+
+## Results
+
+This is just a minimal stub for now!
+
+The topological closure of a subalgebra is still a subalgebra,
+which as an algebra is a topological algebra.
+-/
+
+open classical set topological_space algebra
+open_locale classical
+
+universes u v w
+
+section topological_algebra
+variables (R : Type*) [topological_space R] [comm_ring R] [topological_ring R]
+variables (A : Type u) [topological_space A]
+variables [ring A]
+
+/-- A topological algebra over a topological ring `R` is a
+topological ring with a compatible continuous scalar multiplication by elements of `R`. -/
+class topological_algebra [algebra R A] [topological_ring A] : Prop :=
+(continuous_algebra_map : continuous (algebra_map R A))
+
+attribute [continuity] topological_algebra.continuous_algebra_map
+
+end topological_algebra
+
+section topological_algebra
+variables {R : Type*} [comm_ring R]
+variables {A : Type u} [topological_space A]
+variables [ring A]
+variables [algebra R A] [topological_ring A]
+
+@[priority 200] -- see Note [lower instance priority]
+instance topological_algebra.to_topological_module
+  [topological_space R] [topological_ring R] [topological_algebra R A] :
+  topological_semimodule R A :=
+{ continuous_smul := begin
+    simp_rw algebra.smul_def,
+    continuity,
+  end, }
+
+/-- The closure of a subalgebra in a topological algebra as a subalgebra. -/
+def subalgebra.topological_closure (s : subalgebra R A) : subalgebra R A :=
+{ carrier := closure (s : set A),
+  algebra_map_mem' := λ r, s.to_subring.subring_topological_closure (s.algebra_map_mem r),
+  ..s.to_subring.topological_closure }
+
+instance subalgebra.topological_closure_topological_ring (s : subalgebra R A) :
+  topological_ring (s.topological_closure) :=
+s.to_subring.topological_closure_topological_ring
+
+instance subalgebra.topological_closure_topological_algebra
+  [topological_space R] [topological_ring R] [topological_algebra R A] (s : subalgebra R A) :
+  topological_algebra R (s.topological_closure) :=
+{ continuous_algebra_map :=
+  begin
+    change continuous (λ r, _),
+    continuity,
+  end }
+
+lemma subalgebra.subring_topological_closure (s : subalgebra R A) :
+  s ≤ s.topological_closure :=
+subset_closure
+
+lemma subalgebra.is_closed_topological_closure (s : subalgebra R A) :
+  is_closed (s.topological_closure : set A) :=
+by convert is_closed_closure
+
+lemma subalgebra.topological_closure_minimal
+  (s : subalgebra R A) {t : subalgebra R A} (h : s ≤ t) (ht : is_closed (t : set A)) :
+  s.topological_closure ≤ t :=
+closure_minimal h ht
+
+end topological_algebra

src/topology/algebra/group.lean

@@ -216,6 +216,39 @@ variable {G}
 lemma inv_closure (s : set G) : (closure s)⁻¹ = closure s⁻¹ :=
 (homeomorph.inv G).preimage_closure s
 
+/-- The (topological-space) closure of a subgroup of a space `M` with `has_continuous_mul` is
+itself a subgroup. -/
+@[to_additive "The (topological-space) closure of an additive subgroup of a space `M` with
+`has_continuous_add` is itself an additive subgroup."]
+def subgroup.topological_closure (s : subgroup G) : subgroup G :=
+{ carrier := closure (s : set G),
+  inv_mem' := λ g m, by simpa [←mem_inv, inv_closure] using m,
+  ..s.to_submonoid.topological_closure }
+
+@[to_additive]
+instance subgroup.topological_closure_topological_group (s : subgroup G) :
+  topological_group (s.topological_closure) :=
+{ continuous_inv :=
+  begin
+    apply continuous_induced_rng,
+    change continuous (λ p : s.topological_closure, (p : G)⁻¹),
+    continuity,
+  end
+  ..s.to_submonoid.topological_closure_has_continuous_mul}
+
+lemma subgroup.subgroup_topological_closure (s : subgroup G) :
+  s ≤ s.topological_closure :=
+subset_closure
+
+lemma subgroup.is_closed_topological_closure (s : subgroup G) :
+  is_closed (s.topological_closure : set G) :=
+by convert is_closed_closure
+
+lemma subgroup.topological_closure_minimal
+  (s : subgroup G) {t : subgroup G} (h : s ≤ t) (ht : is_closed (t : set G)) :
+  s.topological_closure ≤ t :=
+closure_minimal h ht
+
 @[to_additive exists_nhds_half_neg]
 lemma exists_nhds_split_inv {s : set G} (hs : s ∈ 𝓝 (1 : G)) :
   ∃ V ∈ 𝓝 (1 : G), ∀ (v ∈ V) (w ∈ V), v / w ∈ s :=
@@ -240,18 +273,6 @@ lemma topological_group.ext {G : Type*} [group G] {t t' : topological_space G}
 eq_of_nhds_eq_nhds $ λ x, by
   rw [← @nhds_translation_mul_inv G t _ _ x , ← @nhds_translation_mul_inv G t' _ _ x , ← h]
 
-/-- The topological closure of a subgroup as a subgroup. -/
-@[to_additive "The topological closure of an additive subgroup as an additive subgroup."]
-def subgroup.topological_closure (H : subgroup G) : subgroup G :=
-{ carrier := closure H,
-  one_mem' := subset_closure H.one_mem,
-  mul_mem' := λ a b ha hb, H.to_submonoid.top_closure_mul_self_subset ⟨a, b, ha, hb, rfl⟩,
-  inv_mem' := begin
-    change closure (H : set G) ⊆ (λ x : G, x⁻¹) ⁻¹' (closure H),
-    conv_rhs { rw show (H : set G) = (λ x : G, x⁻¹) '' H, by ext ; simp },
-    exact closure_subset_preimage_closure_image (continuous_inv : continuous (λ x : G, _)),
-  end }
-
 @[to_additive]
 lemma topological_group.of_nhds_aux {G : Type*} [group G] [topological_space G]
   (hinv : tendsto (λ (x : G), x⁻¹) (𝓝 1) (𝓝 1))

src/topology/algebra/module.lean

@@ -170,13 +170,22 @@ set.subset.antisymm s.closure_smul_self_subset
 
 variables [has_continuous_add M]
 
-/-- The (topological-space) closure of a submodle of a topological `R`-semimodule `M` is itself
+/-- The (topological-space) closure of a submodule of a topological `R`-semimodule `M` is itself
 a submodule. -/
 def submodule.topological_closure (s : submodule R M) : submodule R M :=
 { carrier := closure (s : set M),
-  zero_mem' := subset_closure s.zero_mem,
-  add_mem' := λ a b ha hb, s.to_add_submonoid.top_closure_add_self_subset ⟨a, b, ha, hb, rfl⟩,
-  smul_mem' := λ c x hx, s.closure_smul_self_subset ⟨⟨c, x⟩, ⟨set.mem_univ _, hx⟩, rfl⟩ }
+  smul_mem' := λ c x hx, s.closure_smul_self_subset ⟨⟨c, x⟩, ⟨set.mem_univ _, hx⟩, rfl⟩,
+  ..s.to_add_submonoid.topological_closure }
+
+instance submodule.topological_closure_topological_semimodule (s : submodule R M) :
+  topological_semimodule R (s.topological_closure) :=
+{ continuous_smul :=
+  begin
+    apply continuous_induced_rng,
+    change continuous (λ p : R × s.topological_closure, p.1 • (p.2 : M)),
+    continuity,
+  end,
+  ..s.to_add_submonoid.topological_closure_has_continuous_add }
 
 lemma submodule.submodule_topological_closure (s : submodule R M) :
   s ≤ s.topological_closure :=

src/topology/algebra/monoid.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import topology.continuous_on
-import group_theory.submonoid.basic
+import group_theory.submonoid.operations
 import algebra.group.prod
 import algebra.pointwise
 
@@ -175,6 +175,16 @@ def submonoid.topological_closure (s : submonoid M) : submonoid M :=
   one_mem' := subset_closure s.one_mem,
   mul_mem' := λ a b ha hb, s.top_closure_mul_self_subset ⟨a, b, ha, hb, rfl⟩ }
 
+@[to_additive]
+instance submonoid.topological_closure_has_continuous_mul (s : submonoid M) :
+  has_continuous_mul (s.topological_closure) :=
+{ continuous_mul :=
+  begin
+    apply continuous_induced_rng,
+    change continuous (λ p : s.topological_closure × s.topological_closure, (p.1 : M) * (p.2 : M)),
+    continuity,
+  end }
+
 lemma submonoid.submonoid_topological_closure (s : submonoid M) :
   s ≤ s.topological_closure :=
 subset_closure

src/topology/algebra/ring.lean

@@ -7,6 +7,7 @@ Theory of topological rings.
 -/
 import topology.algebra.group
 import ring_theory.ideal.basic
+import ring_theory.subring
 import algebra.ring.prod
 
 open classical set filter topological_space
@@ -19,26 +20,65 @@ variables (α : Type*)
 class topological_semiring [topological_space α] [semiring α]
   extends has_continuous_add α, has_continuous_mul α : Prop
 
-/-- A topological ring is a ring where the ring operations are continuous. -/
-class topological_ring [topological_space α] [ring α]
-  extends has_continuous_add α, has_continuous_mul α : Prop :=
-(continuous_neg : continuous (λa:α, -a))
+section
+variables {α} [topological_space α] [semiring α] [topological_semiring α]
+
+/-- The (topological-space) closure of a subsemiring of a topological semiring is
+itself a subsemiring. -/
+def subsemiring.topological_closure (s : subsemiring α) : subsemiring α :=
+{ carrier := closure (s : set α),
+  ..(s.to_submonoid.topological_closure),
+  ..(s.to_add_submonoid.topological_closure ) }
+
+instance subsemiring.topological_closure_topological_semiring (s : subsemiring α) :
+  topological_semiring (s.topological_closure) :=
+{ ..s.to_add_submonoid.topological_closure_has_continuous_add,
+  ..s.to_submonoid.topological_closure_has_continuous_mul }
 
-variables {α}
+lemma subsemiring.subring_topological_closure (s : subsemiring α) :
+  s ≤ s.topological_closure :=
+subset_closure
+
+lemma subsemiring.is_closed_topological_closure (s : subsemiring α) :
+  is_closed (s.topological_closure : set α) :=
+by convert is_closed_closure
+
+lemma subsemiring.topological_closure_minimal
+  (s : subsemiring α) {t : subsemiring α} (h : s ≤ t) (ht : is_closed (t : set α)) :
+  s.topological_closure ≤ t :=
+closure_minimal h ht
+
+instance (S : submonoid α) : has_continuous_mul (S.topological_closure) :=
+{ continuous_mul :=
+  begin
+    apply continuous_induced_rng,
+    change continuous (λ p : S.topological_closure × S.topological_closure, (p.1 : α) * (p.2 : α)),
+    continuity,
+  end }
 
 /-- 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 α]
+end
+
+/-- A topological ring is a ring where the ring operations are continuous. -/
+class topological_ring [topological_space α] [ring α]
+  extends has_continuous_add α, has_continuous_mul α : Prop :=
+(continuous_neg : continuous (λa:α, -a))
+
+variables {α} [ring α] [topological_space α]
+
+section
+variables [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}
+end
 
 variables [topological_ring α]
 
@@ -56,6 +96,31 @@ continuous_const.mul continuous_id
 lemma mul_right_continuous (x : α) : continuous (add_monoid_hom.mul_right x) :=
 continuous_id.mul continuous_const
 
+/-- The (topological-space) closure of a subring of a topological semiring is
+itself a subring. -/
+def subring.topological_closure (S : subring α) : subring α :=
+{ carrier := closure (S : set α),
+  ..(S.to_submonoid.topological_closure),
+  ..(S.to_add_subgroup.topological_closure) }
+
+instance subring.topological_closure_topological_ring (s : subring α) :
+  topological_ring (s.topological_closure) :=
+{ ..s.to_add_subgroup.topological_closure_topological_add_group,
+  ..s.to_submonoid.topological_closure_has_continuous_mul }
+
+lemma subring.subring_topological_closure (s : subring α) :
+  s ≤ s.topological_closure :=
+subset_closure
+
+lemma subring.is_closed_topological_closure (s : subring α) :
+  is_closed (s.topological_closure : set α) :=
+by convert is_closed_closure
+
+lemma subring.topological_closure_minimal
+  (s : subring α) {t : subring α} (h : s ≤ t) (ht : is_closed (t : set α)) :
+  s.topological_closure ≤ t :=
+closure_minimal h ht
+
 end topological_ring
 
 section topological_comm_ring
@@ -64,12 +129,10 @@ variables {α : Type*} [topological_space α] [comm_ring α] [topological_ring 
 /-- The closure of an ideal in a topological ring as an ideal. -/
 def ideal.closure (S : ideal α) : ideal α :=
 { carrier := closure S,
-  zero_mem' := subset_closure S.zero_mem,
-  add_mem'  := assume x y hx hy,
-    map_mem_closure2 continuous_add hx hy $ assume a b, S.add_mem,
-  smul_mem'  := assume c x hx,
+  smul_mem' := assume c x hx,
     have continuous (λx:α, c * x) := continuous_const.mul continuous_id,
-    map_mem_closure this hx $ assume a, S.mul_mem_left _ }
+    map_mem_closure this hx $ assume a, S.mul_mem_left _,
+  ..(add_submonoid.topological_closure S.to_add_submonoid) }
 
 @[simp] lemma ideal.coe_closure (S : ideal α) :
   (S.closure : set α) = closure S := rfl