refactor(topology/*): define and use dense_inducing

src/data/prod.lean

@@ -78,3 +78,9 @@ instance lex.decidable [decidable_eq α] [decidable_eq β]
 λ p q, decidable_of_decidable_of_iff (by apply_instance) (lex_def r s).symm
 
 end prod
+
+open function
+
+lemma function.injective_prod {f : α → γ} {g : β → δ} (hf : injective f) (hg : injective g) :
+  injective (λ p : α × β, (f p.1, g p.2)) :=
+assume ⟨a₁, b₁⟩ ⟨a₂, b₂⟩, by { simp [prod.mk.inj_iff],exact λ ⟨eq₁, eq₂⟩, ⟨hf eq₁, hg eq₂⟩ }

src/logic/function.lean

@@ -218,6 +218,17 @@ end update
 lemma uncurry_def {α β γ} (f : α → β → γ) : uncurry f = (λp, f p.1 p.2) :=
 funext $ assume ⟨a, b⟩, rfl
 
+-- `uncurry'` is the version of `uncurry` with correct definitional reductions
+def uncurry' {α β γ} (f : α → β → γ) := λ p : α × β, f p.1 p.2
+
+@[simp]
+lemma curry_uncurry' {α : Type*} {β : Type*} {γ : Type*} (f : α → β → γ) : curry (uncurry' f) = f :=
+by funext ; refl
+
+@[simp]
+lemma uncurry'_curry {α : Type*} {β : Type*} {γ : Type*} (f : α × β → γ) : uncurry' (curry f) = f :=
+by { funext, simp [curry, uncurry', prod.mk.eta] }
+
 def restrict {α β} (f : α → β) (s : set α) : subtype s → β := λ x, f x.val
 
 theorem restrict_eq {α β} (f : α → β) (s : set α) : function.restrict f s = f ∘ (@subtype.val _ s) := rfl
@@ -238,6 +249,8 @@ lemma uncurry_bicompr (f : α → β → γ) (g : γ → δ) :
   uncurry (g ∘₂ f) = (g ∘ uncurry f) :=
 funext $ λ ⟨p, q⟩, rfl
 
+lemma uncurry'_bicompr (f : α → β → γ) (g : γ → δ) :
+  uncurry' (g ∘₂ f) = (g ∘ uncurry' f) := rfl
 end bicomp
 
 end function

src/measure_theory/bochner_integration.lean

@@ -93,7 +93,7 @@ variables [normed_space ℝ γ]
 
 -- bochner integration over functions in l1 space
 def integral (f : α →₁ γ) : γ :=
-dense_embedding.extend dense_embedding_of_simple_func simple_func.integral f
+dense_embedding_of_simple_func.to_dense_inducing.extend simple_func.integral f
 
 end l1
 

src/topology/algebra/group_completion.lean

@@ -16,43 +16,48 @@ instance [has_zero α] : has_zero (completion α) := ⟨(0 : α)⟩
 instance [has_neg α] : has_neg (completion α) := ⟨completion.map (λa, -a : α → α)⟩
 instance [has_add α] : has_add (completion α) := ⟨completion.map₂ (+)⟩
 
-lemma coe_zero [has_zero α] : ((0 : α) : completion α) = 0 := rfl
+-- TODO: switch sides once #1103 is fixed
+@[elim_cast]
+lemma coe_zero [has_zero α] : 0 = ((0 : α) : completion α) := rfl
 end group
 
 namespace uniform_space.completion
 section uniform_add_group
 open uniform_space uniform_space.completion
 variables {α : Type*} [uniform_space α] [add_group α] [uniform_add_group α]
 
+@[move_cast]
 lemma coe_neg (a : α) : ((- a : α) : completion α) = - a :=
 (map_coe uniform_continuous_neg' a).symm
 
+@[move_cast]
 lemma coe_add (a b : α) : ((a + b : α) : completion α) = a + b :=
 (map₂_coe_coe a b (+) uniform_continuous_add').symm
 
 instance : add_group (completion α) :=
 { zero_add     := assume a, completion.induction_on a
    (is_closed_eq (continuous_map₂ continuous_const continuous_id) continuous_id)
-    (assume a, show 0 + (a : completion α) = a, by rw [← coe_zero, ← coe_add, zero_add]),
+    (assume a, show 0 + (a : completion α) = a, by rw_mod_cast zero_add),
   add_zero     := assume a, completion.induction_on a
     (is_closed_eq (continuous_map₂ continuous_id continuous_const) continuous_id)
-    (assume a, show (a : completion α) + 0 = a, by rw [← coe_zero, ← coe_add, add_zero]),
+    (assume a, show (a : completion α) + 0 = a, by rw_mod_cast add_zero),
   add_left_neg := assume a, completion.induction_on a
     (is_closed_eq (continuous_map₂ completion.continuous_map continuous_id) continuous_const)
-    (assume a, show - (a : completion α) + a = 0, by rw [← coe_neg, ← coe_add, add_left_neg, coe_zero]),
+    (assume a, show - (a : completion α) + a = 0, by rw_mod_cast add_left_neg),
   add_assoc    := assume a b c, completion.induction_on₃ a b c
     (is_closed_eq
       (continuous_map₂
         (continuous_map₂ continuous_fst (continuous_fst.comp continuous_snd)) (continuous_snd.comp continuous_snd))
       (continuous_map₂ continuous_fst
         (continuous_map₂ (continuous_fst.comp continuous_snd) (continuous_snd.comp continuous_snd))))
     (assume a b c, show (a : completion α) + b + c = a + (b + c),
-      by repeat { rw [← coe_add] }; rw [add_assoc]),
+      by repeat { rw_mod_cast add_assoc }),
   .. completion.has_zero, .. completion.has_neg, ..completion.has_add }
 
 instance : uniform_add_group (completion α) :=
-⟨ (uniform_continuous_map₂' (+)).comp (uniform_continuous.prod_mk uniform_continuous_fst
-    (uniform_continuous_map.comp uniform_continuous_snd)) ⟩
+⟨((uniform_continuous_map₂ (+)).comp
+  (uniform_continuous.prod_mk uniform_continuous_fst
+                              (uniform_continuous_map.comp uniform_continuous_snd)) : _)⟩
 
 instance is_add_group_hom_coe : is_add_group_hom (coe : α → completion α) :=
 ⟨ coe_add ⟩
@@ -66,7 +71,7 @@ have hf : uniform_continuous f, from uniform_continuous_of_continuous hf,
   (is_closed_eq
     (continuous_extension.comp continuous_add')
     (continuous_add (continuous_extension.comp continuous_fst) (continuous_extension.comp continuous_snd)))
-  (assume a b, by rw [← coe_add, extension_coe hf, extension_coe hf, extension_coe hf, is_add_group_hom.map_add f])⟩
+  (assume a b, by rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf, is_add_group_hom.map_add f])⟩
 
 lemma is_add_group_hom_map [add_group β] [uniform_add_group β]
   {f : α → β} [is_add_group_hom f] (hf : continuous f) : is_add_group_hom (completion.map f) :=
@@ -93,8 +98,7 @@ lemma is_add_group_hom_prod [add_group β] [uniform_add_group β] :
       exact continuous.prod_mk (continuous_fst.comp continuous_snd) (continuous_snd.comp continuous_snd) },
     { assume a b c d,
       show completion.prod (↑a + ↑c, ↑b + ↑d) = completion.prod (↑a, ↑b) + completion.prod (↑c, ↑d),
-      rw [← coe_add, ← coe_add, prod_coe_coe, prod_coe_coe, prod_coe_coe, ← coe_add],
-      refl }
+      norm_cast }
   end⟩
 
 end instance_max_depth

src/topology/algebra/ordered.lean

@@ -270,7 +270,8 @@ theorem induced_orderable_topology' {α : Type u} {β : Type v}
 begin
   letI := induced f ta,
   refine ⟨eq_of_nhds_eq_nhds (λ a, _)⟩,
-  rw [nhds_induced_eq_comap, nhds_generate_from, @nhds_eq_orderable β _ _], apply le_antisymm,
+  rw [nhds_induced, nhds_generate_from, @nhds_eq_orderable β _ _],
+  apply le_antisymm,
   { refine le_infi (λ s, le_infi $ λ hs, le_principal_iff.2 _),
     rcases hs with ⟨ab, b, rfl|rfl⟩,
     { exact mem_comap_sets.2 ⟨{x | f b < x},

src/topology/algebra/uniform_group.lean

@@ -13,7 +13,8 @@ Uniform structure on topological groups:
 * `add_group_with_zero_nhd`: construct the topological structure from a group with a neighbourhood
   around zero. Then with `topological_add_group.to_uniform_space` one can derive a `uniform_space`.
 -/
-import topology.uniform_space.uniform_embedding topology.uniform_space.separation topology.algebra.group
+import topology.uniform_space.uniform_embedding topology.uniform_space.complete_separated
+import topology.algebra.group
 
 noncomputable theory
 local attribute [instance, priority 0] classical.prop_decidable
@@ -85,12 +86,12 @@ le_antisymm
       filter.map_mono (uniform_continuous_add uniform_continuous_id uniform_continuous_const))
 
 lemma uniform_embedding_translate (a : α) : uniform_embedding (λx:α, x + a) :=
-begin
-  refine ⟨assume x y, eq_of_add_eq_add_right, _⟩,
-  rw [← uniformity_translate a, comap_map] {occs := occurrences.pos [1]},
-  rintros ⟨p₁, p₂⟩ ⟨q₁, q₂⟩,
-  simp [prod.eq_iff_fst_eq_snd_eq] {contextual := tt}
-end
+{ comap_uniformity := begin
+    rw [← uniformity_translate a, comap_map] {occs := occurrences.pos [1]},
+    rintros ⟨p₁, p₂⟩ ⟨q₁, q₂⟩,
+    simp [prod.eq_iff_fst_eq_snd_eq] {contextual := tt}
+  end,
+  inj := assume x y, eq_of_add_eq_add_right }
 
 section
 variables (α)
@@ -312,7 +313,7 @@ variables [topological_space α] [add_comm_group α] [topological_add_group α]
 
 -- β is a dense subgroup of α, inclusion is denoted by e
 variables [topological_space β] [add_comm_group β] [topological_add_group β]
-variables {e : β → α} [is_add_group_hom e] (de : dense_embedding e)
+variables {e : β → α} [is_add_group_hom e] (de : dense_inducing e)
 include de
 
 lemma tendsto_sub_comap_self (x₀ : α) :
@@ -330,20 +331,7 @@ begin
 end
 end
 
-namespace dense_embedding
-open filter
-variables {α : Type*} [topological_space α]
-variables {β : Type*} [topological_space β]
-variables {γ : Type*} [uniform_space γ] [complete_space γ] [separated γ]
-
-lemma continuous_extend_of_cauchy {e : α → β} {f : α → γ}
-  (de : dense_embedding e) (h : ∀ b : β, cauchy (map f (comap e $ nhds b))) :
-  continuous (de.extend f) :=
-continuous_extend de $ λ b, complete_space.complete (h b)
-
-end dense_embedding
-
-namespace dense_embedding
+namespace dense_inducing
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 variables {G : Type*}
 
@@ -354,8 +342,8 @@ variables [topological_space β] [add_comm_group β] [topological_add_group β]
 variables [topological_space γ] [add_comm_group γ] [topological_add_group γ]
 variables [topological_space δ] [add_comm_group δ] [topological_add_group δ]
 variables [uniform_space G] [add_comm_group G] [uniform_add_group G] [separated G] [complete_space G]
-variables {e : β → α} [is_add_group_hom e] (de : dense_embedding e)
-variables {f : δ → γ} [is_add_group_hom f] (df : dense_embedding f)
+variables {e : β → α} [is_add_group_hom e] (de : dense_inducing e)
+variables {f : δ → γ} [is_add_group_hom f] (df : dense_inducing f)
 variables {φ : β × δ → G} (hφ : continuous φ) [bilin : is_Z_bilin φ]
 
 include de df hφ bilin
@@ -385,7 +373,7 @@ private lemma extend_Z_bilin_key (x₀ : α) (y₀ : γ) :
 begin
   let Nx := nhds x₀,
   let Ny := nhds y₀,
-  let dp := dense_embedding.prod de df,
+  let dp := dense_inducing.prod de df,
   let ee := λ u : β × β, (e u.1, e u.2),
   let ff := λ u : δ × δ, (f u.1, f u.2),
 
@@ -445,22 +433,24 @@ begin
 
   exact W4 h₁ h₂ h₃ h₄
 end
+
 omit W'_nhd
 
+open dense_inducing
+
 /-- Bourbaki GT III.6.5 Theorem I:
-ℤ-bilinear continuous maps from dense sub-groups into a complete Hausdorff group extend by continuity.
+ℤ-bilinear continuous maps from dense images into a complete Hausdorff group extend by continuity.
 Note: Bourbaki assumes that α and β are also complete Hausdorff, but this is not necessary. -/
-theorem extend_Z_bilin  : continuous (extend (dense_embedding.prod de df) φ) :=
+theorem extend_Z_bilin  : continuous (extend (de.prod df) φ) :=
 begin
-  let dp := dense_embedding.prod de df,
-  refine dense_embedding.continuous_extend_of_cauchy (dense_embedding.prod de df) _,
+  refine continuous_extend_of_cauchy _ _,
   rintro ⟨x₀, y₀⟩,
   split,
   { apply map_ne_bot,
     apply comap_neq_bot,
 
     intros U h,
-    rcases exists_mem_of_ne_empty (mem_closure_iff_nhds.1 (dp.dense (x₀, y₀)) U h)
+    rcases exists_mem_of_ne_empty (mem_closure_iff_nhds.1 ((de.prod df).dense (x₀, y₀)) U h)
       with ⟨x, x_in, ⟨z, z_x⟩⟩,
     existsi z,
     cc },
@@ -494,4 +484,4 @@ begin
       rcases p with ⟨⟨x, y⟩, ⟨x', y'⟩⟩,
       apply h ; tauto } }
 end
-end dense_embedding
+end dense_inducing

src/topology/algebra/uniform_ring.lean

@@ -13,35 +13,46 @@ local attribute [instance] classical.prop_decidable
 noncomputable theory
 
 namespace uniform_space.completion
-open dense_embedding uniform_space
-variables (α : Type*) [ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] [separated α]
-
-instance is_Z_bilin_mul : is_Z_bilin (λp:α×α, p.1 * p.2) :=
-⟨assume a a' b, add_mul a a' b, assume a b b', mul_add a b b'⟩
+open dense_inducing uniform_space function
+variables (α : Type*) [ring α] [uniform_space α] [uniform_add_group α] [topological_ring α]
 
 instance : has_one (completion α) := ⟨(1:α)⟩
 
 instance : has_mul (completion α) :=
-⟨λa b, extend (dense_embedding_coe.prod dense_embedding_coe)
-  ((coe : α → completion α) ∘ (λp:α×α, p.1 * p.2)) (a, b)⟩
+  ⟨curry $ (dense_inducing_coe.prod dense_inducing_coe).extend (coe ∘ uncurry' (*))⟩
 
+@[elim_cast]
 lemma coe_one : ((1 : α) : completion α) = 1 := rfl
 
-lemma continuous_mul' : continuous (λp:completion α×completion α, p.1 * p.2) :=
-suffices continuous $ extend (dense_embedding_coe.prod dense_embedding_coe) $
-  ((coe : α → completion α) ∘ (λp:α×α, p.1 * p.2)),
-{ convert this, ext ⟨a, b⟩, refl },
-extend_Z_bilin dense_embedding_coe dense_embedding_coe ((continuous_coe α).comp continuous_mul')
-
-section rules
 variables {α}
+
+@[move_cast]
 lemma coe_mul (a b : α) : ((a * b : α) : completion α) = a * b :=
-eq.symm (extend_e_eq (dense_embedding_coe.prod dense_embedding_coe) (a, b))
+((dense_inducing_coe.prod dense_inducing_coe).extend_eq_of_cont
+  ((continuous_coe α).comp continuous_mul') (a, b)).symm
+
+lemma continuous_mul' : continuous (λ p : completion α × completion α, p.1 * p.2) :=
+begin
+  haveI : is_Z_bilin ((coe ∘ uncurry' (*)) : α × α → completion α) :=
+  { add_left := begin
+      introv,
+      change coe ((a + a')*b) = coe (a*b) + coe (a'*b),
+      rw_mod_cast add_mul
+    end,
+    add_right := begin
+      introv,
+      change coe (a*(b + b')) = coe (a*b) + coe (a*b'),
+      rw_mod_cast mul_add
+    end },
+  have : continuous ((coe ∘ uncurry' (*)) : α × α → completion α),
+    from (continuous_coe α).comp continuous_mul',
+  convert dense_inducing_coe.extend_Z_bilin dense_inducing_coe this,
+  simp only [(*), curry, prod.mk.eta]
+end
 
 lemma continuous_mul {β : Type*} [topological_space β] {f g : β → completion α}
   (hf : continuous f) (hg : continuous g) : continuous (λb, f b * g b) :=
-(continuous_mul' α).comp (continuous.prod_mk hf hg)
-end rules
+continuous_mul'.comp (continuous.prod_mk hf hg)
 
 instance : ring (completion α) :=
 { one_mul       := assume a, completion.induction_on a
@@ -78,27 +89,48 @@ instance : ring (completion α) :=
 
 instance is_ring_hom_coe : is_ring_hom (coe : α → completion α) :=
 ⟨coe_one α, assume a b, coe_mul a b, assume a b, coe_add a b⟩
-universe u
-instance is_ring_hom_extension
-  {β : Type u} [uniform_space β] [ring β] [uniform_add_group β] [topological_ring β]
-    [complete_space β] [separated β]
-  {f : α → β} [is_ring_hom f] (hf : continuous f) :
+
+universes u
+variables {β : Type u} [uniform_space β] [ring β] [uniform_add_group β] [topological_ring β]
+          {f : α → β} [is_ring_hom f] (hf : continuous f)
+
+instance is_ring_hom_extension [complete_space β] [separated β] :
   is_ring_hom (completion.extension f) :=
 have hf : uniform_continuous f, from uniform_continuous_of_continuous hf,
 { map_one := by rw [← coe_one, extension_coe hf, is_ring_hom.map_one f],
   map_add := assume a b, completion.induction_on₂ a b
     (is_closed_eq
       (continuous_extension.comp continuous_add')
-      (continuous_add (continuous_extension.comp continuous_fst) (continuous_extension.comp continuous_snd)))
+      (continuous_add (continuous_extension.comp continuous_fst)
+                      (continuous_extension.comp continuous_snd)))
     (assume a b,
-      by rw [← coe_add, extension_coe hf, extension_coe hf, extension_coe hf, is_add_group_hom.map_add f]),
+      by rw [← coe_add, extension_coe hf, extension_coe hf, extension_coe hf,
+             is_add_group_hom.map_add f]),
   map_mul := assume a b, completion.induction_on₂ a b
     (is_closed_eq
-      (continuous_extension.comp (continuous_mul' α))
-      (_root_.continuous_mul (continuous_extension.comp continuous_fst) (continuous_extension.comp continuous_snd)))
+      (continuous_extension.comp continuous_mul')
+      (_root_.continuous_mul (continuous_extension.comp continuous_fst)
+                             (continuous_extension.comp continuous_snd)))
     (assume a b,
       by rw [← coe_mul, extension_coe hf, extension_coe hf, extension_coe hf, is_ring_hom.map_mul f]) }
 
+instance top_ring_compl : topological_ring (completion α) :=
+{ continuous_add := continuous_add',
+  continuous_mul := continuous_mul',
+  continuous_neg := continuous_neg' }
+
+instance is_ring_hom_map : is_ring_hom (completion.map f) :=
+completion.is_ring_hom_extension $ (continuous_coe β).comp hf
+
+variables (R : Type*) [comm_ring R] [uniform_space R] [uniform_add_group R] [topological_ring R]
+
+instance : comm_ring (completion R) :=
+{ mul_comm := assume a b, completion.induction_on₂ a b
+      (is_closed_eq (continuous_mul continuous_fst continuous_snd)
+                    (continuous_mul continuous_snd continuous_fst))
+      (assume a b, by rw [← coe_mul, ← coe_mul, mul_comm]),
+ ..completion.ring }
+
 end uniform_space.completion