Generator maps for the canonical Eval representatives

This file upgrades the explicit carrier-coordinate comparisons to maps between the full raw generator relations. Together with the reverse maps from the trusted Eval constructors, these maps identify the generated equivalence relations and descend the one-face carrier homeomorphisms to the canonical quotient spaces.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableGenerator_to_eqvGen {p n : ℕ} (hvalid : 1 ≤ p ∨ 1 ≤ n) {x y : (orientableCellComplex p n).PolygonalPreRealization} (hxy : PolygonGluing.Generator ((orientableCellComplex p n).polygonalIdentifications ⋯) x y) : Relation.EqvGen (OrientableRel p n) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) x) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) y)

Every orientable polygon generator maps into the trusted equivalence closure.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableGenerator_to_eqvGen {p n : ℕ} (hp : 1 ≤ p) {x y : (nonOrientableCellComplex p n).PolygonalPreRealization} (hxy : PolygonGluing.Generator ((nonOrientableCellComplex p n).polygonalIdentifications ⋯) x y) : Relation.EqvGen (NonOrientableRel p n) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) x) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) y)

Every nonorientable polygon generator maps into the trusted equivalence closure.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableRel_to_polygonEqvGen {p n : ℕ} (hvalid : 1 ≤ p ∨ 1 ≤ n) {x y : Complex.ClosedUnitDisc} (hxy : OrientableRel p n x y) : Relation.EqvGen (PolygonGluing.Generator ((orientableCellComplex p n).polygonalIdentifications ⋯)) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)).symm x) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)).symm y)

Every trusted orientable generator maps back into the polygonal equivalence closure.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableRel_to_polygonEqvGen {p n : ℕ} (hp : 1 ≤ p) {x y : Complex.ClosedUnitDisc} (hxy : NonOrientableRel p n x y) : Relation.EqvGen (PolygonGluing.Generator ((nonOrientableCellComplex p n).polygonalIdentifications ⋯)) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)).symm x) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)).symm y)

Every trusted nonorientable generator maps back into the polygonal equivalence closure.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientablePolygonalRealizationHomeomorph {p n : ℕ} (hvalid : 1 ≤ p ∨ 1 ≤ n) : (orientableCellComplex p n).PolygonalRealization ⋯ ≃ₜ Quot (OrientableRel p n)

The canonical orientable polygonal realization is the trusted Eval quotient.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientablePolygonalRealizationHomeomorph {p n : ℕ} (hp : 1 ≤ p) : (nonOrientableCellComplex p n).PolygonalRealization ⋯ ≃ₜ Quot (NonOrientableRel p n)

The canonical nonorientable polygonal realization is the trusted Eval quotient.

Equations

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