Radial extension of circle homeomorphisms

Every PolygonCell n has the closed unit disk as its carrier. This file implements the radial extension (Alexander trick) of a homeomorphism of the unit circle. The extension preserves the norm exactly, is continuous at the origin by that norm identity, and restricts to the selected circle homeomorphism on the boundary.

The side-count indices of the source and target cells are independent phantom parameters. A later boundary reparameterization only needs to construct a circle homeomorphism with the desired action on marked arcs; PolygonCell.radialHomeomorph then supplies the disk homeomorphism.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Circle.direction (z : ℂ) (hz : z ≠ 0) : Circle

The direction of a nonzero complex number as a point of the unit circle.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Circle.direction z hz = ⟨z / ↑‖z‖, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Circle.coe_direction (z : ℂ) (hz : z ≠ 0) : ↑(direction z hz) = z / ↑‖z‖

theorem LeanEval.Topology.ClassificationOfSurfaces.Circle.continuous_direction : Continuous fun (w : { w : ℂ // w ≠ 0 }) => direction ↑w ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Circle.radialMap (h : Circle ≃ₜ Circle) (z : ℂ) : ℂ

Radially extend a circle homeomorphism to the complex plane, fixing the origin.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Circle.radialMap h z = if hz : z = 0 then 0 else ↑‖z‖ * ↑(h (LeanEval.Topology.ClassificationOfSurfaces.Circle.direction z hz))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Circle.radialMap_zero (h : Circle ≃ₜ Circle) : radialMap h 0 = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Circle.radialMap_of_ne (h : Circle ≃ₜ Circle) {z : ℂ} (hz : z ≠ 0) : radialMap h z = ↑‖z‖ * ↑(h (direction z hz))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Circle.norm_radialMap (h : Circle ≃ₜ Circle) (z : ℂ) : ‖radialMap h z‖ = ‖z‖

Radial extension preserves distance from the origin exactly.

theorem LeanEval.Topology.ClassificationOfSurfaces.Circle.radialMap_ne_zero (h : Circle ≃ₜ Circle) {z : ℂ} (hz : z ≠ 0) : radialMap h z ≠ 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Circle.direction_radialMap (h : Circle ≃ₜ Circle) {z : ℂ} (hz : z ≠ 0) : direction (radialMap h z) ⋯ = h (direction z hz)

The direction of a radial image is the selected image direction.

theorem LeanEval.Topology.ClassificationOfSurfaces.Circle.radialMap_symm_apply (h : Circle ≃ₜ Circle) (z : ℂ) : radialMap h.symm (radialMap h z) = z

Extending the inverse circle homeomorphism gives the inverse radial map.

theorem LeanEval.Topology.ClassificationOfSurfaces.Circle.continuousAt_radialMap_zero (h : Circle ≃ₜ Circle) : ContinuousAt (radialMap h) 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Circle.continuousAt_radialMap_of_ne (h : Circle ≃ₜ Circle) {z : ℂ} (hz : z ≠ 0) : ContinuousAt (radialMap h) z

theorem LeanEval.Topology.ClassificationOfSurfaces.Circle.continuous_radialMap (h : Circle ≃ₜ Circle) : Continuous (radialMap h)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Circle.radialMap_coe (h : Circle ≃ₜ Circle) (z : Circle) : radialMap h ↑z = ↑(h z)

On the unit circle, radial extension is exactly the original homeomorphism.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.radialHomeomorph {n m : ℕ} (h : Circle ≃ₜ Circle) : PolygonCell n ≃ₜ PolygonCell m

Radially extend a circle homeomorphism between closed polygon-cell carriers.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.radialHomeomorph_apply_val {n m : ℕ} (h : Circle ≃ₜ Circle) (z : PolygonCell n) : ((radialHomeomorph h) z).val = Circle.radialMap h z.val

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.radialHomeomorph_ofCircle {n m : ℕ} (h : Circle ≃ₜ Circle) (z : Circle) : (radialHomeomorph h) ((ofCircle n) z) = (ofCircle m) (h z)

The radial cell homeomorphism restricts to the selected circle homeomorphism.