feat(analysis/normed_space/inner_product): double orthogonal compleme…

…nt is closure (#5876)

Put a submodule structure on the closure (as a set in a topological space) of a submodule of a topological module.  Show that in a complete inner product space, the double orthogonal complement of a submodule is its closure.

src/algebra/pointwise.lean

@@ -437,4 +437,13 @@ lemma mul_subset_closure {s t u : set M} (hs : s ⊆ u) (ht : t ⊆ u) :
   s * t ⊆ submonoid.closure u :=
 mul_subset (subset.trans hs submonoid.subset_closure) (subset.trans ht submonoid.subset_closure)
 
+@[to_additive]
+lemma coe_mul_self_eq (s : submonoid M) : (s : set M) * s = s :=
+begin
+  ext x,
+  refine ⟨_, λ h, ⟨x, 1, h, s.one_mem, mul_one x⟩⟩,
+  rintros ⟨a, b, ha, hb, rfl⟩,
+  exact s.mul_mem ha hb
+end
+
 end submonoid

src/analysis/normed_space/inner_product.lean

@@ -2004,6 +2004,12 @@ subspaces. -/
 lemma submodule.orthogonal_le {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂) : K₂ᗮ ≤ K₁ᗮ :=
 (submodule.orthogonal_gc 𝕜 E).monotone_l h
 
+/-- `submodule.orthogonal.orthogonal` preserves the `≤` ordering of two
+subspaces. -/
+lemma submodule.orthogonal_orthogonal_monotone {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂) :
+  K₁ᗮᗮ ≤ K₂ᗮᗮ :=
+submodule.orthogonal_le (submodule.orthogonal_le h)
+
 /-- `K` is contained in `Kᗮᗮ`. -/
 lemma submodule.le_orthogonal_orthogonal : K ≤ Kᗮᗮ := (submodule.orthogonal_gc 𝕜 E).le_u_l _
 
@@ -2076,6 +2082,17 @@ begin
     exact hw v hv }
 end
 
+lemma submodule.orthogonal_orthogonal_eq_closure [complete_space E] :
+  Kᗮᗮ = K.topological_closure :=
+begin
+  refine le_antisymm _ _,
+  { convert submodule.orthogonal_orthogonal_monotone K.submodule_topological_closure,
+    haveI : complete_space K.topological_closure :=
+      K.is_closed_topological_closure.complete_space_coe,
+    rw K.topological_closure.orthogonal_orthogonal },
+  { exact K.topological_closure_minimal K.le_orthogonal_orthogonal Kᗮ.is_closed_orthogonal }
+end
+
 variables {K}
 
 /-- If `K` is complete, `K` and `Kᗮ` are complements of each other. -/

src/topology/algebra/module.lean

@@ -135,6 +135,59 @@ end
 
 end
 
+section closure
+variables {R : Type u} {M : Type v}
+[semiring R] [topological_space R]
+[topological_space M] [add_comm_monoid M]
+[semimodule R M] [topological_semimodule R M]
+
+lemma submodule.closure_smul_self_subset (s : submodule R M) :
+  (λ p : R × M, p.1 • p.2) '' ((set.univ : set R).prod (closure (s : set M)))
+  ⊆ closure (s : set M) :=
+calc
+(λ p : R × M, p.1 • p.2) '' ((set.univ : set R).prod (closure (s : set M)))
+    = (λ p : R × M, p.1 • p.2) '' (closure ((set.univ : set R).prod s)) : by simp [closure_prod_eq]
+... ⊆ closure ((λ p : R × M, p.1 • p.2) '' ((set.univ : set R).prod s)) :
+  image_closure_subset_closure_image continuous_smul
+... = closure s : begin
+  congr,
+  ext x,
+  refine ⟨_, λ hx, ⟨⟨1, x⟩, ⟨set.mem_univ _, hx⟩, one_smul R _⟩⟩,
+  rintros ⟨⟨c, y⟩, ⟨hc, hy⟩, rfl⟩,
+  simp [s.smul_mem c hy]
+end
+
+lemma submodule.closure_smul_self_eq (s : submodule R M) :
+  (λ p : R × M, p.1 • p.2) '' ((set.univ : set R).prod (closure (s : set M)))
+  = closure (s : set M) :=
+set.subset.antisymm s.closure_smul_self_subset
+  (λ x hx, ⟨⟨1, x⟩, ⟨set.mem_univ _, hx⟩, one_smul R _⟩)
+
+variables [has_continuous_add M]
+
+/-- The (topological-space) closure of a submodle 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⟩ }
+
+lemma submodule.submodule_topological_closure (s : submodule R M) :
+  s ≤ s.topological_closure :=
+subset_closure
+
+lemma submodule.is_closed_topological_closure (s : submodule R M) :
+  is_closed (s.topological_closure : set M) :=
+by convert is_closed_closure
+
+lemma submodule.topological_closure_minimal
+  (s : submodule R M) {t : submodule R M} (h : s ≤ t) (ht : is_closed (t : set M)) :
+  s.topological_closure ≤ t :=
+closure_minimal h ht
+
+end closure
+
 section
 
 variables {R : Type*} {M : Type*} {a : R}

src/topology/algebra/monoid.lean

@@ -149,6 +149,45 @@ section has_continuous_mul
 
 variables [topological_space M] [monoid M] [has_continuous_mul M]
 
+@[to_additive]
+lemma submonoid.top_closure_mul_self_subset (s : submonoid M) :
+  (closure (s : set M)) * closure (s : set M) ⊆ closure (s : set M) :=
+calc
+(closure (s : set M)) * closure (s : set M)
+    = (λ p : M × M, p.1 * p.2) '' (closure ((s : set M).prod s)) : by simp [closure_prod_eq]
+... ⊆ closure ((λ p : M × M, p.1 * p.2) '' ((s : set M).prod s)) :
+  image_closure_subset_closure_image continuous_mul
+... = closure s : by simp [s.coe_mul_self_eq]
+
+@[to_additive]
+lemma submonoid.top_closure_mul_self_eq (s : submonoid M) :
+  (closure (s : set M)) * closure (s : set M) = closure (s : set M) :=
+subset.antisymm
+  s.top_closure_mul_self_subset
+  (λ x hx, ⟨x, 1, hx, subset_closure s.one_mem, mul_one _⟩)
+
+/-- The (topological-space) closure of a submonoid of a space `M` with `has_continuous_mul` is
+itself a submonoid. -/
+@[to_additive "The (topological-space) closure of an additive submonoid of a space `M` with
+`has_continuous_add` is itself an additive submonoid."]
+def submonoid.topological_closure (s : submonoid M) : submonoid M :=
+{ carrier := closure (s : set 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⟩ }
+
+lemma submonoid.submonoid_topological_closure (s : submonoid M) :
+  s ≤ s.topological_closure :=
+subset_closure
+
+lemma submonoid.is_closed_topological_closure (s : submonoid M) :
+  is_closed (s.topological_closure : set M) :=
+by convert is_closed_closure
+
+lemma submonoid.topological_closure_minimal
+  (s : submonoid M) {t : submonoid M} (h : s ≤ t) (ht : is_closed (t : set M)) :
+  s.topological_closure ≤ t :=
+closure_minimal h ht
+
 @[to_additive exists_open_nhds_zero_half]
 lemma exists_open_nhds_one_split {s : set M} (hs : s ∈ 𝓝 (1 : M)) :
   ∃ V : set M, is_open V ∧ (1 : M) ∈ V ∧ ∀ (v ∈ V) (w ∈ V), v * w ∈ s :=