Hemisphere maps for the two-monogon sphere

This file maps the two disk faces of SurfaceCellComplex.sphere to the upper and lower unit hemispheres. The lower face uses complex conjugation, so the existing opposite-direction monogon pairing has identical images.

The two possible directed sphere identifications are classified explicitly. The resulting continuous facewise map on the polygonal pre-realization respects every raw gluing generator. SphereQuotientHomeomorph descends this map and proves that it is a homeomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.normSq_le_one {n : ℕ} (z : PolygonCell n) : Complex.normSq z.val ≤ 1

The squared radius of a point in an indexed polygon cell is at most one.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.hemisphereHeight {n : ℕ} (z : PolygonCell n) : ℝ

The nonnegative height above the equatorial plane associated to a disk point.

Equations

• z.hemisphereHeight = √(1 - Complex.normSq z.val)

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.hemisphereHeight_nonneg {n : ℕ} (z : PolygonCell n) : 0 ≤ z.hemisphereHeight

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.hemisphereHeight_sq {n : ℕ} (z : PolygonCell n) : z.hemisphereHeight ^ 2 = 1 - Complex.normSq z.val

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.continuous_hemisphereHeight {n : ℕ} : Continuous hemisphereHeight

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.upperHemisphereVector (z : PolygonCell 1) : EuclideanSpace ℝ (Fin 3)

A disk point placed on the upper unit hemisphere.

Equations

• z.upperHemisphereVector = !₂[z.val.re, z.val.im, z.hemisphereHeight]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.lowerHemisphereVector (z : PolygonCell 1) : EuclideanSpace ℝ (Fin 3)

A conjugated disk point placed on the lower unit hemisphere.

Equations

• z.lowerHemisphereVector = !₂[((starRingEnd ℂ) z.val).re, ((starRingEnd ℂ) z.val).im, -z.hemisphereHeight]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.upperHemisphereVector_norm (z : PolygonCell 1) : ‖z.upperHemisphereVector‖ = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.lowerHemisphereVector_norm (z : PolygonCell 1) : ‖z.lowerHemisphereVector‖ = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.continuous_upperHemisphereVector : Continuous upperHemisphereVector

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.continuous_lowerHemisphereVector : Continuous lowerHemisphereVector

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.upperHemisphere : C(PolygonCell 1, SphereRepresentative)

The continuous map from a monogon disk to the upper unit hemisphere.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.lowerHemisphere : C(PolygonCell 1, SphereRepresentative)

The continuous map from a monogon disk to the lower unit hemisphere.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.hemisphereHeight_side_monogon (t : ↑unitInterval) : ((side 0) t).hemisphereHeight = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.upperHemisphere_side_eq_lowerHemisphere_side_symm (t : ↑unitInterval) : upperHemisphere ((side 0) t) = lowerHemisphere ((side 0) (unitInterval.symm t))

The positive-to-negative monogon pairing has the same upper and lower hemisphere image.

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.lowerHemisphere_side_eq_upperHemisphere_side_symm (t : ↑unitInterval) : lowerHemisphere ((side 0) t) = upperHemisphere ((side 0) (unitInterval.symm t))

The swapped monogon pairing has the same lower and upper hemisphere image.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereBoundaryOccurrence_eq (occurrence : sphere.BoundaryOccurrence) : occurrence = spherePositiveOccurrence ∨ occurrence = sphereNegativeOccurrence

Every boundary occurrence of the sphere is one of its two monogon occurrences.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.mem_sphere_polygonalIdentifications_iff (identification : PolygonGluing.Identification sphere.Face sphere.faceBoundaryLength) : identification ∈ sphere.polygonalIdentifications sphere_occurrencePairingValid ↔ identification = sphereBoundaryPairing.identification ∨ identification = swapIdentification sphereBoundaryPairing.identification

The two directed forms of the unique sphere side pairing exhaust its identifications.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePreMap : C(sphere.PolygonalPreRealization, SphereRepresentative)

The continuous facewise map from the two monogon disks to the corresponding hemispheres.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePreMap_false (z : PolygonCell 1) : spherePreMap ⟨false, z⟩ = PolygonCell.upperHemisphere z

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePreMap_true (z : PolygonCell 1) : spherePreMap ⟨true, z⟩ = PolygonCell.lowerHemisphere z

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePreMap_sphereBoundaryPairing (t : ↑unitInterval) : spherePreMap (sphereBoundaryPairing.identification.source.point t) = spherePreMap (sphereBoundaryPairing.identification.target.point (sphereBoundaryPairing.identification.parameter t))

The facewise map respects the canonical directed sphere boundary pairing.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePreMap_swapSphereBoundaryPairing (t : ↑unitInterval) : spherePreMap ((swapIdentification sphereBoundaryPairing.identification).source.point t) = spherePreMap ((swapIdentification sphereBoundaryPairing.identification).target.point ((swapIdentification sphereBoundaryPairing.identification).parameter t))

The facewise map respects the swapped directed sphere boundary pairing.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePreMap_eq_of_generator {x y : sphere.PolygonalPreRealization} (hxy : PolygonGluing.Generator (sphere.polygonalIdentifications sphere_occurrencePairingValid) x y) : spherePreMap x = spherePreMap y

The facewise sphere map identifies the endpoints of every raw polygon gluing generator.