From a310a89b3b6adc75dcde4df238382a90c1888d6c Mon Sep 17 00:00:00 2001 From: Winston Yin Date: Fri, 5 Jan 2024 09:42:52 +0000 Subject: [PATCH 1/3] feat: Boundaryless manifold (#9323) This is a more general notion of boundaryless manifold than `ModelWithCorners.Boundaryless`, which requires the `ModelWithCorners` to map to the whole model vector space. To justify this new type class, consider the interior of a manifold with non-empty boundary. It inherits a manifold structure via its embedding, and it would be convenient to use the same `ModelWithCorners` for the interior as for the whole space. Even though the interior is boundaryless, its inherited `ModelWithCorners` doesn't satisfy `ModelWithCorners.Boundaryless`. --- .../Geometry/Manifold/InteriorBoundary.lean | 41 +++++++++++++------ .../Manifold/SmoothManifoldWithCorners.lean | 4 +- 2 files changed, 32 insertions(+), 13 deletions(-) diff --git a/Mathlib/Geometry/Manifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/InteriorBoundary.lean index e8f1d22de97be..970413b2edd42 100644 --- a/Mathlib/Geometry/Manifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/InteriorBoundary.lean @@ -103,25 +103,42 @@ lemma _root_.range_mem_nhds_isInteriorPoint {x : M} (h : I.IsInteriorPoint x) : rw [mem_nhds_iff] exact ⟨interior (range I), interior_subset, isOpen_interior, h⟩ -section boundaryless +/-- Type class for manifold without boundary. This differs from `ModelWithCorners.Boundaryless`, + which states that the `ModelWithCorners` maps to the whole model vector space. -/ +class _root_.BoundarylessManifold {𝕜 : Type*} [NontriviallyNormedField 𝕜] + {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] + {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) + (M : Type*) [TopologicalSpace M] [ChartedSpace H M] : Prop where + isInteriorPoint' : ∀ x : M, IsInteriorPoint I x + +section Boundaryless variable [I.Boundaryless] -/-- If `I` is boundaryless, every point of `M` is an interior point. -/ -lemma isInteriorPoint {x : M} : I.IsInteriorPoint x := by - let r := ((chartAt H x).isOpen_extend_target I).interior_eq - have : extChartAt I x = (chartAt H x).extend I := rfl - rw [← this] at r - rw [ModelWithCorners.isInteriorPoint_iff, r] - exact PartialEquiv.map_source _ (mem_extChartAt_source _ _) +/-- Boundaryless `ModelWithCorners` implies boundaryless manifold. -/ +instance : BoundarylessManifold I M where + isInteriorPoint' x := by + let r := ((chartAt H x).isOpen_extend_target I).interior_eq + have : extChartAt I x = (chartAt H x).extend I := rfl + rw [← this] at r + rw [ModelWithCorners.isInteriorPoint_iff, r] + exact PartialEquiv.map_source _ (mem_extChartAt_source _ _) -/-- If `I` is boundaryless, `M` has full interior. -/ +end Boundaryless + +section BoundarylessManifold +variable [BoundarylessManifold I M] + +lemma _root_.BoundarylessManifold.isInteriorPoint {x : M} : + IsInteriorPoint I x := BoundarylessManifold.isInteriorPoint' x + +/-- Boundaryless manifolds have full interior. -/ lemma interior_eq_univ : I.interior M = univ := by ext - refine ⟨fun _ ↦ trivial, fun _ ↦ I.isInteriorPoint⟩ + refine ⟨fun _ ↦ trivial, fun _ ↦ BoundarylessManifold.isInteriorPoint I⟩ -/-- If `I` is boundaryless, `M` has empty boundary. -/ +/-- Boundaryless manifolds have empty boundary. -/ lemma Boundaryless.boundary_eq_empty : I.boundary M = ∅ := by rw [I.boundary_eq_complement_interior, I.interior_eq_univ, compl_empty_iff] -end boundaryless +end BoundarylessManifold end ModelWithCorners diff --git a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean index 7612e907c11ae..e958357df8faf 100644 --- a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean +++ b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean @@ -478,7 +478,9 @@ end ModelWithCornersProd section Boundaryless -/-- Property ensuring that the model with corners `I` defines manifolds without boundary. -/ +/-- Property ensuring that the model with corners `I` defines manifolds without boundary. This + differs from the more general `BoundarylessManifold`, which requires every point on the manifold + to be an interior point. -/ class ModelWithCorners.Boundaryless {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : Prop where From 4d385393cd569f08ac30425ef886a57bb10daaa5 Mon Sep 17 00:00:00 2001 From: L Date: Fri, 5 Jan 2024 10:17:16 +0000 Subject: [PATCH 2/3] feat: `IndepFun.symm` of different domains (#9425) Co-authored-by: L Lllvvuu --- Mathlib/Probability/Independence/Basic.lean | 7 ++++--- Mathlib/Probability/Independence/Kernel.lean | 7 ++++--- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/Mathlib/Probability/Independence/Basic.lean b/Mathlib/Probability/Independence/Basic.lean index 18a7e4b341b6c..1e461cc0a4f38 100644 --- a/Mathlib/Probability/Independence/Basic.lean +++ b/Mathlib/Probability/Independence/Basic.lean @@ -650,11 +650,12 @@ theorem indepFun_iff_map_prod_eq_prod_map_map {mβ : MeasurableSpace β} {mβ' : rw [(h₀ hs ht).1, (h₀ hs ht).2, h, Measure.prod_prod] @[symm] -nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {f g : Ω → β} (hfg : IndepFun f g μ) : - IndepFun g f μ := hfg.symm +nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {_ : MeasurableSpace β'} + (hfg : IndepFun f g μ) : IndepFun g f μ := hfg.symm #align probability_theory.indep_fun.symm ProbabilityTheory.IndepFun.symm -theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {f g f' g' : Ω → β} (hfg : IndepFun f g μ) +theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} + {f' : Ω → β} {g' : Ω → β'} (hfg : IndepFun f g μ) (hf : f =ᵐ[μ] f') (hg : g =ᵐ[μ] g') : IndepFun f' g' μ := by refine kernel.IndepFun.ae_eq hfg ?_ ?_ <;> simp only [ae_dirac_eq, Filter.eventually_pure, kernel.const_apply] diff --git a/Mathlib/Probability/Independence/Kernel.lean b/Mathlib/Probability/Independence/Kernel.lean index 89457332a0f2f..222525433f5ab 100644 --- a/Mathlib/Probability/Independence/Kernel.lean +++ b/Mathlib/Probability/Independence/Kernel.lean @@ -788,10 +788,11 @@ theorem indepFun_iff_indepSet_preimage {mβ : MeasurableSpace β} {mβ' : Measur · rwa [← indepSet_iff_measure_inter_eq_mul (hf hs) (hg ht) κ μ] @[symm] -nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {f g : Ω → β} (hfg : IndepFun f g κ μ) : - IndepFun g f κ μ := hfg.symm +nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {_ : MeasurableSpace β'} + (hfg : IndepFun f g κ μ) : IndepFun g f κ μ := hfg.symm -theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {f g f' g' : Ω → β} (hfg : IndepFun f g κ μ) +theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} + {f' : Ω → β} {g' : Ω → β'} (hfg : IndepFun f g κ μ) (hf : ∀ᵐ a ∂μ, f =ᵐ[κ a] f') (hg : ∀ᵐ a ∂μ, g =ᵐ[κ a] g') : IndepFun f' g' κ μ := by rintro _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩ From a5346b6b0de2a269b02d7046418916a1ba5e3a86 Mon Sep 17 00:00:00 2001 From: Winston Yin Date: Fri, 5 Jan 2024 10:45:53 +0000 Subject: [PATCH 3/3] chore: rename in `PartialEquiv`, `Homeomorph`, `PartialHomeomorph` (#9430) Items 4-5 in [reference Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Assorted.20renames/near/411096017) Also added `symm` and `trans` definitions for `PartialEquiv`, `Homeomorph`, and `PartialHomeomorph`. --- Mathlib/Geometry/Manifold/ChartedSpace.lean | 6 +++--- Mathlib/Geometry/Manifold/Diffeomorph.lean | 3 ++- .../Manifold/SmoothManifoldWithCorners.lean | 4 ++-- Mathlib/Logic/Equiv/PartialEquiv.lean | 12 +++++++----- Mathlib/Topology/Homeomorph.lean | 2 ++ Mathlib/Topology/PartialHomeomorph.lean | 16 +++++++++------- 6 files changed, 25 insertions(+), 18 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean index e519a641f3a3e..2ad848a4620ec 100644 --- a/Mathlib/Geometry/Manifold/ChartedSpace.lean +++ b/Mathlib/Geometry/Manifold/ChartedSpace.lean @@ -1030,7 +1030,7 @@ theorem StructureGroupoid.compatible_of_mem_maximalAtlas {e e' : PartialHomeomor have D : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s := calc (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e' := by simp only [trans_assoc] _ ≈ e.symm ≫ₕ ofSet f.source f.open_source ≫ₕ e' := - EqOnSource.trans' (refl _) (EqOnSource.trans' (trans_self_symm _) (refl _)) + EqOnSource.trans' (refl _) (EqOnSource.trans' (self_trans_symm _) (refl _)) _ ≈ (e.symm ≫ₕ ofSet f.source f.open_source) ≫ₕ e' := by rw [trans_assoc] _ ≈ e.symm.restr s ≫ₕ e' := by rw [trans_of_set']; apply refl _ ≈ (e.symm ≫ₕ e').restr s := by rw [restr_trans] @@ -1098,7 +1098,7 @@ theorem singleton_hasGroupoid (h : e.source = Set.univ) (G : StructureGroupoid H intro e' e'' he' he'' rw [e.singletonChartedSpace_mem_atlas_eq h e' he', e.singletonChartedSpace_mem_atlas_eq h e'' he''] - refine' G.eq_on_source _ e.trans_symm_self + refine' G.eq_on_source _ e.symm_trans_self have hle : idRestrGroupoid ≤ G := (closedUnderRestriction_iff_id_le G).mp (by assumption) exact StructureGroupoid.le_iff.mp hle _ (idRestrGroupoid_mem _) } #align local_homeomorph.singleton_has_groupoid PartialHomeomorph.singleton_hasGroupoid @@ -1262,7 +1262,7 @@ def Structomorph.trans (e : Structomorph G M M') (e' : Structomorph G M' M'') : F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' := by simp only [trans_assoc, _root_.refl] _ ≈ c.symm ≫ₕ f₁ ≫ₕ ofSet g.source g.open_source ≫ₕ f₂ ≫ₕ c' := EqOnSource.trans' (_root_.refl _) (EqOnSource.trans' (_root_.refl _) - (EqOnSource.trans' (trans_self_symm g) (_root_.refl _))) + (EqOnSource.trans' (self_trans_symm g) (_root_.refl _))) _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source g.open_source) ≫ₕ f₂ ≫ₕ c' := by simp only [trans_assoc, _root_.refl] _ ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c' := by rw [trans_of_set'] diff --git a/Mathlib/Geometry/Manifold/Diffeomorph.lean b/Mathlib/Geometry/Manifold/Diffeomorph.lean index 38875a608ffa6..995a04d616bf6 100644 --- a/Mathlib/Geometry/Manifold/Diffeomorph.lean +++ b/Mathlib/Geometry/Manifold/Diffeomorph.lean @@ -195,6 +195,7 @@ theorem coe_refl : ⇑(Diffeomorph.refl I M n) = id := end /-- Composition of two diffeomorphisms. -/ +@[trans] protected def trans (h₁ : M ≃ₘ^n⟮I, I'⟯ M') (h₂ : M' ≃ₘ^n⟮I', J⟯ N) : M ≃ₘ^n⟮I, J⟯ N where contMDiff_toFun := h₂.contMDiff.comp h₁.contMDiff contMDiff_invFun := h₁.contMDiff_invFun.comp h₂.contMDiff_invFun @@ -217,7 +218,7 @@ theorem coe_trans (h₁ : M ≃ₘ^n⟮I, I'⟯ M') (h₂ : M' ≃ₘ^n⟮I', J #align diffeomorph.coe_trans Diffeomorph.coe_trans /-- Inverse of a diffeomorphism. -/ -@[pp_dot] +@[symm] protected def symm (h : M ≃ₘ^n⟮I, J⟯ N) : N ≃ₘ^n⟮J, I⟯ M where contMDiff_toFun := h.contMDiff_invFun contMDiff_invFun := h.contMDiff_toFun diff --git a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean index e958357df8faf..be615f8a99e15 100644 --- a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean +++ b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean @@ -619,7 +619,7 @@ the `C^n` groupoid. -/ theorem symm_trans_mem_contDiffGroupoid (e : PartialHomeomorph M H) : e.symm.trans e ∈ contDiffGroupoid n I := haveI : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target := - PartialHomeomorph.trans_symm_self _ + PartialHomeomorph.symm_trans_self _ StructureGroupoid.eq_on_source _ (ofSet_mem_contDiffGroupoid n I e.open_target) this #align symm_trans_mem_cont_diff_groupoid symm_trans_mem_contDiffGroupoid @@ -778,7 +778,7 @@ the analytic groupoid. -/ theorem symm_trans_mem_analyticGroupoid (e : PartialHomeomorph M H) : e.symm.trans e ∈ analyticGroupoid I := haveI : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target := - PartialHomeomorph.trans_symm_self _ + PartialHomeomorph.symm_trans_self _ StructureGroupoid.eq_on_source _ (ofSet_mem_analyticGroupoid I e.open_target) this /-- The analytic groupoid is closed under restriction. -/ diff --git a/Mathlib/Logic/Equiv/PartialEquiv.lean b/Mathlib/Logic/Equiv/PartialEquiv.lean index 39ed99c0b3f3a..c3a0d71e6b55d 100644 --- a/Mathlib/Logic/Equiv/PartialEquiv.lean +++ b/Mathlib/Logic/Equiv/PartialEquiv.lean @@ -148,6 +148,7 @@ instance [Inhabited α] [Inhabited β] : Inhabited (PartialEquiv α β) := eqOn_empty _ _⟩⟩ /-- The inverse of a partial equivalence -/ +@[symm] protected def symm : PartialEquiv β α where toFun := e.invFun invFun := e.toFun @@ -689,6 +690,7 @@ protected def trans' (e' : PartialEquiv β γ) (h : e.target = e'.source) : Part /-- Composing two partial equivs, by restricting to the maximal domain where their composition is well defined. -/ +@[trans] protected def trans : PartialEquiv α γ := PartialEquiv.trans' (e.symm.restr e'.source).symm (e'.restr e.target) (inter_comm _ _) #align local_equiv.trans PartialEquiv.trans @@ -896,18 +898,18 @@ theorem EqOnSource.source_inter_preimage_eq {e e' : PartialEquiv α β} (he : e /-- Composition of a partial equivlance and its inverse is equivalent to the restriction of the identity to the source. -/ -theorem trans_self_symm : e.trans e.symm ≈ ofSet e.source := by +theorem self_trans_symm : e.trans e.symm ≈ ofSet e.source := by have A : (e.trans e.symm).source = e.source := by mfld_set_tac refine' ⟨by rw [A, ofSet_source], fun x hx => _⟩ rw [A] at hx simp only [hx, mfld_simps] -#align local_equiv.trans_self_symm PartialEquiv.trans_self_symm +#align local_equiv.self_trans_symm PartialEquiv.self_trans_symm /-- Composition of the inverse of a partial equivalence and this partial equivalence is equivalent to the restriction of the identity to the target. -/ -theorem trans_symm_self : e.symm.trans e ≈ PartialEquiv.ofSet e.target := - trans_self_symm e.symm -#align local_equiv.trans_symm_self PartialEquiv.trans_symm_self +theorem symm_trans_self : e.symm.trans e ≈ PartialEquiv.ofSet e.target := + self_trans_symm e.symm +#align local_equiv.symm_trans_self PartialEquiv.symm_trans_self /-- Two equivalent partial equivs are equal when the source and target are `univ`. -/ theorem eq_of_eqOnSource_univ (e e' : PartialEquiv α β) (h : e ≈ e') (s : e.source = univ) diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean index eab27e4b2cba2..62369062ba06a 100644 --- a/Mathlib/Topology/Homeomorph.lean +++ b/Mathlib/Topology/Homeomorph.lean @@ -74,6 +74,7 @@ protected def empty [IsEmpty X] [IsEmpty Y] : X ≃ₜ Y where __ := Equiv.equivOfIsEmpty X Y /-- Inverse of a homeomorphism. -/ +@[symm] protected def symm (h : X ≃ₜ Y) : Y ≃ₜ X where continuous_toFun := h.continuous_invFun continuous_invFun := h.continuous_toFun @@ -117,6 +118,7 @@ protected def refl (X : Type*) [TopologicalSpace X] : X ≃ₜ X where #align homeomorph.refl Homeomorph.refl /-- Composition of two homeomorphisms. -/ +@[trans] protected def trans (h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) : X ≃ₜ Z where continuous_toFun := h₂.continuous_toFun.comp h₁.continuous_toFun continuous_invFun := h₁.continuous_invFun.comp h₂.continuous_invFun diff --git a/Mathlib/Topology/PartialHomeomorph.lean b/Mathlib/Topology/PartialHomeomorph.lean index d0c6a7b94550f..c290c93085038 100644 --- a/Mathlib/Topology/PartialHomeomorph.lean +++ b/Mathlib/Topology/PartialHomeomorph.lean @@ -76,6 +76,7 @@ instance : CoeFun (PartialHomeomorph α β) fun _ => α → β := ⟨fun e => e.toFun'⟩ /-- The inverse of a partial homeomorphism -/ +@[symm] protected def symm : PartialHomeomorph β α where toPartialEquiv := e.toPartialEquiv.symm open_source := e.open_target @@ -816,6 +817,7 @@ protected def trans' (h : e.target = e'.source) : PartialHomeomorph α γ where /-- Composing two partial homeomorphisms, by restricting to the maximal domain where their composition is well defined. -/ +@[trans] protected def trans : PartialHomeomorph α γ := PartialHomeomorph.trans' (e.symm.restrOpen e'.source e'.open_source).symm (e'.restrOpen e.target e.open_target) (by simp [inter_comm]) @@ -1024,13 +1026,13 @@ theorem Set.EqOn.restr_eqOn_source {e e' : PartialHomeomorph α β} /-- Composition of a partial homeomorphism and its inverse is equivalent to the restriction of the identity to the source -/ -theorem trans_self_symm : e.trans e.symm ≈ PartialHomeomorph.ofSet e.source e.open_source := - PartialEquiv.trans_self_symm _ -#align local_homeomorph.trans_self_symm PartialHomeomorph.trans_self_symm +theorem self_trans_symm : e.trans e.symm ≈ PartialHomeomorph.ofSet e.source e.open_source := + PartialEquiv.self_trans_symm _ +#align local_homeomorph.self_trans_symm PartialHomeomorph.self_trans_symm -theorem trans_symm_self : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target := - e.symm.trans_self_symm -#align local_homeomorph.trans_symm_self PartialHomeomorph.trans_symm_self +theorem symm_trans_self : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target := + e.symm.self_trans_symm +#align local_homeomorph.symm_trans_self PartialHomeomorph.symm_trans_self theorem eq_of_eqOnSource_univ {e e' : PartialHomeomorph α β} (h : e ≈ e') (s : e.source = univ) (t : e.target = univ) : e = e' := @@ -1445,7 +1447,7 @@ theorem subtypeRestr_symm_trans_subtypeRestr (f f' : PartialHomeomorph α β) : rw [ofSet_trans', sets_identity, ← trans_of_set' _ openness₂, trans_assoc] refine' EqOnSource.trans' (eqOnSource_refl _) _ -- f has been eliminated !!! - refine' Setoid.trans (trans_symm_self s.localHomeomorphSubtypeCoe) _ + refine' Setoid.trans (symm_trans_self s.localHomeomorphSubtypeCoe) _ simp only [mfld_simps, Setoid.refl] #align local_homeomorph.subtype_restr_symm_trans_subtype_restr PartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr