Normalization of interval charts

Affine tools for putting interval charts into standard position without changing their sources: an HChart can be rescaled so its target is Iio 1, an OChart so its target is Ioo 0 1, and an OChart with target Ioo 0 1 can be orientation-reversed (x ↦ 1 - x). H-charts cannot be flipped: the closed end at 0 is a boundary point.

noncomputable def OneMfld.NNReal.mulHomeomorph (c : NNReal) (hc : 0 < c) : NNReal ≃ₜ NNReal

Multiplication by a positive constant, as a self-homeomorphism of ℝ≥0.

Equations

• OneMfld.NNReal.mulHomeomorph c hc = { toFun := fun (x : NNReal) => c * x, invFun := fun (y : NNReal) => c⁻¹ * y, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem OneMfld.NNReal.mulHomeomorph_apply (c : NNReal) (hc : 0 < c) (x : NNReal) : (mulHomeomorph c hc) x = c * x

@[simp]

theorem OneMfld.NNReal.mulHomeomorph_symm_apply (c : NNReal) (hc : 0 < c) (y : NNReal) : (mulHomeomorph c hc).symm y = c⁻¹ * y

noncomputable def OneMfld.affineIooOPH (u v : NNReal) (h : u < v) : { e : OpenPartialHomeomorph NNReal NNReal // e.source = Set.Ioo u v ∧ e.target = Set.Ioo 0 1 ∧ ∀ x ∈ Set.Ioo u v, ↑e x = (x - u) / (v - u) }

The affine map x ↦ (x - u) / (v - u), as an OpenPartialHomeomorph ℝ≥0 ℝ≥0 with source Ioo u v and target Ioo 0 1.

Equations

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

def OneMfld.reflectIooOPH : { e : OpenPartialHomeomorph NNReal NNReal // e.source = Set.Ioo 0 1 ∧ e.target = Set.Ioo 0 1 ∧ ∀ x ∈ Set.Ioo 0 1, ↑e x = 1 - x }

The reflection x ↦ 1 - x, as an OpenPartialHomeomorph ℝ≥0 ℝ≥0 with source and target Ioo 0 1.

Equations

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

noncomputable def OneMfld.HChart.rescale {M : Type u_1} [TopologicalSpace M] (a : HChart M) (hne : a.source.Nonempty) : { b : HChart M // b.source = a.source ∧ b.target = Set.Iio 1 ∧ ∃ (v : NNReal), 0 < v ∧ a.target = Set.Iio v ∧ ∀ x ∈ a.source, ↑b.toPartialEquiv x = v⁻¹ * ↑a.toPartialEquiv x }

Rescale an HChart so its target is Iio 1, without changing its source.

Equations

• a.rescale hne = ⟨{ toOpenPartialHomeomorph := a.transHomeomorph (OneMfld.NNReal.mulHomeomorph ⋯.choose⁻¹ ⋯), target_iio := ⋯ }, ⋯⟩

noncomputable def OneMfld.OChart.rescale {M : Type u_1} [TopologicalSpace M] (a : OChart M) (hne : a.source.Nonempty) : { b : OChart M // b.source = a.source ∧ b.target = Set.Ioo 0 1 ∧ ∃ (u : NNReal) (v : NNReal), u < v ∧ a.target = Set.Ioo u v ∧ ∀ x ∈ a.source, ↑b.toPartialEquiv x = (↑a.toPartialEquiv x - u) / (v - u) }

Rescale an OChart so its target is Ioo 0 1, without changing its source.

Equations

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

def OneMfld.OChart.flip {M : Type u_1} [TopologicalSpace M] (a : OChart M) (h01 : a.target = Set.Ioo 0 1) : { b : OChart M // b.source = a.source ∧ b.target = Set.Ioo 0 1 ∧ ∀ x ∈ a.source, ↑b.toPartialEquiv x = 1 - ↑a.toPartialEquiv x }

Reverse the orientation of an OChart with target Ioo 0 1, without changing its source.

Equations

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