feat(topology/constructions): distributivity of products over sums (#…

…1059)

* feat(topology/constructions): distributivity of products over sums

* Update src/topology/maps.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Reverse direction of sigma_prod_distrib

src/data/equiv/basic.lean

@@ -491,6 +491,13 @@ calc α × (β ⊕ γ) ≃ (β ⊕ γ) × α       : prod_comm _ _
 @[simp] theorem prod_sum_distrib_apply_right {α β γ} (a : α) (c : γ) :
    prod_sum_distrib α β γ (a, sum.inr c) = sum.inr (a, c) := rfl
 
+def sigma_prod_distrib {ι : Type*} (α : ι → Type*) (β : Type*) :
+  ((Σ i, α i) × β) ≃ (Σ i, (α i × β)) :=
+⟨λ p, ⟨p.1.1, (p.1.2, p.2)⟩,
+ λ p, (⟨p.1, p.2.1⟩, p.2.2),
+ λ p, by { rcases p with ⟨⟨_, _⟩, _⟩, refl },
+ λ p, by { rcases p with ⟨_, ⟨_, _⟩⟩, refl }⟩
+
 def bool_prod_equiv_sum (α : Type u) : bool × α ≃ α ⊕ α :=
 calc bool × α ≃ (unit ⊕ unit) × α       : prod_congr bool_equiv_punit_sum_punit (equiv.refl _)
       ...     ≃ α × (unit ⊕ unit)       : prod_comm _ _

src/data/set/lattice.lean

@@ -446,6 +446,16 @@ set.ext $ by simp
 theorem Union_eq_range_sigma (s : α → set β) : (⋃ i, s i) = range (λ a : Σ i, s i, a.2) :=
 by simp [set.ext_iff]
 
