The canonical finite-cyclic sphere realization

This file compares the finite-cyclic two-monogon presentation with the existing typed two-monogon presentation and transports the already established sphere homeomorphism across that comparison.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonFaceEquiv : twoMonogonSphere.Face ≃ Bool

The two faces of the finite-cyclic sphere, in the order used by the typed sphere model.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonFaceEquiv_zero : twoMonogonFaceEquiv 0 = false

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonFaceEquiv_one : twoMonogonFaceEquiv 1 = true

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogon_faceBoundaryLength_eq (f : twoMonogonSphere.Face) : (twoMonogonSphere.boundary f).length = SurfaceCellComplex.sphere.faceBoundaryLength (twoMonogonFaceEquiv f)

Corresponding monogon faces have the same side count.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonFaceHomeomorph (f : twoMonogonSphere.Face) : PolygonCell (twoMonogonSphere.boundary f).length ≃ₜ PolygonCell (SurfaceCellComplex.sphere.faceBoundaryLength (twoMonogonFaceEquiv f))

The identity disk map, with its side-count index transported to the typed sphere model.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPreHomeomorph : twoMonogonSphere.PolygonalPreRealization ≃ₜ SurfaceCellComplex.sphere.PolygonalPreRealization

Relabel the two finite-cyclic monogon faces by Bool, leaving both disks fixed.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPreHomeomorph_zero (z : PolygonCell 1) : twoMonogonPreHomeomorph ⟨0, z⟩ = ⟨false, z⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPreHomeomorph_one (z : PolygonCell 1) : twoMonogonPreHomeomorph ⟨1, z⟩ = ⟨true, z⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPreHomeomorph_symm_false (z : PolygonCell 1) : twoMonogonPreHomeomorph.symm ⟨false, z⟩ = ⟨0, z⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPreHomeomorph_symm_true (z : PolygonCell 1) : twoMonogonPreHomeomorph.symm ⟨true, z⟩ = ⟨1, z⟩

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPositiveOccurrence : twoMonogonSphere.BoundaryOccurrence

The positive monogon occurrence in the finite-cyclic sphere.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonNegativeOccurrence : twoMonogonSphere.BoundaryOccurrence

The negative monogon occurrence in the finite-cyclic sphere.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPositiveOccurrence_dart : twoMonogonPositiveOccurrence.dart = SurfaceCellComplex.SignedDart.pos 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonNegativeOccurrence_dart : twoMonogonNegativeOccurrence.dart = SurfaceCellComplex.SignedDart.neg 0

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonBoundaryOccurrence_eq (occurrence : twoMonogonSphere.BoundaryOccurrence) : occurrence = twoMonogonPositiveOccurrence ∨ occurrence = twoMonogonNegativeOccurrence

Every boundary occurrence of the finite-cyclic sphere is one of its two monogon sides.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogon_not_isBoundaryEdge (e : twoMonogonSphere.Edge) : ¬twoMonogonSphere.IsBoundaryEdge e

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonBoundaryPairing : twoMonogonSphere.BoundaryPairing

The directed positive-to-negative side pairing of the finite-cyclic sphere.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonReverseBoundaryPairing : twoMonogonSphere.BoundaryPairing

The reverse directed form of the unique finite-cyclic sphere pairing.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonBoundaryPairing_mem : twoMonogonBoundaryPairing.identification ∈ twoMonogonSphere.polygonalIdentifications twoMonogonSphere_isSurfaceValid

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonReverseBoundaryPairing_mem : twoMonogonReverseBoundaryPairing.identification ∈ twoMonogonSphere.polygonalIdentifications twoMonogonSphere_isSurfaceValid

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.mem_twoMonogon_polygonalIdentifications_iff (identification : PolygonGluing.Identification twoMonogonSphere.Face fun (f : twoMonogonSphere.Face) => (twoMonogonSphere.boundary f).length) : identification ∈ twoMonogonSphere.polygonalIdentifications twoMonogonSphere_isSurfaceValid ↔ identification = twoMonogonBoundaryPairing.identification ∨ identification = twoMonogonReverseBoundaryPairing.identification

