Documentation

LeanPool.ClassificationOfSurfaces.Moise.NoRetraction

The disk has no retraction onto its boundary #

This is Moise, Chapter 4, Problem 2 (proved as Theorem 10.10 later in the book). We use the covering map Circle.exp : ℝ → S¹: a map from the contractible closed disk to the circle lifts to ℝ, whereas its restriction to the boundary cannot be the identity because the standard boundary loop has lifts whose endpoints differ by 2π.

source
@[reducible, inline]
abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.ClosedUnitDisk :
Set ℂ

The complex closed unit disk, used only as the standard model for the no-retraction argument.

Equations
Instances For
    source
    def LeanEval.Topology.ClassificationOfSurfaces.Moise.circleToClosedUnitDisk (z : Circle) :
    ↑ClosedUnitDisk

    The boundary circle included in the closed unit disk.

    Equations
    Instances For
      source
      @[simp]
      theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.circleToClosedUnitDisk_coe (z : Circle) :
      ↑(circleToClosedUnitDisk z) = ↑z
      source
      theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.continuous_circleToClosedUnitDisk :
      Continuous circleToClosedUnitDisk
      source
      theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.no_retraction_closedUnitDisk :
      ¬∃ (r : ↑ClosedUnitDisk → Circle), Continuous r ∧ ∀ (z : Circle), r (circleToClosedUnitDisk z) = z

      The closed disk does not retract continuously onto its boundary circle.

      source
      @[reducible, inline]
      noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.planeComplexIsometry :
      Plane ≃ₗᵢ[ℝ] ℂ

      The Euclidean plane and the complex plane are linearly isometric, using the orthonormal basis (1, I) of ℂ over ℝ.

      Equations
      Instances For
        source
        noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.circleToPlaneClosedUnitBall (z : Circle) :
        ↑(Metric.closedBall 0 1)

        A complex unit direction, transported to the Euclidean plane, lies in the plane unit ball.

        Equations
        Instances For
          source
          noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.planeUnitSphereToCircle (x : ↑(Metric.sphere 0 1)) :
          Circle

          A point on the Euclidean unit sphere, transported to ℂ, is a point of Circle.

          Equations
          Instances For
            source
            @[simp]
            theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.planeUnitSphereToCircle_circleToPlaneClosedUnitBall (z : Circle) :
            planeUnitSphereToCircle ⟨↑(circleToPlaneClosedUnitBall z), ⋯⟩ = z
            source
            theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.continuous_circleToPlaneClosedUnitBall :
            Continuous circleToPlaneClosedUnitBall
            source
            theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.continuous_planeUnitSphereToCircle :
            Continuous planeUnitSphereToCircle
            source
            noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.complexDiskToPlaneClosedUnitBall (z : ↑ClosedUnitDisk) :
            ↑(Metric.closedBall 0 1)

            The linear isometry sends the complex unit disk to the plane unit ball.

            Equations
            Instances For
              source
              theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.continuous_complexDiskToPlaneClosedUnitBall :
              Continuous complexDiskToPlaneClosedUnitBall
              source
              theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.no_retraction_planeClosedUnitBall :
              ¬∃ (r : ↑(Metric.closedBall 0 1) → ↑(Metric.sphere 0 1)), Continuous r ∧ ∀ (z : ↑(Metric.sphere 0 1)), r ⟨↑z, ⋯⟩ = z

              The closed unit ball in the project's Euclidean plane does not retract onto its sphere.

              source
              theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.no_retraction_of_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {A B : Set X} {A' B' : Set Y} (e : X ≃ₜ Y) (hA : ⇑e '' A = A') (hB : ⇑e '' B = B') (hBA : B ⊆ A) (hB'A' : B' ⊆ A') (hno : ¬∃ (r : ↑A' → ↑B'), Continuous r ∧ ∀ (z : ↑B'), r ⟨↑z, ⋯⟩ = z) :
              ¬∃ (r : ↑A → ↑B), Continuous r ∧ ∀ (z : ↑B), r ⟨↑z, ⋯⟩ = z

              Retractions are invariant under an ambient homeomorphism carrying both the disk and its boundary to the target disk and boundary.

              source
              theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IsTriangle.no_retraction {C : Set Plane} (hC : IsTriangle C) :
              ¬∃ (r : ↑C → ↑(frontier C)), Continuous r ∧ ∀ (z : ↑(frontier C)), r ⟨↑z, ⋯⟩ = z

              A nondegenerate closed plane triangle has no continuous retraction onto its frontier.

              source
              theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_radial_retraction_to_frontier {C : Set Plane} (hconvex : Convex ℝ C) (hbounded : Bornology.IsBounded C) {q : Plane} (hq : q ∈ interior C) :
              ∃ (R : { x : Plane // x ≠ q } → ↑(frontier C)), Continuous R ∧ ∀ (x : ↑(frontier C)), R ⟨↑x, ⋯⟩ = x

              Radial projection from an interior point of a bounded convex plane set retracts the punctured plane onto the set's frontier. The Minkowski gauge supplies the distance to the frontier along each ray.