Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
  • Loading branch information
Parcly-Taxel authored and semorrison committed Jun 23, 2023
1 parent fada7dc commit 7687a27
Show file tree
Hide file tree
Showing 3 changed files with 67 additions and 4 deletions.
16 changes: 15 additions & 1 deletion Mathlib/Geometry/Manifold/ChartedSpace.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel
! This file was ported from Lean 3 source module geometry.manifold.charted_space
! leanprover-community/mathlib commit bcfa726826abd57587355b4b5b7e78ad6527b7e4
! leanprover-community/mathlib commit 431589bce478b2229eba14b14a283250428217db
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
Expand Down Expand Up @@ -1080,6 +1080,20 @@ protected instance instHasGroupoid [ClosedUnderRestriction G] : HasGroupoid s G
· exact preimage_open_of_open_symm (chartAt _ _) s.2
#align topological_space.opens.has_groupoid TopologicalSpace.Opens.instHasGroupoid

theorem chartAt_inclusion_symm_eventuallyEq {U V : Opens M} (hUV : U ≤ V) {x : U} :
(chartAt H (Set.inclusion hUV x)).symm
=ᶠ[𝓝 (chartAt H (Set.inclusion hUV x) (Set.inclusion hUV x))]
Set.inclusion hUV ∘ (chartAt H x).symm := by
set i := Set.inclusion hUV
set e := chartAt H (x : M)
haveI : Nonempty U := ⟨x⟩
haveI : Nonempty V := ⟨i x⟩
have heUx_nhds : (e.subtypeRestr U).target ∈ 𝓝 (e x) := by
apply (e.subtypeRestr U).open_target.mem_nhds
exact e.map_subtype_source (mem_chart_source _ _)
exact Filter.eventuallyEq_of_mem heUx_nhds (e.subtypeRestr_symm_eqOn_of_le hUV)
#align topological_space.opens.chart_at_inclusion_symm_eventually_eq TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq

end TopologicalSpace.Opens

/-! ### Structomorphisms -/
Expand Down
24 changes: 22 additions & 2 deletions Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel, Floris van Doorn
! This file was ported from Lean 3 source module geometry.manifold.local_invariant_properties
! leanprover-community/mathlib commit be2c24f56783935652cefffb4bfca7e4b25d167e
! leanprover-community/mathlib commit 431589bce478b2229eba14b14a283250428217db
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
Expand Down Expand Up @@ -52,7 +52,7 @@ noncomputable section

open Classical Manifold Topology

open Set Filter
open Set Filter TopologicalSpace

variable {H M H' M' X : Type _}

Expand Down Expand Up @@ -545,6 +545,26 @@ theorem liftProp_id (hG : G.LocalInvariantProp G Q) (hQ : ∀ y, Q id univ y) :
exact fun x ↦ hG.congr' ((chartAt H x).eventually_right_inverse <| mem_chart_target H x) (hQ _)
#align structure_groupoid.local_invariant_prop.lift_prop_id StructureGroupoid.LocalInvariantProp.liftProp_id

theorem liftPropAt_iff_comp_inclusion (hG : LocalInvariantProp G G' P) {U V : Opens M} (hUV : U ≤ V)
(f : V → M') (x : U) :
LiftPropAt P f (Set.inclusion hUV x) ↔ LiftPropAt P (f ∘ Set.inclusion hUV : U → M') x := by
change (_ ∧ _) ↔ (_ ∧ _); congr! 1 -- Porting note: was `congrm _ ∧ _`
· simp [continuousWithinAt_univ,
(TopologicalSpace.Opens.openEmbedding_of_le hUV).continuousAt_iff]
· apply hG.congr_iff
exact (TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq hUV).fun_comp
(chartAt H' (f (Set.inclusion hUV x)) ∘ f)
#align structure_groupoid.local_invariant_prop.lift_prop_at_iff_comp_inclusion StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion

theorem liftProp_inclusion {Q : (H → H) → Set H → H → Prop} (hG : LocalInvariantProp G G Q)
(hQ : ∀ y, Q id univ y) {U V : Opens M} (hUV : U ≤ V) :
LiftProp Q (Set.inclusion hUV : U → V) := by
intro x
show LiftPropAt Q (id ∘ inclusion hUV) x
rw [← hG.liftPropAt_iff_comp_inclusion hUV]
apply hG.liftProp_id hQ
#align structure_groupoid.local_invariant_prop.lift_prop_inclusion StructureGroupoid.LocalInvariantProp.liftProp_inclusion

end LocalInvariantProp

section LocalStructomorph
Expand Down
31 changes: 30 additions & 1 deletion Mathlib/Topology/LocalHomeomorph.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel
! This file was ported from Lean 3 source module topology.local_homeomorph
! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988
! leanprover-community/mathlib commit 431589bce478b2229eba14b14a283250428217db
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
Expand Down Expand Up @@ -1379,6 +1379,16 @@ theorem subtypeRestr_source : (e.subtypeRestr s).source = (↑) ⁻¹' e.source
simp only [subtypeRestr_def, mfld_simps]
#align local_homeomorph.subtype_restr_source LocalHomeomorph.subtypeRestr_source

variable {s}

theorem map_subtype_source {x : s} (hxe : (x : α) ∈ e.source): e x ∈ (e.subtypeRestr s).target := by
refine' ⟨e.map_source hxe, _⟩
rw [s.localHomeomorphSubtypeCoe_target, mem_preimage, e.leftInvOn hxe]
exact x.prop
#align local_homeomorph.map_subtype_source LocalHomeomorph.map_subtype_source

variable (s)

/- This lemma characterizes the transition functions of an open subset in terms of the transition
functions of the original space. -/
theorem subtypeRestr_symm_trans_subtypeRestr (f f' : LocalHomeomorph α β) :
Expand All @@ -1399,4 +1409,23 @@ theorem subtypeRestr_symm_trans_subtypeRestr (f f' : LocalHomeomorph α β) :
simp only [mfld_simps, Setoid.refl]
#align local_homeomorph.subtype_restr_symm_trans_subtype_restr LocalHomeomorph.subtypeRestr_symm_trans_subtypeRestr

theorem subtypeRestr_symm_eqOn_of_le {U V : Opens α} [Nonempty U] [Nonempty V] (hUV : U ≤ V) :
EqOn (e.subtypeRestr V).symm (Set.inclusion hUV ∘ (e.subtypeRestr U).symm)
(e.subtypeRestr U).target := by
set i := Set.inclusion hUV
intro y hy
dsimp [LocalHomeomorph.subtypeRestr_def] at hy ⊢
have hyV : e.symm y ∈ V.localHomeomorphSubtypeCoe.target := by
rw [Opens.localHomeomorphSubtypeCoe_target] at hy ⊢
exact hUV hy.2
refine' V.localHomeomorphSubtypeCoe.injOn _ trivial _
· rw [← LocalHomeomorph.symm_target]
apply LocalHomeomorph.map_source
rw [LocalHomeomorph.symm_source]
exact hyV
· rw [V.localHomeomorphSubtypeCoe.right_inv hyV]
show _ = U.localHomeomorphSubtypeCoe _
rw [U.localHomeomorphSubtypeCoe.right_inv hy.2]
#align local_homeomorph.subtype_restr_symm_eq_on_of_le LocalHomeomorph.subtypeRestr_symm_eqOn_of_le

end LocalHomeomorph

0 comments on commit 7687a27

Please sign in to comment.