From d7bbeb12f0f0c409db418362d547589d5877a9d1 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Fri, 17 May 2024 12:30:31 +0200 Subject: [PATCH 1/7] first commit --- .../UniformSpace/AbstractCompletion.lean | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean index a379ce6371b921..c61184617a33d6 100644 --- a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean +++ b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean @@ -283,6 +283,29 @@ theorem uniformContinuous_compareEquiv_symm : UniformContinuous (pkg.compareEqui pkg'.uniformContinuous_compare pkg #align abstract_completion.uniform_continuous_compare_equiv_symm AbstractCompletion.uniformContinuous_compareEquiv_symm +/-Let `f : α → β` be a continuous function between a uniform space `α` and a regular topological +space `γ`, and let `pkg, pkg'` be two abstract completions of `α`. Then +if for every point `a : pkg` the filter `f.map (coe⁻¹ (𝓝 a))` obtained by pushing forward with `f` +the preimage in `α` of `𝓝 a` tends to `𝓝 (f.extend a : β)`, then the comparison map +between `pkg` and `pkg'` composed with the extension of `f` to `pkg`` coincides with the +extension of `f` to `pkg'` -/ +theorem CompareComp_Compare (γ : Type*) [TopologicalSpace γ] extend_compare_extend + [T3Space γ] (f : α → γ) (cont_f : Continuous f) : + let _ := pkg.uniformStruct.toTopologicalSpace + let _ := pkg'.uniformStruct.toTopologicalSpace + (_ : ∀ a : pkg.space, + Filter.Tendsto f (Filter.comap pkg.coe (𝓝 a)) (𝓝 ((pkg.denseInducing.extend f) a))) → + pkg.denseInducing.extend f ∘ pkg'.compare pkg = pkg'.denseInducing.extend f := by + let _ := pkg'.uniformStruct + let _ := pkg.uniformStruct + intro _ _ h + have : ∀ x : α, (pkg.denseInducing.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x := by + simp only [Function.comp_apply, compare_coe, DenseInducing.extend_eq _ cont_f, implies_true] + apply (DenseInducing.extend_unique (AbstractCompletion.denseInducing _) this + (Continuous.comp _ (uniformContinuous_compare pkg' pkg).continuous )).symm + apply DenseInducing.continuous_extend + exact fun a => ⟨(pkg.denseInducing.extend f) a, h a⟩ + end Compare section Prod From a4f99b302b79caae4a9703c5392aed7ca75a4532 Mon Sep 17 00:00:00 2001 From: "Filippo A. E. Nuccio" Date: Fri, 17 May 2024 12:35:49 +0200 Subject: [PATCH 2/7] Update Mathlib/Topology/UniformSpace/AbstractCompletion.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> --- Mathlib/Topology/UniformSpace/AbstractCompletion.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean index c61184617a33d6..36fa3c8ec1891a 100644 --- a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean +++ b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean @@ -290,7 +290,7 @@ the preimage in `α` of `𝓝 a` tends to `𝓝 (f.extend a : β)`, then the com between `pkg` and `pkg'` composed with the extension of `f` to `pkg`` coincides with the extension of `f` to `pkg'` -/ theorem CompareComp_Compare (γ : Type*) [TopologicalSpace γ] extend_compare_extend - [T3Space γ] (f : α → γ) (cont_f : Continuous f) : + [T3Space γ] (f : α → γ) (cont_f : Continuous f) : let _ := pkg.uniformStruct.toTopologicalSpace let _ := pkg'.uniformStruct.toTopologicalSpace (_ : ∀ a : pkg.space, From 0407fe085f2d2d136367f4268d9b2646abdea0e0 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Fri, 17 May 2024 14:03:41 +0200 Subject: [PATCH 3/7] fixing --- .../UniformSpace/AbstractCompletion.lean | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean index c61184617a33d6..6741d799e42014 100644 --- a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean +++ b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean @@ -289,22 +289,22 @@ if for every point `a : pkg` the filter `f.map (coe⁻¹ (𝓝 a))` obtained by the preimage in `α` of `𝓝 a` tends to `𝓝 (f.extend a : β)`, then the comparison map between `pkg` and `pkg'` composed with the extension of `f` to `pkg`` coincides with the extension of `f` to `pkg'` -/ -theorem CompareComp_Compare (γ : Type*) [TopologicalSpace γ] extend_compare_extend - [T3Space γ] (f : α → γ) (cont_f : Continuous f) : - let _ := pkg.uniformStruct.toTopologicalSpace - let _ := pkg'.uniformStruct.toTopologicalSpace - (_ : ∀ a : pkg.space, - Filter.Tendsto f (Filter.comap pkg.coe (𝓝 a)) (𝓝 ((pkg.denseInducing.extend f) a))) → - pkg.denseInducing.extend f ∘ pkg'.compare pkg = pkg'.denseInducing.extend f := by - let _ := pkg'.uniformStruct - let _ := pkg.uniformStruct - intro _ _ h - have : ∀ x : α, (pkg.denseInducing.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x := by - simp only [Function.comp_apply, compare_coe, DenseInducing.extend_eq _ cont_f, implies_true] - apply (DenseInducing.extend_unique (AbstractCompletion.denseInducing _) this - (Continuous.comp _ (uniformContinuous_compare pkg' pkg).continuous )).symm - apply DenseInducing.continuous_extend - exact fun a => ⟨(pkg.denseInducing.extend f) a, h a⟩ +-- theorem CompareComp_Compare (γ : Type*) [TopologicalSpace γ] extend_compare_extend +-- [T3Space γ] (f : α → γ) (cont_f : Continuous f) : +-- let _ := pkg.uniformStruct.toTopologicalSpace +-- let _ := pkg'.uniformStruct.toTopologicalSpace +-- (_ : ∀ a : pkg.space, +-- Filter.Tendsto f (Filter.comap pkg.coe (𝓝 a)) (𝓝 ((pkg.denseInducing.extend f) a))) → +-- pkg.denseInducing.extend f ∘ pkg'.compare pkg = pkg'.denseInducing.extend f := by +-- let _ := pkg'.uniformStruct +-- let _ := pkg.uniformStruct +-- intro _ _ h +-- have : ∀ x : α, (pkg.denseInducing.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x := by +-- simp only [Function.comp_apply, compare_coe, DenseInducing.extend_eq _ cont_f, implies_true] +-- apply (DenseInducing.extend_unique (AbstractCompletion.denseInducing _) this +-- (Continuous.comp _ (uniformContinuous_compare pkg' pkg).continuous )).symm +-- apply DenseInducing.continuous_extend +-- exact fun a => ⟨(pkg.denseInducing.extend f) a, h a⟩ end Compare From 0120bdf63fbb2b0cde6027a880eac5be074d6428 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Mon, 20 May 2024 10:24:29 +0200 Subject: [PATCH 4/7] fixed scoped notation --- .../UniformSpace/AbstractCompletion.lean | 35 ++++++++++--------- 1 file changed, 19 insertions(+), 16 deletions(-) diff --git a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean index 6741d799e42014..b90a78ff1bc42b 100644 --- a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean +++ b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean @@ -289,22 +289,25 @@ if for every point `a : pkg` the filter `f.map (coe⁻¹ (𝓝 a))` obtained by the preimage in `α` of `𝓝 a` tends to `𝓝 (f.extend a : β)`, then the comparison map between `pkg` and `pkg'` composed with the extension of `f` to `pkg`` coincides with the extension of `f` to `pkg'` -/ --- theorem CompareComp_Compare (γ : Type*) [TopologicalSpace γ] extend_compare_extend --- [T3Space γ] (f : α → γ) (cont_f : Continuous f) : --- let _ := pkg.uniformStruct.toTopologicalSpace --- let _ := pkg'.uniformStruct.toTopologicalSpace --- (_ : ∀ a : pkg.space, --- Filter.Tendsto f (Filter.comap pkg.coe (𝓝 a)) (𝓝 ((pkg.denseInducing.extend f) a))) → --- pkg.denseInducing.extend f ∘ pkg'.compare pkg = pkg'.denseInducing.extend f := by --- let _ := pkg'.uniformStruct --- let _ := pkg.uniformStruct --- intro _ _ h --- have : ∀ x : α, (pkg.denseInducing.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x := by --- simp only [Function.comp_apply, compare_coe, DenseInducing.extend_eq _ cont_f, implies_true] --- apply (DenseInducing.extend_unique (AbstractCompletion.denseInducing _) this --- (Continuous.comp _ (uniformContinuous_compare pkg' pkg).continuous )).symm --- apply DenseInducing.continuous_extend --- exact fun a => ⟨(pkg.denseInducing.extend f) a, h a⟩ + +open scoped Topology + +theorem CompareComp_Compare (γ : Type*) [TopologicalSpace γ] + [T3Space γ] (f : α → γ) (cont_f : Continuous f) : + let _ := pkg.uniformStruct.toTopologicalSpace + let _ := pkg'.uniformStruct.toTopologicalSpace + (_ : ∀ a : pkg.space, + Filter.Tendsto f (Filter.comap pkg.coe (𝓝 a)) (𝓝 ((pkg.denseInducing.extend f) a))) → + pkg.denseInducing.extend f ∘ pkg'.compare pkg = pkg'.denseInducing.extend f := by + let _ := pkg'.uniformStruct + let _ := pkg.uniformStruct + intro _ _ h + have : ∀ x : α, (pkg.denseInducing.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x := by + simp only [Function.comp_apply, compare_coe, DenseInducing.extend_eq _ cont_f, implies_true] + apply (DenseInducing.extend_unique (AbstractCompletion.denseInducing _) this + (Continuous.comp _ (uniformContinuous_compare pkg' pkg).continuous )).symm + apply DenseInducing.continuous_extend + exact fun a => ⟨(pkg.denseInducing.extend f) a, h a⟩ end Compare From 65b1c83171ca3c989ca7bfb4df8023bcef642458 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Mon, 20 May 2024 18:31:45 +0200 Subject: [PATCH 5/7] improved doc --- .../Topology/UniformSpace/AbstractCompletion.lean | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean index b90a78ff1bc42b..eaa15d190a3c95 100644 --- a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean +++ b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean @@ -283,12 +283,20 @@ theorem uniformContinuous_compareEquiv_symm : UniformContinuous (pkg.compareEqui pkg'.uniformContinuous_compare pkg #align abstract_completion.uniform_continuous_compare_equiv_symm AbstractCompletion.uniformContinuous_compareEquiv_symm -/-Let `f : α → β` be a continuous function between a uniform space `α` and a regular topological +/-Let `f : α → γ` be a continuous function between a uniform space `α` and a regular topological space `γ`, and let `pkg, pkg'` be two abstract completions of `α`. Then if for every point `a : pkg` the filter `f.map (coe⁻¹ (𝓝 a))` obtained by pushing forward with `f` the preimage in `α` of `𝓝 a` tends to `𝓝 (f.extend a : β)`, then the comparison map between `pkg` and `pkg'` composed with the extension of `f` to `pkg`` coincides with the -extension of `f` to `pkg'` -/ +extension of `f` to `pkg'`: the situation is described in the following diagram, where the +two diagonal arrows are the extensions of `f` to the two different completions `pkg` and `pkg'`: +`α^`=`pkg` ≅ `α^'`=`pkg'` *here `≅` is `compare`* + ∧ \ / + | \ / + | \ / + | V ∨ + α ---f---> γ + -/ open scoped Topology From 85f9e4e34c4e826db73ab9ae0fdbd6bdf2d7ad41 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Mon, 17 Jun 2024 09:49:42 +0200 Subject: [PATCH 6/7] addressed reviewer's comment and improved doc --- .../UniformSpace/AbstractCompletion.lean | 26 ++++++++++--------- 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean index f7dd4d161c274f..405cd45b94a7a8 100644 --- a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean +++ b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean @@ -282,13 +282,18 @@ theorem uniformContinuous_compareEquiv_symm : UniformContinuous (pkg.compareEqui pkg'.uniformContinuous_compare pkg #align abstract_completion.uniform_continuous_compare_equiv_symm AbstractCompletion.uniformContinuous_compareEquiv_symm + +open scoped Topology + /-Let `f : α → γ` be a continuous function between a uniform space `α` and a regular topological space `γ`, and let `pkg, pkg'` be two abstract completions of `α`. Then if for every point `a : pkg` the filter `f.map (coe⁻¹ (𝓝 a))` obtained by pushing forward with `f` the preimage in `α` of `𝓝 a` tends to `𝓝 (f.extend a : β)`, then the comparison map between `pkg` and `pkg'` composed with the extension of `f` to `pkg`` coincides with the -extension of `f` to `pkg'`: the situation is described in the following diagram, where the -two diagonal arrows are the extensions of `f` to the two different completions `pkg` and `pkg'`: +extension of `f` to `pkg'`. The situation is described in the following diagram, where the +two diagonal arrows are the extensions of `f` to the two different completions `pkg` and `pkg'`; +the statement of `compare_comp_eq_compare` is the commutativity of the right triangle. + `α^`=`pkg` ≅ `α^'`=`pkg'` *here `≅` is `compare`* ∧ \ / | \ / @@ -296,20 +301,17 @@ two diagonal arrows are the extensions of `f` to the two different completions ` | V ∨ α ---f---> γ -/ - -open scoped Topology - -theorem CompareComp_Compare (γ : Type*) [TopologicalSpace γ] - [T3Space γ] (f : α → γ) (cont_f : Continuous f) : - let _ := pkg.uniformStruct.toTopologicalSpace - let _ := pkg'.uniformStruct.toTopologicalSpace - (_ : ∀ a : pkg.space, +theorem compare_comp_eq_compare (γ : Type*) [TopologicalSpace γ] + [T3Space γ] {f : α → γ} (cont_f : Continuous f) : + letI := pkg.uniformStruct.toTopologicalSpace + letI := pkg'.uniformStruct.toTopologicalSpace + (∀ a : pkg.space, Filter.Tendsto f (Filter.comap pkg.coe (𝓝 a)) (𝓝 ((pkg.denseInducing.extend f) a))) → pkg.denseInducing.extend f ∘ pkg'.compare pkg = pkg'.denseInducing.extend f := by let _ := pkg'.uniformStruct let _ := pkg.uniformStruct - intro _ _ h - have : ∀ x : α, (pkg.denseInducing.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x := by + intro h + have (x : α) : (pkg.denseInducing.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x := by simp only [Function.comp_apply, compare_coe, DenseInducing.extend_eq _ cont_f, implies_true] apply (DenseInducing.extend_unique (AbstractCompletion.denseInducing _) this (Continuous.comp _ (uniformContinuous_compare pkg' pkg).continuous )).symm From bcf0b5b6d917017eadb567b08984910052ba6458 Mon Sep 17 00:00:00 2001 From: "Filippo A. E. Nuccio" Date: Mon, 15 Jul 2024 19:56:20 +0200 Subject: [PATCH 7/7] Update Mathlib/Topology/UniformSpace/AbstractCompletion.lean Co-authored-by: Patrick Massot --- Mathlib/Topology/UniformSpace/AbstractCompletion.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean index 405cd45b94a7a8..9c97f5c7580559 100644 --- a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean +++ b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean @@ -316,7 +316,7 @@ theorem compare_comp_eq_compare (γ : Type*) [TopologicalSpace γ] apply (DenseInducing.extend_unique (AbstractCompletion.denseInducing _) this (Continuous.comp _ (uniformContinuous_compare pkg' pkg).continuous )).symm apply DenseInducing.continuous_extend - exact fun a => ⟨(pkg.denseInducing.extend f) a, h a⟩ + exact fun a ↦ ⟨(pkg.denseInducing.extend f) a, h a⟩ end Compare