refactor(topology/algebra): define has_continuous_smul, use for top…

…ological semirings and algebras (#6823)

docs/overview.yaml

@@ -213,7 +213,7 @@ Topology:
     infinite sum: 'has_sum'
     topological ring: 'topological_ring'
     completion of a topological ring: 'uniform_space.completion.ring'
-    topological module: 'topological_module'
+    topological module: 'has_continuous_smul'
     Haar measure on a locally compact Hausdorff group: 'measure_theory.measure.haar_measure'
   Metric spaces:
     metric space: 'metric_space'
@@ -230,7 +230,7 @@ Topology:
 Analysis:
   Normed vector spaces:
     normed vector space over a normed field: 'normed_space'
-    topology on a normed vector space: 'normed_space.topological_vector_space'
+    topology on a normed vector space: 'normed_space.has_continuous_smul'
     equivalence of norms in finite dimension: 'linear_equiv.to_continuous_linear_equiv'
     finite dimensional normed spaces over complete normed fields are complete: 'submodule.complete_of_finite_dimensional'
     Heine-Borel theorem (finite dimensional normed spaces are proper): 'finite_dimensional.proper'

docs/undergrad.yaml

@@ -412,7 +412,7 @@ Topology:
     complete metric spaces: 'metric.complete_of_cauchy_seq_tendsto'
     contraction mapping theorem: 'contracting_with.exists_fixed_point'
   Normed vector spaces on $\R$ and $\C$:
-    topology on a normed vector space: 'normed_space.topological_vector_space'
+    topology on a normed vector space: 'normed_space.has_continuous_smul'
     equivalent norms:
     Banach open mapping theorem: 'open_mapping'
     equivalence of norms in finite dimension: 'linear_equiv.to_continuous_linear_equiv'

src/algebra/algebra/basic.lean

@@ -158,6 +158,9 @@ lemma algebra_map_eq_smul_one (r : R) : algebra_map R A r = r • 1 :=
 calc algebra_map R A r = algebra_map R A r * 1 : (mul_one _).symm
                    ... = r • 1                 : (algebra.smul_def r 1).symm
 
+lemma algebra_map_eq_smul_one' : ⇑(algebra_map R A) = λ r, r • (1 : A) :=
+funext algebra_map_eq_smul_one
+
 theorem commutes (r : R) (x : A) : algebra_map R A r * x = x * algebra_map R A r :=
 algebra.commutes' r x
 

src/analysis/convex/extrema.lean

@@ -15,7 +15,7 @@ a global minimum, and likewise for concave functions.
 -/
 
 variables {E β: Type*} [add_comm_group E] [topological_space E]
-  [module ℝ E] [topological_add_group E] [topological_vector_space ℝ E]
+  [module ℝ E] [topological_add_group E] [has_continuous_smul ℝ E]
   [linear_ordered_add_comm_group β] [semimodule ℝ β] [ordered_semimodule ℝ β]
   {s : set E}
 

src/analysis/convex/topology.lean

@@ -72,10 +72,10 @@ end std_simplex
 
 /-! ### Topological vector space -/
 
-section topological_vector_space
+section has_continuous_smul
 
 variables [add_comm_group E] [vector_space ℝ E] [topological_space E]
-  [topological_add_group E] [topological_vector_space ℝ E]
+  [topological_add_group E] [has_continuous_smul ℝ E]
 
 /-- In a topological vector space, the interior of a convex set is convex. -/
 lemma convex.interior {s : set E} (hs : convex s) : convex (interior s) :=
@@ -85,10 +85,10 @@ convex_iff_pointwise_add_subset.mpr $ λ a b ha hb hab,
   (λ heq,
     have hne : b ≠ 0, by { rw [heq, zero_add] at hab, rw hab, exact one_ne_zero },
     by { rw ← image_smul,
-         exact (is_open_map_smul_of_ne_zero hne _ is_open_interior).add_left } )
+         exact (is_open_map_smul' hne _ is_open_interior).add_left } )
   (λ hne,
     by { rw ← image_smul,
-         exact (is_open_map_smul_of_ne_zero hne _ is_open_interior).add_right }),
+         exact (is_open_map_smul' hne _ is_open_interior).add_right }),
   (subset_interior_iff_subset_of_open h).mpr $ subset.trans
     (by { simp only [← image_smul], apply add_subset_add; exact image_subset _ interior_subset })
     (convex_iff_pointwise_add_subset.mp hs ha hb hab)
@@ -118,7 +118,7 @@ lemma set.finite.is_closed_convex_hull [t2_space E] {s : set E} (hs : finite s)
   is_closed (convex_hull s) :=
 hs.compact_convex_hull.is_closed
 
-end topological_vector_space
+end has_continuous_smul
 
 /-! ### Normed vector space -/
 

src/analysis/normed_space/basic.lean

@@ -1030,7 +1030,7 @@ variables {E : Type*} {F : Type*}
 [normed_group E] [normed_space α E] [normed_group F] [normed_space α F]
 
 @[priority 100] -- see Note [lower instance priority]
-instance normed_space.topological_vector_space : topological_vector_space α E :=
+instance normed_space.has_continuous_smul : has_continuous_smul α E :=
 begin
   refine { continuous_smul := continuous_iff_continuous_at.2 $
     λ p, tendsto_iff_norm_tendsto_zero.2 _ },
@@ -1205,21 +1205,6 @@ normed_algebra.norm_algebra_map_eq _
 variables (𝕜 : Type*) [normed_field 𝕜]
 variables (𝕜' : Type*) [normed_ring 𝕜']
 
--- This could also be proved via `linear_map.continuous_of_bound`,
--- but this is further up the import tree in `normed_space.operator_norm`, so not yet available.
-@[continuity] lemma normed_algebra.algebra_map_continuous
-  [normed_algebra 𝕜 𝕜'] :
-  continuous (algebra_map 𝕜 𝕜') :=
-begin
-  change continuous (algebra_map 𝕜 𝕜').to_add_monoid_hom,
-  exact add_monoid_hom.continuous_of_bound _ 1 (λ x, by simp),
-end
-
-@[priority 100]
-instance normed_algebra.to_topological_algebra [normed_algebra 𝕜 𝕜'] :
-  topological_algebra 𝕜 𝕜' :=
-⟨by continuity⟩
-
 @[priority 100]
 instance normed_algebra.to_normed_space [h : normed_algebra 𝕜 𝕜'] : normed_space 𝕜 𝕜' :=
 { norm_smul_le := λ s x, calc

src/analysis/normed_space/finite_dimension.lean

@@ -48,7 +48,7 @@ noncomputable theory
 /-- A linear map on `ι → 𝕜` (where `ι` is a fintype) is continuous -/
 lemma linear_map.continuous_on_pi {ι : Type w} [fintype ι] {𝕜 : Type u} [normed_field 𝕜]
   {E : Type v}  [add_comm_group E] [vector_space 𝕜 E] [topological_space E]
-  [topological_add_group E] [topological_vector_space 𝕜 E] (f : (ι → 𝕜) →ₗ[𝕜] E) : continuous f :=
+  [topological_add_group E] [has_continuous_smul 𝕜 E] (f : (ι → 𝕜) →ₗ[𝕜] E) : continuous f :=
 begin
   -- for the proof, write `f` in the standard basis, and use that each coordinate is a continuous
   -- function.
@@ -66,7 +66,7 @@ variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
 {E : Type v} [normed_group E] [normed_space 𝕜 E]
 {F : Type w} [normed_group F] [normed_space 𝕜 F]
 {F' : Type x} [add_comm_group F'] [vector_space 𝕜 F'] [topological_space F']
-[topological_add_group F'] [topological_vector_space 𝕜 F']
+[topological_add_group F'] [has_continuous_smul 𝕜 F']
 [complete_space 𝕜]
 
 /-- In finite dimension over a complete field, the canonical identification (in terms of a basis)

src/analysis/normed_space/operator_norm.lean

@@ -414,7 +414,7 @@ le_antisymm
 
 /-- `continuous_linear_map.prod` as a `linear_isometry_equiv`. -/
 def prodₗᵢ (R : Type*) [ring R] [topological_space R] [module R F] [module R G]
-  [topological_module R F] [topological_module R G]
+  [has_continuous_smul R F] [has_continuous_smul R G]
   [smul_comm_class 𝕜 R F] [smul_comm_class 𝕜 R G] :
   (E →L[𝕜] F) × (E →L[𝕜] G) ≃ₗᵢ[R] (E →L[𝕜] F × G) :=
 ⟨prodₗ R, λ ⟨f, g⟩, op_norm_prod f g⟩
@@ -907,7 +907,7 @@ le_antisymm (op_norm_le_bound _ (norm_nonneg _) $ λ x, f.le_op_norm x)
   (op_norm_le_bound _ (norm_nonneg _) $ λ x, f.le_op_norm x)
 
 variables (𝕜 E F 𝕜') (𝕜'' : Type*) [ring 𝕜''] [topological_space 𝕜''] [module 𝕜'' F]
-  [topological_module 𝕜'' F] [smul_comm_class 𝕜 𝕜'' F] [smul_comm_class 𝕜' 𝕜'' F]
+  [has_continuous_smul 𝕜'' F] [smul_comm_class 𝕜 𝕜'' F] [smul_comm_class 𝕜' 𝕜'' F]
 
 /-- `continuous_linear_map.restrict_scalars` as a `linear_isometry`. -/
 def restrict_scalars_isometry : (E →L[𝕜] F) →ₗᵢ[𝕜''] (E →L[𝕜'] F) :=

src/analysis/seminorm.lean

@@ -75,7 +75,7 @@ end
 /-!
 Properties of balanced and absorbing sets in a topological vector space:
 -/
-variables [topological_space E] [topological_vector_space 𝕜 E]
+variables [topological_space E] [has_continuous_smul 𝕜 E]
 
 /-- Every neighbourhood of the origin is absorbent. -/
 lemma absorbent_nhds_zero (hA : A ∈ 𝓝 (0 : E)) : absorbent 𝕜 A :=
@@ -106,16 +106,12 @@ lemma balanced_zero_union_interior (hA : balanced 𝕜 A) :
 begin
   intros a ha, by_cases a = 0,
   { rw [h, zero_smul_set],
-    apply subset_union_left _,
-    exact union_nonempty.mpr (or.intro_left _ $ singleton_nonempty _) },
-  { rw [←image_smul, image_union, union_subset_iff], split,
-    { rw [image_singleton, smul_zero], exact subset_union_left _ _ },
-    { apply subset_union_of_subset_right,
-      apply interior_maximal,
-      rw image_subset_iff,
-      calc _ ⊆ A : interior_subset
-      ...    ⊆ _ : by { rw ←image_subset_iff, exact hA _ ha},
-      exact is_open_map_smul_of_ne_zero h _ is_open_interior }},
+    exacts [subset_union_left _ _, ⟨0, or.inl rfl⟩] },
+  { rw [←image_smul, image_union],
+    apply union_subset_union,
+    { rw [image_singleton, smul_zero] },
+    { calc a • interior A ⊆ interior (a • A) : (is_open_map_smul' h).image_interior_subset A
+                      ... ⊆ interior A       : interior_mono (hA _ ha) } }
 end
 
 /-- The interior of a balanced set is balanced if it contains the origin. -/
@@ -129,14 +125,9 @@ end
 
 /-- The closure of a balanced set is balanced. -/
 lemma balanced.closure (hA : balanced 𝕜 A) : balanced 𝕜 (closure A) :=
-begin
-  intros a ha,
-  calc _ ⊆ closure (a • A) :
-  by { simp_rw ←image_smul,
-       exact image_closure_subset_closure_image
-               (continuous_const.smul continuous_id) }
-  ...    ⊆ _ : closure_mono (hA _ ha),
-end
+assume a ha,
+calc _ ⊆ closure (a • A) : image_closure_subset_closure_image (continuous_id.const_smul _)
+...    ⊆ _ : closure_mono (hA _ ha)
 
 end
 

src/data/equiv/mul_add.lean

@@ -362,6 +362,8 @@ def to_units {G} [group G] : G ≃* units G :=
   right_inv := λ u, units.ext rfl,
   map_mul' := λ x y, units.ext rfl }
 
+protected lemma group.is_unit {G} [group G] (x : G) : is_unit x := is_unit_unit (to_units x)
+
 namespace units
 
 variables [monoid M] [monoid N] [monoid P]

src/geometry/manifold/basic_smooth_bundle.lean

@@ -511,7 +511,7 @@ instance : smooth_manifold_with_corners I.tangent (tangent_bundle I M) :=
 local attribute [reducible] tangent_space
 variables {M} (x : M)
 
-instance : topological_module 𝕜 (tangent_space I x) := by apply_instance
+instance : has_continuous_smul 𝕜 (tangent_space I x) := by apply_instance
 instance : topological_space (tangent_space I x) := by apply_instance
 instance : add_comm_group (tangent_space I x) := by apply_instance
 instance : topological_add_group (tangent_space I x) := by apply_instance

src/measure_theory/ae_eq_fun.lean

@@ -374,7 +374,7 @@ section semimodule
 
 variables {𝕜 : Type*} [semiring 𝕜] [topological_space 𝕜]
 variables [topological_space γ] [borel_space γ] [add_comm_monoid γ] [semimodule 𝕜 γ]
-  [topological_semimodule 𝕜 γ]
+  [has_continuous_smul 𝕜 γ]
 
 instance : has_scalar 𝕜 (α →ₘ[μ] γ) :=
 ⟨λ c f, comp ((•) c) (measurable_id.const_smul c) f⟩

src/measure_theory/borel_space.lean

@@ -431,43 +431,43 @@ h.measurable.comp_ae_measurable (hf.prod_mk hg)
 
 lemma measurable.smul [semiring α] [second_countable_topology α]
   [add_comm_monoid γ] [second_countable_topology γ]
-  [semimodule α γ] [topological_semimodule α γ]
+  [semimodule α γ] [has_continuous_smul α γ]
   {f : δ → α} {g : δ → γ} (hf : measurable f) (hg : measurable g) :
   measurable (λ c, f c • g c) :=
 continuous_smul.measurable2 hf hg
 
 lemma ae_measurable.smul [semiring α] [second_countable_topology α]
   [add_comm_monoid γ] [second_countable_topology γ]
-  [semimodule α γ] [topological_semimodule α γ]
+  [semimodule α γ] [has_continuous_smul α γ]
   {f : δ → α} {g : δ → γ} {μ : measure δ} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
   ae_measurable (λ c, f c • g c) μ :=
 continuous_smul.ae_measurable2 hf hg
 
 lemma measurable.const_smul {R M : Type*} [topological_space R] [semiring R]
-  [add_comm_monoid M] [semimodule R M] [topological_space M] [topological_semimodule R M]
+  [add_comm_monoid M] [semimodule R M] [topological_space M] [has_continuous_smul R M]
   [measurable_space M] [borel_space M]
   {f : δ → M} (hf : measurable f) (c : R) :
   measurable (λ x, c • f x) :=
 (continuous_const.smul continuous_id).measurable.comp hf
 
 lemma ae_measurable.const_smul {R M : Type*} [topological_space R] [semiring R]
-  [add_comm_monoid M] [semimodule R M] [topological_space M] [topological_semimodule R M]
+  [add_comm_monoid M] [semimodule R M] [topological_space M] [has_continuous_smul R M]
   [measurable_space M] [borel_space M]
   {f : δ → M} {μ : measure δ} (hf : ae_measurable f μ) (c : R) :
   ae_measurable (λ x, c • f x) μ :=
 (continuous_const.smul continuous_id).measurable.comp_ae_measurable hf
 
 lemma measurable_const_smul_iff {α : Type*} [topological_space α]
   [division_ring α] [add_comm_monoid γ]
-  [semimodule α γ] [topological_semimodule α γ]
+  [semimodule α γ] [has_continuous_smul α γ]
   {f : δ → γ} {c : α} (hc : c ≠ 0) :
   measurable (λ x, c • f x) ↔ measurable f :=
 ⟨λ h, by simpa only [smul_smul, inv_mul_cancel hc, one_smul] using h.const_smul c⁻¹,
   λ h, h.const_smul c⟩
 
 lemma ae_measurable_const_smul_iff {α : Type*} [topological_space α]
   [division_ring α] [add_comm_monoid γ]
-  [semimodule α γ] [topological_semimodule α γ]
+  [semimodule α γ] [has_continuous_smul α γ]
   {f : δ → γ} {μ : measure δ} {c : α} (hc : c ≠ 0) :
   ae_measurable (λ x, c • f x) μ ↔ ae_measurable f μ :=
 ⟨λ h, by simpa only [smul_smul, inv_mul_cancel hc, one_smul] using h.const_smul c⁻¹,

src/topology/algebra/affine.lean

@@ -40,7 +40,7 @@ begin
 end
 
 /-- The line map is continuous. -/
-lemma line_map_continuous [topological_space R] [topological_semimodule R F] {p v : F} :
+lemma line_map_continuous [topological_space R] [has_continuous_smul R F] {p v : F} :
   continuous ⇑(line_map p v : R →ᵃ[R] F) :=
 continuous_iff.mpr $ (continuous_id.smul continuous_const).add $
   @continuous_const _ _ _ _ (0 : F)

src/topology/algebra/algebra.lean

@@ -9,8 +9,9 @@ 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`.
+A topological algebra over a topological semiring `R` is a topological ring with a compatible
+continuous scalar multiplication by elements of `R`. We reuse typeclass `has_continuous_smul` for
+topological algebras.
 
 ## Results
 
@@ -26,52 +27,50 @@ open_locale classical
 universes u v w
 
 section topological_algebra
-variables (R : Type*) [topological_space R] [comm_ring R] [topological_ring R]
+variables (R : Type*) [topological_space R] [comm_semiring 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
+variables [semiring A]
+
+lemma continuous_algebra_map_iff_smul [algebra R A] [topological_semiring A] :
+  continuous (algebra_map R A) ↔ continuous (λ p : R × A, p.1 • p.2) :=
+begin
+  refine ⟨λ h, _, λ h, _⟩,
+  { simp only [algebra.smul_def], exact (h.comp continuous_fst).mul continuous_snd },
+  { rw algebra_map_eq_smul_one', exact h.comp (continuous_id.prod_mk continuous_const) }
+end
+
+@[continuity]
+lemma continuous_algebra_map [algebra R A] [topological_semiring A] [has_continuous_smul R A] :
+  continuous (algebra_map R A) :=
+(continuous_algebra_map_iff_smul R A).2 continuous_smul
+
+lemma has_continuous_smul_of_algebra_map [algebra R A] [topological_semiring A]
+  (h : continuous (algebra_map R A)) :
+  has_continuous_smul R A :=
+⟨(continuous_algebra_map_iff_smul R A).1 h⟩
 
 end topological_algebra
 
 section topological_algebra
-variables {R : Type*} [comm_ring R]
+variables {R : Type*} [comm_semiring 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, }
+variables [semiring A]
+variables [algebra R A] [topological_semiring A]
 
 /-- 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 }
+  algebra_map_mem' := λ r, s.to_subsemiring.subring_topological_closure (s.algebra_map_mem r),
+  .. s.to_subsemiring.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_semiring (s : subalgebra R A) :
+  topological_semiring (s.topological_closure) :=
+s.to_subsemiring.topological_closure_topological_semiring
 
 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 }
+  [topological_space R] [has_continuous_smul R A] (s : subalgebra R A) :
+  has_continuous_smul R (s.topological_closure) :=
+s.to_submodule.topological_closure_has_continuous_smul
 
 lemma subalgebra.subring_topological_closure (s : subalgebra R A) :
   s ≤ s.topological_closure :=