feat(topology/metric_space/*): additive/multiplicative/order_dual instances (#15704)

YaelDillies · YaelDillies · commit 14d34b71b6d8 · 2022-08-06T09:17:24.000Z
Transfer topology, bornology, uniform space and metric space instances to `additive`, `multiplicative` and `order_dual`.
diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean
@@ -231,12 +231,12 @@ end
 
 end pointwise_limits
 
-instance additive.has_continuous_neg [h : topological_space H] [has_inv H]
-  [has_continuous_inv H] : @has_continuous_neg (additive H) h _ :=
+instance [topological_space H] [has_inv H] [has_continuous_inv H] :
+  has_continuous_neg (additive H) :=
 { continuous_neg := @continuous_inv H _ _ _ }
 
-instance multiplicative.has_continuous_inv [h : topological_space H] [has_neg H]
-  [has_continuous_neg H] : @has_continuous_inv (multiplicative H) h _ :=
+instance [topological_space H] [has_neg H] [has_continuous_neg H] :
+  has_continuous_inv (multiplicative H) :=
 { continuous_inv := @continuous_neg H _ _ _ }
 
 end continuous_inv
@@ -1131,12 +1131,12 @@ end
 
 end filter_mul
 
-instance additive.topological_add_group {G} [h : topological_space G]
-  [group G] [topological_group G] : @topological_add_group (additive G) h _ :=
+instance {G} [topological_space G] [group G] [topological_group G] :
+  topological_add_group (additive G) :=
 { continuous_neg := @continuous_inv G _ _ _ }
 
-instance multiplicative.topological_group {G} [h : topological_space G]
-  [add_group G] [topological_add_group G] : @topological_group (multiplicative G) h _ :=
+instance {G} [topological_space G] [add_group G] [topological_add_group G] :
+  topological_group (multiplicative G) :=
 { continuous_inv := @continuous_neg G _ _ _ }
 
 section quotient
diff --git a/src/topology/algebra/monoid.lean b/src/topology/algebra/monoid.lean
@@ -550,12 +550,12 @@ end
 
 end
 
-instance additive.has_continuous_add {M} [h : topological_space M] [has_mul M]
-  [has_continuous_mul M] : @has_continuous_add (additive M) h _ :=
+instance [topological_space M] [has_mul M] [has_continuous_mul M] :
+  has_continuous_add (additive M) :=
 { continuous_add := @continuous_mul M _ _ _ }
 
-instance multiplicative.has_continuous_mul {M} [h : topological_space M] [has_add M]
-  [has_continuous_add M] : @has_continuous_mul (multiplicative M) h _ :=
+instance [topological_space M] [has_add M] [has_continuous_add M] :
+  has_continuous_mul (multiplicative M) :=
 { continuous_mul := @continuous_add M _ _ _ }
 
 section lattice_ops
diff --git a/src/topology/algebra/order/basic.lean b/src/topology/algebra/order/basic.lean
@@ -91,8 +91,6 @@ generally, and suffices to derive many interesting properties relating order and
 class order_closed_topology (α : Type*) [topological_space α] [preorder α] : Prop :=
 (is_closed_le' : is_closed {p:α×α | p.1 ≤ p.2})
 
-instance : Π [topological_space α], topological_space αᵒᵈ := id
-
 instance [topological_space α] [h : first_countable_topology α] : first_countable_topology αᵒᵈ := h
 
 instance [topological_space α] [h : second_countable_topology α] : second_countable_topology αᵒᵈ :=
diff --git a/src/topology/bornology/constructions.lean b/src/topology/bornology/constructions.lean
@@ -145,3 +145,23 @@ alias bounded_space_coe_set_iff ↔ _ bornology.is_bounded.bounded_space_coe
 
 instance [bounded_space α] {p : α → Prop} : bounded_space (subtype p) :=
 (is_bounded.all {x | p x}).bounded_space_subtype
+
+/-!
+### `additive`, `multiplicative`
+
+The bornology on those type synonyms is inherited without change.
+-/
+
+instance : bornology (additive α) := ‹bornology α›
+instance : bornology (multiplicative α) := ‹bornology α›
+instance [bounded_space α] : bounded_space (additive α) := ‹bounded_space α›
+instance [bounded_space α] : bounded_space (multiplicative α) := ‹bounded_space α›
+
+/-!
+### Order dual
+
+The bornology on this type synonym is inherited without change.
+-/
+
+instance : bornology αᵒᵈ := ‹bornology α›
+instance [bounded_space α] : bounded_space αᵒᵈ := ‹bounded_space α›
diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean
@@ -67,6 +67,76 @@ instance Pi.topological_space {β : α → Type v} [t₂ : Πa, topological_spac
 instance ulift.topological_space [t : topological_space α] : topological_space (ulift.{v u} α) :=
 t.induced ulift.down
 
+/-!
+### `additive`, `multiplicative`
+
+The topology on those type synonyms is inherited without change.
+-/
+
+section
+variables [topological_space α]
+
+open additive multiplicative
+
+instance : topological_space (additive α) := ‹topological_space α›
+instance : topological_space (multiplicative α) := ‹topological_space α›
+instance [discrete_topology α] : discrete_topology (additive α) := ‹discrete_topology α›
+instance [discrete_topology α] : discrete_topology (multiplicative α) := ‹discrete_topology α›
+
+lemma continuous_of_mul : continuous (of_mul : α → additive α) := continuous_id
+lemma continuous_to_mul : continuous (to_mul : additive α → α) := continuous_id
+lemma continuous_of_add : continuous (of_add : α → multiplicative α) := continuous_id
+lemma continuous_to_add : continuous (to_add : multiplicative α → α) := continuous_id
+
+lemma is_open_map_of_mul : is_open_map (of_mul : α → additive α) := is_open_map.id
+lemma is_open_map_to_mul : is_open_map (to_mul : additive α → α) := is_open_map.id
+lemma is_open_map_of_add : is_open_map (of_add : α → multiplicative α) := is_open_map.id
+lemma is_open_map_to_add : is_open_map (to_add : multiplicative α → α) := is_open_map.id
+
+lemma is_closed_map_of_mul : is_closed_map (of_mul : α → additive α) := is_closed_map.id
+lemma is_closed_map_to_mul : is_closed_map (to_mul : additive α → α) := is_closed_map.id
+lemma is_closed_map_of_add : is_closed_map (of_add : α → multiplicative α) := is_closed_map.id
+lemma is_closed_map_to_add : is_closed_map (to_add : multiplicative α → α) := is_closed_map.id
+
+local attribute [semireducible] nhds
+
+lemma nhds_of_mul (a : α) : 𝓝 (of_mul a) = map of_mul (𝓝 a) := rfl
+lemma nhds_of_add (a : α) : 𝓝 (of_add a) = map of_add (𝓝 a) := rfl
+lemma nhds_to_mul (a : additive α) : 𝓝 (to_mul a) = map to_mul (𝓝 a) := rfl
+lemma nhds_to_add (a : multiplicative α) : 𝓝 (to_add a) = map to_add (𝓝 a) := rfl
+
+end
+
+/-!
+### Order dual
+
+The topology on this type synonym is inherited without change.
+-/
+
+section
+variables [topological_space α]
+
+open order_dual
+
+instance : topological_space αᵒᵈ := ‹topological_space α›
+instance [discrete_topology α] : discrete_topology (αᵒᵈ) := ‹discrete_topology α›
+
+lemma continuous_to_dual : continuous (to_dual : α → αᵒᵈ) := continuous_id
+lemma continuous_of_dual : continuous (of_dual : αᵒᵈ → α) := continuous_id
+
+lemma is_open_map_to_dual : is_open_map (to_dual : α → αᵒᵈ) := is_open_map.id
+lemma is_open_map_of_dual : is_open_map (of_dual : αᵒᵈ → α) := is_open_map.id
+
+lemma is_closed_map_to_dual : is_closed_map (to_dual : α → αᵒᵈ) := is_closed_map.id
+lemma is_closed_map_of_dual : is_closed_map (of_dual : αᵒᵈ → α) := is_closed_map.id
+
+local attribute [semireducible] nhds
+
+lemma nhds_to_dual (a : α) : 𝓝 (to_dual a) = map to_dual (𝓝 a) := rfl
+lemma nhds_of_dual (a : α) : 𝓝 (of_dual a) = map of_dual (𝓝 a) := rfl
+
+end
+
 lemma quotient.preimage_mem_nhds [topological_space α] [s : setoid α]
   {V : set $ quotient s} {a : α} (hs : V ∈ 𝓝 (quotient.mk a)) : quotient.mk ⁻¹' V ∈ 𝓝 a :=
 preimage_nhds_coinduced hs
diff --git a/src/topology/metric_space/algebra.lean b/src/topology/metric_space/algebra.lean
@@ -176,3 +176,12 @@ instance has_bounded_smul.op [has_smul αᵐᵒᵖ β] [is_central_scalar α β]
     by simpa only [op_smul_eq_smul] using dist_pair_smul x₁ x₂ y }
 
 end has_bounded_smul
+
+instance [monoid α] [has_lipschitz_mul α] : has_lipschitz_add (additive α) :=
+⟨@has_lipschitz_mul.lipschitz_mul α _ _ _⟩
+
+instance [add_monoid α] [has_lipschitz_add α] : has_lipschitz_mul (multiplicative α) :=
+⟨@has_lipschitz_add.lipschitz_add α _ _ _⟩
+
+@[to_additive] instance [monoid α] [has_lipschitz_mul α] : has_lipschitz_mul αᵒᵈ :=
+‹has_lipschitz_mul α›
diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
@@ -54,7 +54,7 @@ open set filter topological_space bornology
 open_locale uniformity topological_space big_operators filter nnreal ennreal
 
 universes u v w
-variables {α : Type u} {β : Type v}
+variables {α : Type u} {β : Type v} {X : Type*}
 
 /-- Construct a uniform structure core from a distance function and metric space axioms.
 This is a technical construction that can be immediately used to construct a uniform structure
@@ -2881,3 +2881,75 @@ instance metric_space_quot {α : Type u} [pseudo_metric_space α] :
     λxc yc zc, quotient.induction_on₃ xc yc zc (λx y z, pseudo_metric_space.dist_triangle _ _ _) }
 
 end eq_rel
+
+/-!
+### `additive`, `multiplicative`
+
+The distance on those type synonyms is inherited without change.
+-/
+
+open additive multiplicative
+
+section
+variables [has_dist X]
+
+instance : has_dist (additive X) := ‹has_dist X›
+instance : has_dist (multiplicative X) := ‹has_dist X›
+
+@[simp] lemma dist_of_mul (a b : X) : dist (of_mul a) (of_mul b) = dist a b := rfl
+@[simp] lemma dist_of_add (a b : X) : dist (of_add a) (of_add b) = dist a b := rfl
+@[simp] lemma dist_to_mul (a b : additive X) : dist (to_mul a) (to_mul b) = dist a b := rfl
+@[simp] lemma dist_to_add (a b : multiplicative X) : dist (to_add a) (to_add b) = dist a b := rfl
+
+end
+
+section
+variables [pseudo_metric_space X]
+
+instance : pseudo_metric_space (additive X) := ‹pseudo_metric_space X›
+instance : pseudo_metric_space (multiplicative X) := ‹pseudo_metric_space X›
+
+@[simp] lemma nndist_of_mul (a b : X) : nndist (of_mul a) (of_mul b) = nndist a b := rfl
+@[simp] lemma nndist_of_add (a b : X) : nndist (of_add a) (of_add b) = nndist a b := rfl
+@[simp] lemma nndist_to_mul (a b : additive X) : nndist (to_mul a) (to_mul b) = nndist a b := rfl
+@[simp] lemma nndist_to_add (a b : multiplicative X) : nndist (to_add a) (to_add b) = nndist a b :=
+rfl
+
+end
+
+instance [metric_space X] : metric_space (additive X) := ‹metric_space X›
+instance [metric_space X] : metric_space (multiplicative X) := ‹metric_space X›
+instance [pseudo_metric_space X] [proper_space X] : proper_space (additive X) := ‹proper_space X›
+instance [pseudo_metric_space X] [proper_space X] : proper_space (multiplicative X) :=
+‹proper_space X›
+
+/-!
+### Order dual
+
+The distance on this type synonym is inherited without change.
+-/
+
+open order_dual
+
+section
+variables [has_dist X]
+
+instance : has_dist Xᵒᵈ := ‹has_dist X›
+
+@[simp] lemma dist_to_dual (a b : X) : dist (to_dual a) (to_dual b) = dist a b := rfl
+@[simp] lemma dist_of_dual (a b : Xᵒᵈ) : dist (of_dual a) (of_dual b) = dist a b := rfl
+
+end
+
+section
+variables [pseudo_metric_space X]
+
+instance : pseudo_metric_space Xᵒᵈ := ‹pseudo_metric_space X›
+
+@[simp] lemma nndist_to_dual (a b : X) : nndist (to_dual a) (to_dual b) = nndist a b := rfl
+@[simp] lemma nndist_of_dual (a b : Xᵒᵈ) : nndist (of_dual a) (of_dual b) = nndist a b := rfl
+
+end
+
+instance [metric_space X] : metric_space Xᵒᵈ := ‹metric_space X›
+instance [pseudo_metric_space X] [proper_space X] : proper_space Xᵒᵈ := ‹proper_space X›
diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean
@@ -33,7 +33,7 @@ noncomputable theory
 open_locale uniformity topological_space big_operators filter nnreal ennreal
 
 universes u v w
-variables {α : Type u} {β : Type v}
+variables {α : Type u} {β : Type v} {X : Type*}
 
 /-- Characterizing uniformities associated to a (generalized) distance function `D`
 in terms of the elements of the uniformity. -/
@@ -1015,3 +1015,51 @@ by simp only [pos_iff_ne_zero, ne.def, diam_eq_zero_iff, set.subsingleton, not_f
 end diam
 
 end emetric
+
+/-!
+### `additive`, `multiplicative`
+
+The distance on those type synonyms is inherited without change.
+-/
+
+open additive multiplicative
+
+section
+variables [has_edist X]
+
+instance : has_edist (additive X) := ‹has_edist X›
+instance : has_edist (multiplicative X) := ‹has_edist X›
+
+@[simp] lemma edist_of_mul (a b : X) : edist (of_mul a) (of_mul b) = edist a b := rfl
+@[simp] lemma edist_of_add (a b : X) : edist (of_add a) (of_add b) = edist a b := rfl
+@[simp] lemma edist_to_mul (a b : additive X) : edist (to_mul a) (to_mul b) = edist a b := rfl
+@[simp] lemma edist_to_add (a b : multiplicative X) : edist (to_add a) (to_add b) = edist a b := rfl
+
+end
+
+instance [pseudo_emetric_space X] : pseudo_emetric_space (additive X) := ‹pseudo_emetric_space X›
+instance [pseudo_emetric_space X] : pseudo_emetric_space (multiplicative X) :=
+‹pseudo_emetric_space X›
+instance [emetric_space X] : emetric_space (additive X) := ‹emetric_space X›
+instance [emetric_space X] : emetric_space (multiplicative X) := ‹emetric_space X›
+
+/-!
+### Order dual
+
+The distance on this type synonym is inherited without change.
+-/
+
+open order_dual
+
+section
+variables [has_edist X]
+
+instance : has_edist Xᵒᵈ := ‹has_edist X›
+
+@[simp] lemma edist_to_dual (a b : X) : edist (to_dual a) (to_dual b) = edist a b := rfl
+@[simp] lemma edist_of_dual (a b : Xᵒᵈ) : edist (of_dual a) (of_dual b) = edist a b := rfl
+
+end
+
+instance [pseudo_emetric_space X] : pseudo_emetric_space Xᵒᵈ := ‹pseudo_emetric_space X›
+instance [emetric_space X] : emetric_space Xᵒᵈ := ‹emetric_space X›
diff --git a/src/topology/uniform_space/basic.lean b/src/topology/uniform_space/basic.lean
@@ -1241,6 +1241,31 @@ instance : uniform_space bool := ⊥
 instance : uniform_space ℕ := ⊥
 instance : uniform_space ℤ := ⊥
 
+section
+variables [uniform_space α]
+
+open additive multiplicative
+
+instance : uniform_space (additive α) := ‹uniform_space α›
+instance : uniform_space (multiplicative α) := ‹uniform_space α›
+
+lemma uniform_continuous_of_mul : uniform_continuous (of_mul : α → additive α) :=
+uniform_continuous_id
+lemma uniform_continuous_to_mul : uniform_continuous (to_mul : additive α → α) :=
+uniform_continuous_id
+lemma uniform_continuous_of_add : uniform_continuous (of_add : α → multiplicative α) :=
+uniform_continuous_id
+lemma uniform_continuous_to_add : uniform_continuous (to_add : multiplicative α → α) :=
+uniform_continuous_id
+
+lemma uniformity_additive : 𝓤 (additive α) = (𝓤 α).map (prod.map of_mul of_mul) :=
+by { convert map_id.symm, exact prod.map_id }
+
+lemma uniformity_multiplicative : 𝓤 (multiplicative α) = (𝓤 α).map (prod.map of_add of_add) :=
+by { convert map_id.symm, exact prod.map_id }
+
+end
+
 instance {p : α → Prop} [t : uniform_space α] : uniform_space (subtype p) :=
 uniform_space.comap subtype.val t
 
