The two-monogon quotient is the standard sphere

The facewise hemisphere map from SphereHemisphere respects the equivalence relation generated by the sphere's side pairing, so it descends to the polygonal realization. This file proves that the descended map is bijective and hence, by compactness of the source and the Hausdorff property of the target, a homeomorphism with SphereRepresentative.

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.upperHemisphere_injective : Function.Injective ⇑upperHemisphere

The upper hemisphere parameterization remembers its disk point.

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.lowerHemisphere_injective : Function.Injective ⇑lowerHemisphere

The lower hemisphere parameterization remembers its disk point.

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.mem_sphere_of_hemisphereHeight_eq_zero {n : ℕ} (z : PolygonCell n) (hz : z.hemisphereHeight = 0) : z.val ∈ Metric.sphere 0 1

Zero hemisphere height means that the disk point lies on its boundary circle.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.sphereDiskPoint (x : SphereRepresentative) : PolygonCell 1

The horizontal coordinates of a point on the standard sphere, regarded as a disk point.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.sphereDiskPoint x = { val := { re := (↑x).ofLp 0, im := (↑x).ofLp 1 }, property := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.sphereDiskPoint_re (x : SphereRepresentative) : (sphereDiskPoint x).val.re = (↑x).ofLp 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.sphereDiskPoint_im (x : SphereRepresentative) : (sphereDiskPoint x).val.im = (↑x).ofLp 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.hemisphereHeight_sphereDiskPoint (x : SphereRepresentative) : (sphereDiskPoint x).hemisphereHeight = |(↑x).ofLp 2|

The height recovered from the horizontal coordinates is the absolute vertical coordinate.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.hemisphereHeight_conjHomeomorph {n : ℕ} (z : PolygonCell n) : ((conjHomeomorph n) z).hemisphereHeight = z.hemisphereHeight

Complex conjugation does not change the height assigned to a disk point.

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.upperHemisphere_sphereDiskPoint (x : SphereRepresentative) (hx : 0 ≤ (↑x).ofLp 2) : upperHemisphere (sphereDiskPoint x) = x

A sphere point with nonnegative vertical coordinate is hit by the upper hemisphere.

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.lowerHemisphere_conj_sphereDiskPoint (x : SphereRepresentative) (hx : (↑x).ofLp 2 ≤ 0) : lowerHemisphere ((conjHomeomorph 1) (sphereDiskPoint x)) = x

A sphere point with nonpositive vertical coordinate is hit by the conjugated lower face.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePreMap_eq_of_gluingRel {x y : sphere.PolygonalPreRealization} (hxy : (sphere.PolygonalGluingRel sphere_occurrencePairingValid) x y) : spherePreMap x = spherePreMap y

The sphere pre-map is constant on the equivalence relation generated by the side pairing.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereQuotientMap : C(sphere.PolygonalRealization sphere_occurrencePairingValid, SphereRepresentative)

The continuous sphere map descended from the two monogon faces to their polygonal quotient.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereQuotientMap_polygonalMk (x : sphere.PolygonalPreRealization) : sphereQuotientMap (sphere.polygonalMk sphere_occurrencePairingValid x) = spherePreMap x

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereGluingRel_of_upperHemisphere_eq_lowerHemisphere (z w : PolygonCell 1) (hzw : PolygonCell.upperHemisphere z = PolygonCell.lowerHemisphere w) : (sphere.PolygonalGluingRel sphere_occurrencePairingValid) ⟨false, z⟩ ⟨true, w⟩

Equality between an upper- and a lower-hemisphere image is exactly an equatorial gluing.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereGluingRel_of_spherePreMap_eq {x y : sphere.PolygonalPreRealization} (hxy : spherePreMap x = spherePreMap y) : (sphere.PolygonalGluingRel sphere_occurrencePairingValid) x y

Equal images under the facewise map are related by the generated sphere gluing relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePreMap_eq_iff_gluingRel {x y : sphere.PolygonalPreRealization} : spherePreMap x = spherePreMap y ↔ (sphere.PolygonalGluingRel sphere_occurrencePairingValid) x y

The generated sphere gluing relation is precisely the kernel relation of the pre-map.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereQuotientMap_injective : Function.Injective ⇑sphereQuotientMap

The descended sphere map is injective.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereQuotientMap_surjective : Function.Surjective ⇑sphereQuotientMap

Every point of the standard sphere is hit by the descended two-monogon map.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereQuotientMap_bijective : Function.Bijective ⇑sphereQuotientMap

The descended sphere map is bijective.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePolygonalRealizationEquiv : sphere.PolygonalRealization sphere_occurrencePairingValid ≃ SphereRepresentative

The underlying equivalence of the two-monogon quotient with the standard sphere.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePolygonalRealizationEquiv_apply (q : sphere.PolygonalRealization sphere_occurrencePairingValid) : spherePolygonalRealizationEquiv q = sphereQuotientMap q

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePolygonalRealizationHomeomorph : sphere.PolygonalRealization sphere_occurrencePairingValid ≃ₜ SphereRepresentative

The polygonal realization of the two-monogon presentation is the standard two-sphere.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePolygonalRealizationHomeomorph_apply (q : sphere.PolygonalRealization sphere_occurrencePairingValid) : spherePolygonalRealizationHomeomorph q = sphereQuotientMap q

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePolygonalRealizationHomeomorph_polygonalMk (x : sphere.PolygonalPreRealization) : spherePolygonalRealizationHomeomorph (sphere.polygonalMk sphere_occurrencePairingValid x) = spherePreMap x