The two directed forms of the monogon pairing exhaust the finite-cyclic sphere generators.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPreHomeomorph_boundaryPairing_source (t : ↑unitInterval) : twoMonogonPreHomeomorph (twoMonogonBoundaryPairing.identification.source.point t) = SurfaceCellComplex.sphereBoundaryPairing.identification.source.point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPreHomeomorph_boundaryPairing_target (t : ↑unitInterval) : twoMonogonPreHomeomorph (twoMonogonBoundaryPairing.identification.target.point t) = SurfaceCellComplex.sphereBoundaryPairing.identification.target.point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPreHomeomorph_reverseBoundaryPairing_source (t : ↑unitInterval) : twoMonogonPreHomeomorph (twoMonogonReverseBoundaryPairing.identification.source.point t) = (SurfaceCellComplex.swapIdentification SurfaceCellComplex.sphereBoundaryPairing.identification).source.point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPreHomeomorph_reverseBoundaryPairing_target (t : ↑unitInterval) : twoMonogonPreHomeomorph (twoMonogonReverseBoundaryPairing.identification.target.point t) = (SurfaceCellComplex.swapIdentification SurfaceCellComplex.sphereBoundaryPairing.identification).target.point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPreHomeomorph_related {x y : twoMonogonSphere.PolygonalPreRealization} (hxy : (twoMonogonSphere.PolygonalGluingRel twoMonogonSphere_isSurfaceValid) x y) : (SurfaceCellComplex.sphere.PolygonalGluingRel SurfaceCellComplex.sphere_occurrencePairingValid) (twoMonogonPreHomeomorph x) (twoMonogonPreHomeomorph y)

Relabeling the two monogon faces sends the finite-cyclic gluing relation into the typed sphere gluing relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPreHomeomorph_symm_related {x y : SurfaceCellComplex.sphere.PolygonalPreRealization} (hxy : (SurfaceCellComplex.sphere.PolygonalGluingRel SurfaceCellComplex.sphere_occurrencePairingValid) x y) : (twoMonogonSphere.PolygonalGluingRel twoMonogonSphere_isSurfaceValid) (twoMonogonPreHomeomorph.symm x) (twoMonogonPreHomeomorph.symm y)

The inverse face relabeling sends the typed sphere gluing relation back into the finite-cyclic gluing relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonPreHomeomorph_related_iff (x y : twoMonogonSphere.PolygonalPreRealization) : (twoMonogonSphere.PolygonalGluingRel twoMonogonSphere_isSurfaceValid) x y ↔ (SurfaceCellComplex.sphere.PolygonalGluingRel SurfaceCellComplex.sphere_occurrencePairingValid) (twoMonogonPreHomeomorph x) (twoMonogonPreHomeomorph y)

The face relabeling identifies the generated finite-cyclic and typed sphere relations exactly.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonRealizationHomeomorph : twoMonogonSphere.PolygonalRealization twoMonogonSphere_isSurfaceValid ≃ₜ SurfaceCellComplex.sphere.PolygonalRealization SurfaceCellComplex.sphere_occurrencePairingValid

The faithful finite-cyclic two-monogon quotient is homeomorphic to the typed sphere quotient.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonSphereRepresentativeHomeomorph : twoMonogonSphere.PolygonalRealization twoMonogonSphere_isSurfaceValid ≃ₜ SphereRepresentative

The canonical finite-cyclic sphere presentation realizes the exact Eval sphere representative.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.canonicalSphereRealizationHomeomorph : sphere.canonicalPresentation.PolygonalRealization ⋯ ≃ₜ SphereRepresentative

The sphere branch of canonicalPresentation realizes the exact Eval sphere representative.

Equations

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