+theorem Union_image_preimage_sigma_mk_eq_self {ι : Type*} {σ : ι → Type*} (s : set (sigma σ)) :
+  (⋃ i, sigma.mk i '' (sigma.mk i ⁻¹' s)) = s :=
+begin
+  ext x,
+  simp only [mem_Union, mem_image, mem_preimage],
+  split,
+  { rintros ⟨i, a, h, rfl⟩, exact h },
+  { intro h, cases x with i a, exact ⟨i, a, h, rfl⟩ }
+end
+
 lemma sUnion_mono {s t : set (set α)} (h : s ⊆ t) : (⋃₀ s) ⊆ (⋃₀ t) :=
 sUnion_subset $ assume t' ht', subset_sUnion_of_mem $ h ht'
 

src/topology/constructions.lean

@@ -154,6 +154,13 @@ begin
   exact filter.prod_mono ((is_open_map_iff_nhds_le f).1 hf a) ((is_open_map_iff_nhds_le g).1 hg b)
 end
 
+protected lemma open_embedding.prod
+  [topological_space α] [topological_space β] [topological_space γ] [topological_space δ]
+  {f : α → β} {g : γ → δ} (hf : open_embedding f) (hg : open_embedding g) :
+  open_embedding (λx:α×γ, (f x.1, g x.2)) :=
+open_embedding_of_embedding_open (hf.1.prod_mk hg.1)
+  (hf.is_open_map.prod hg.is_open_map)
+
 section tube_lemma
 
 def nhds_contain_boxes (s : set α) (t : set β) : Prop :=
@@ -696,6 +703,10 @@ end
 lemma is_closed_sigma_mk {i : ι} : is_closed (set.range (@sigma.mk ι σ i)) :=
 by { rw ←set.image_univ, exact is_closed_map_sigma_mk _ is_closed_univ }
 
+lemma open_embedding_sigma_mk {i : ι} : open_embedding (@sigma.mk ι σ i) :=
+open_embedding_of_continuous_injective_open
+  continuous_sigma_mk injective_sigma_mk is_open_map_sigma_mk
+
 lemma closed_embedding_sigma_mk {i : ι} : closed_embedding (@sigma.mk ι σ i) :=
 closed_embedding_of_continuous_injective_closed
   continuous_sigma_mk injective_sigma_mk is_closed_map_sigma_mk
@@ -715,6 +726,21 @@ continuous_sigma $ λ i,
   show continuous (λ a, sigma.mk (f₁ i) (f₂ i a)),
   from continuous_sigma_mk.comp (hf i)
 
+lemma is_open_map_sigma [topological_space β] {f : sigma σ → β}
+  (h : ∀ i, is_open_map (λ a, f ⟨i, a⟩)) : is_open_map f :=
+begin
+  intros s hs,
+  rw is_open_sigma_iff at hs,
+  have : s = ⋃ i, sigma.mk i '' (sigma.mk i ⁻¹' s),
+  { rw Union_image_preimage_sigma_mk_eq_self },
+  rw this,
+  rw [image_Union],
+  apply is_open_Union,
+  intro i,
+  rw [image_image],
+  exact h i _ (hs i)
+end
+
 /-- The sum of embeddings is an embedding. -/
 lemma embedding_sigma_map {τ : ι → Type*} [Π i, topological_space (τ i)]
   {f : Π i, σ i → τ i} (hf : ∀ i, embedding (f i)) : embedding (sigma.map id f) :=
@@ -1021,10 +1047,10 @@ lemma range_coe (h : α ≃ₜ β) : range h = univ :=
 eq_univ_of_forall $ assume b, ⟨h.symm b, congr_fun h.self_comp_symm b⟩
 
 lemma image_symm (h : α ≃ₜ β) : image h.symm = preimage h :=
-image_eq_preimage_of_inverse h.symm.to_equiv.left_inv h.symm.to_equiv.right_inv
+funext h.symm.to_equiv.image_eq_preimage
 
 lemma preimage_symm (h : α ≃ₜ β) : preimage h.symm = image h :=
-(image_eq_preimage_of_inverse h.to_equiv.left_inv h.to_equiv.right_inv).symm
+(funext h.to_equiv.image_eq_preimage).symm
 
 lemma induced_eq
   {α : Type*} {β : Type*} [tα : topological_space α] [tβ : topological_space β] (h : α ≃ₜ β) :
@@ -1074,6 +1100,16 @@ begin
   exact continuous_iff_is_closed.1 (h.symm.continuous) _
 end
 
+def homeomorph_of_continuous_open (e : α ≃ β) (h₁ : continuous e) (h₂ : is_open_map e) :
+  α ≃ₜ β :=
+{ continuous_to_fun := h₁,
+  continuous_inv_fun := begin
+    intros s hs,
+    convert ← h₂ s hs using 1,
+    apply e.image_eq_preimage
+  end,
+  .. e }
+
 protected lemma quotient_map (h : α ≃ₜ β) : quotient_map h :=
 ⟨h.to_equiv.surjective, h.coinduced_eq.symm⟩
 
@@ -1103,4 +1139,17 @@ def prod_assoc : (α × β) × γ ≃ₜ α × (β × γ) :=
 
 end
 
+section distrib
+variables {ι : Type*} {σ : ι → Type*} [Π i, topological_space (σ i)] [topological_space β]
+
+def sigma_prod_distrib : ((Σ i, σ i) × β) ≃ₜ (Σ i, (σ i × β)) :=
+homeomorph.symm $
+homeomorph_of_continuous_open (equiv.sigma_prod_distrib σ β).symm
+  (continuous_sigma $ λ i,
+    continuous.prod_mk (continuous_sigma_mk.comp continuous_fst) continuous_snd)
+  (is_open_map_sigma $ λ i,
+    (open_embedding.prod open_embedding_sigma_mk open_embedding_id).is_open_map)
+
+end distrib
+
 end homeomorph

src/topology/maps.lean

@@ -465,6 +465,56 @@ this ▸ continuous_iff_is_closed.mp h s hs
 
 end is_closed_map
 
+section open_embedding
+variables [topological_space α] [topological_space β] [topological_space γ]
+
+/-- An open embedding is an embedding with open image. -/
+def open_embedding (f : α → β) : Prop := embedding f ∧ is_open (range f)
+
+lemma open_embedding.open_iff_image_open {f : α → β} (hf : open_embedding f)
+  {s : set α} : is_open s ↔ is_open (f '' s) :=
+⟨embedding_open hf.1 hf.2,
+ λ h, begin
+   convert ←hf.1.continuous _ h,
+   apply preimage_image_eq _ hf.1.inj
+ end⟩
+
+lemma open_embedding.is_open_map {f : α → β} (hf : open_embedding f) : is_open_map f :=
+λ s, hf.open_iff_image_open.mp
+
+lemma open_embedding.open_iff_preimage_open {f : α → β} (hf : open_embedding f)
+  {s : set β} (hs : s ⊆ range f) : is_open s ↔ is_open (f ⁻¹' s) :=
+begin
+  convert ←hf.open_iff_image_open.symm,
+  rwa [image_preimage_eq_inter_range, inter_eq_self_of_subset_left]
+end
+
+lemma open_embedding_of_embedding_open {f : α → β} (h₁ : embedding f)
+  (h₂ : is_open_map f) : open_embedding f :=
+⟨h₁, by convert h₂ univ is_open_univ; simp⟩
+
+lemma open_embedding_of_continuous_injective_open {f : α → β} (h₁ : continuous f)
+  (h₂ : function.injective f) (h₃ : is_open_map f) : open_embedding f :=
+begin
+  refine open_embedding_of_embedding_open ⟨⟨_⟩, h₂⟩ h₃,
+  apply le_antisymm (continuous_iff_le_induced.mp h₁) _,
+  intro s,
+  change is_open _ ≤ is_open _,
+  rw is_open_induced_iff,
+  refine λ hs, ⟨f '' s, h₃ s hs, _⟩,
+  rw preimage_image_eq _ h₂
+end
+
+lemma open_embedding_id : open_embedding (@id α) :=
+⟨embedding_id, by convert is_open_univ; apply range_id⟩
+
+lemma open_embedding_compose {f : α → β} {g : β → γ}
+  (hg : open_embedding g) (hf : open_embedding f) : open_embedding (g ∘ f) :=
+⟨hg.1.comp hf.1, show is_open (range (g ∘ f)),
+ by rw [range_comp, ←hg.open_iff_image_open]; exact hf.2⟩
+
+end open_embedding
+
 section closed_embedding
 variables [topological_space α] [topological_space β] [topological_space γ]
 
@@ -479,17 +529,24 @@ lemma closed_embedding.closed_iff_image_closed {f : α → β} (hf : closed_embe
    apply preimage_image_eq _ hf.1.inj
  end⟩
 
+lemma closed_embedding.is_closed_map {f : α → β} (hf : closed_embedding f) : is_closed_map f :=
+λ s, hf.closed_iff_image_closed.mp
+
 lemma closed_embedding.closed_iff_preimage_closed {f : α → β} (hf : closed_embedding f)
   {s : set β} (hs : s ⊆ range f) : is_closed s ↔ is_closed (f ⁻¹' s) :=
 begin
   convert ←hf.closed_iff_image_closed.symm,
   rwa [image_preimage_eq_inter_range, inter_eq_self_of_subset_left]
 end
 
+lemma closed_embedding_of_embedding_closed {f : α → β} (h₁ : embedding f)
+  (h₂ : is_closed_map f) : closed_embedding f :=
+⟨h₁, by convert h₂ univ is_closed_univ; simp⟩
+
 lemma closed_embedding_of_continuous_injective_closed {f : α → β} (h₁ : continuous f)
   (h₂ : function.injective f) (h₃ : is_closed_map f) : closed_embedding f :=
 begin
-  refine ⟨⟨⟨_⟩, h₂⟩, by convert h₃ univ is_closed_univ; simp⟩,
+  refine closed_embedding_of_embedding_closed ⟨⟨_⟩, h₂⟩ h₃,
   apply le_antisymm (continuous_iff_le_induced.mp h₁) _,
   intro s',
   change is_open _ ≤ is_open _,