Constructions for open partial homeomorphisms

An open partial homeomorphism restricts to a chart on a subtype when membership in the subtype is detected by a parametrized coordinate slice. This file packages that topological construction; zero-slice subgroup charts use it after translating an ambient chart. Continuous maps that are inverse on open sets also give an open partial homeomorphism on their mutual restrictions (ContinuousOn.toOpenPartialHomeomorph).

Main definitions

• ContinuousOn.toOpenPartialHomeomorph constructs an open partial homeomorphism from continuous maps inverse on their mutual restrictions.

• OpenPartialHomeomorph.subtypeCoord restricts an open partial homeomorphism to a subtype and reads its coordinates through a retraction onto the parametrized slice.

References

This construction abstracts the concrete subtype charts in the following Tau Ceti formalizations:

• boundaryChart in TauCeti/Geometry/Manifold/Boundary/Charts.lean.
• TauCeti.levelSetChart in TauCeti/Analysis/Fredholm/LevelSet/Basic.lean.

noncomputable def OpenPartialHomeomorph.subtypeCoord {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : Nonempty ↑s) (ι : Z → Y) (π : Y → Z) (hι : ∀ {z : Z}, ι z ∈ e.target → ↑e.symm (ι z) ∈ s) (hslice : ∀ {x : X}, x ∈ e.source → x ∈ s → ι (π (↑e x)) = ↑e x) (hπι : Set.LeftInvOn π ι (ι ⁻¹' e.target)) (hιc : Continuous ι) (hπc : ContinuousOn π (e.target ∩ Set.range ι)) : OpenPartialHomeomorph (↑s) Z

Restrict an open partial homeomorphism to a subtype represented by a parametrized coordinate slice.

The map ι : Z → Y parametrizes the slice and π : Y → Z reads its coordinates. The hypotheses say that ambient inverse images of slice points belong to s, that points of s visible in the source lie on the slice, and that π is a left inverse of ι wherever the slice meets the target. Only continuity of π where the parametrized slice meets the target is needed. Outside the target, the inverse uses the canonical choice supplied by Nonempty s; its value there is irrelevant to an open partial homeomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OpenPartialHomeomorph.subtypeCoord_source {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : Nonempty ↑s) (ι : Z → Y) (π : Y → Z) (hι : ∀ {z : Z}, ι z ∈ e.target → ↑e.symm (ι z) ∈ s) (hslice : ∀ {x : X}, x ∈ e.source → x ∈ s → ι (π (↑e x)) = ↑e x) (hπι : Set.LeftInvOn π ι (ι ⁻¹' e.target)) (hιc : Continuous ι) (hπc : ContinuousOn π (e.target ∩ Set.range ι)) : (e.subtypeCoord s hs ι π ⋯ ⋯ hπι hιc hπc).source = Subtype.val ⁻¹' e.source

The source of subtypeCoord is the part of the subtype in the ambient source.

@[simp]

theorem OpenPartialHomeomorph.subtypeCoord_target {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : Nonempty ↑s) (ι : Z → Y) (π : Y → Z) (hι : ∀ {z : Z}, ι z ∈ e.target → ↑e.symm (ι z) ∈ s) (hslice : ∀ {x : X}, x ∈ e.source → x ∈ s → ι (π (↑e x)) = ↑e x) (hπι : Set.LeftInvOn π ι (ι ⁻¹' e.target)) (hιc : Continuous ι) (hπc : ContinuousOn π (e.target ∩ Set.range ι)) : (e.subtypeCoord s hs ι π ⋯ ⋯ hπι hιc hπc).target = ι ⁻¹' e.target

The target of subtypeCoord is the preimage of the ambient target under the slice parametrization.

@[simp]

theorem OpenPartialHomeomorph.subtypeCoord_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : Nonempty ↑s) (ι : Z → Y) (π : Y → Z) (hι : ∀ {z : Z}, ι z ∈ e.target → ↑e.symm (ι z) ∈ s) (hslice : ∀ {x : X}, x ∈ e.source → x ∈ s → ι (π (↑e x)) = ↑e x) (hπι : Set.LeftInvOn π ι (ι ⁻¹' e.target)) (hιc : Continuous ι) (hπc : ContinuousOn π (e.target ∩ Set.range ι)) (x : ↑s) : ↑(e.subtypeCoord s hs ι π ⋯ ⋯ hπι hιc hπc) x = π (↑e ↑x)

subtypeCoord reads a subtype point using the ambient map followed by the coordinate retraction.

theorem OpenPartialHomeomorph.subtypeCoord_parametrization_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : Nonempty ↑s) (ι : Z → Y) (π : Y → Z) (hι : ∀ {z : Z}, ι z ∈ e.target → ↑e.symm (ι z) ∈ s) (hslice : ∀ {x : X}, x ∈ e.source → x ∈ s → ι (π (↑e x)) = ↑e x) (hπι : Set.LeftInvOn π ι (ι ⁻¹' e.target)) (hιc : Continuous ι) (hπc : ContinuousOn π (e.target ∩ Set.range ι)) {x : ↑s} (hx : x ∈ (e.subtypeCoord s hs ι π ⋯ ⋯ hπι hιc hπc).source) : ι (↑(e.subtypeCoord s hs ι π ⋯ ⋯ hπι hιc hπc) x) = ↑e ↑x

On its source, subtypeCoord recovers the ambient coordinate after applying the slice parametrization.

@[simp]

theorem OpenPartialHomeomorph.coe_subtypeCoord_symm_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : Nonempty ↑s) (ι : Z → Y) (π : Y → Z) (hι : ∀ {z : Z}, ι z ∈ e.target → ↑e.symm (ι z) ∈ s) (hslice : ∀ {x : X}, x ∈ e.source → x ∈ s → ι (π (↑e x)) = ↑e x) (hπι : Set.LeftInvOn π ι (ι ⁻¹' e.target)) (hιc : Continuous ι) (hπc : ContinuousOn π (e.target ∩ Set.range ι)) {z : Z} (hz : ι z ∈ e.target) : ↑(↑(e.subtypeCoord s hs ι π ⋯ ⋯ hπι hιc hπc).symm z) = ↑e.symm (ι z)

On its target, the inverse of subtypeCoord is the ambient inverse evaluated on the parametrized slice.

def ContinuousOn.toOpenPartialHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {g : Y → X} {U : Set X} {V : Set Y} (hf : ContinuousOn f U) (hg : ContinuousOn g V) (hU : IsOpen U) (hV : IsOpen V) (hgf : Set.LeftInvOn g f (U ∩ f ⁻¹' V)) (hfg : Set.RightInvOn g f (V ∩ g ⁻¹' U)) : OpenPartialHomeomorph X Y

Continuous maps on open sets define an open partial homeomorphism if they are inverse on points whose images lie in the other set. The forward and inverse maps are the given maps, and the source and target are exactly these mutual restrictions.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousOn.coe_toOpenPartialHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {g : Y → X} {U : Set X} {V : Set Y} (hf : ContinuousOn f U) (hg : ContinuousOn g V) (hU : IsOpen U) (hV : IsOpen V) (hgf : Set.LeftInvOn g f (U ∩ f ⁻¹' V)) (hfg : Set.RightInvOn g f (V ∩ g ⁻¹' U)) : ↑(hf.toOpenPartialHomeomorph hg hU hV hgf hfg) = f

The forward map of toOpenPartialHomeomorph is the given map.

@[simp]

theorem ContinuousOn.coe_toOpenPartialHomeomorph_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {g : Y → X} {U : Set X} {V : Set Y} (hf : ContinuousOn f U) (hg : ContinuousOn g V) (hU : IsOpen U) (hV : IsOpen V) (hgf : Set.LeftInvOn g f (U ∩ f ⁻¹' V)) (hfg : Set.RightInvOn g f (V ∩ g ⁻¹' U)) : ↑(hf.toOpenPartialHomeomorph hg hU hV hgf hfg).symm = g

The inverse map of toOpenPartialHomeomorph is the given inverse.

@[simp]

theorem ContinuousOn.toOpenPartialHomeomorph_source {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {g : Y → X} {U : Set X} {V : Set Y} (hf : ContinuousOn f U) (hg : ContinuousOn g V) (hU : IsOpen U) (hV : IsOpen V) (hgf : Set.LeftInvOn g f (U ∩ f ⁻¹' V)) (hfg : Set.RightInvOn g f (V ∩ g ⁻¹' U)) : (hf.toOpenPartialHomeomorph hg hU hV hgf hfg).source = U ∩ f ⁻¹' V

The source of toOpenPartialHomeomorph consists of points of U mapped into V.

@[simp]

theorem ContinuousOn.toOpenPartialHomeomorph_target {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {g : Y → X} {U : Set X} {V : Set Y} (hf : ContinuousOn f U) (hg : ContinuousOn g V) (hU : IsOpen U) (hV : IsOpen V) (hgf : Set.LeftInvOn g f (U ∩ f ⁻¹' V)) (hfg : Set.RightInvOn g f (V ∩ g ⁻¹' U)) : (hf.toOpenPartialHomeomorph hg hU hV hgf hfg).target = V ∩ g ⁻¹' U

The target of toOpenPartialHomeomorph consists of points of V mapped into U.