Carrier bridge to the Eval quotient representatives

The canonical cell complexes and the trusted Lean-Eval statement use two presentations of the same carrier:

• a one-face polygonal pre-realization, whose unique PolygonCell is a closed disk; and
• Complex.ClosedUnitDisc, on which the benchmark relations are stated.

This file identifies those carriers and records the exact boundary coordinates. It also bridges Lean's raw-relation quotient Quot r with Quotient (Relation.EqvGen.setoid r), the generated setoid used by the polygonal gluing layer.

The remaining comparison is deliberately isolated: prove that the equivalence closure of the canonical polygonal generators transports to the equivalence closure of OrientableRel or NonOrientableRel.

theorem Complex.ClosedUnitDisc.bdyPtOfReal_add_int (r : ℝ) (k : ℤ) : bdyPtOfReal (r + ↑k) = bdyPtOfReal r

The benchmark boundary parameter is periodic with integral period one.

def LeanEval.Topology.ClassificationOfSurfaces.quotEqvGenHomeomorph {X : Type u_1} [TopologicalSpace X] (r : X → X → Prop) : Quot r ≃ₜ Quotient (Relation.EqvGen.setoid r)

Quot by a raw relation is homeomorphic to Quotient by its equivalence closure.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.eqvGenQuotientCongrRaw {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {r : X → X → Prop} {s : Y → Y → Prop} (e : X ≃ₜ Y) (h : ∀ (x y : X), Relation.EqvGen r x y ↔ Relation.EqvGen s (e x) (e y)) : Quotient (Relation.EqvGen.setoid r) ≃ₜ Quot s

Transport equivalence closures and bridge a generated-setoid quotient to a raw quotient.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.eqvGenQuotientCongrRaw e h = (Homeomorph.Quotient.congr e h).trans (LeanEval.Topology.ClassificationOfSurfaces.quotEqvGenHomeomorph s).symm

theorem LeanEval.Topology.ClassificationOfSurfaces.eqvGen_map_of_generator_to_eqvGen {X : Type u_1} {Y : Type u_2} {r : X → X → Prop} {s : Y → Y → Prop} (f : X → Y) (hgen : ∀ (x y : X), r x y → Relation.EqvGen s (f x) (f y)) {x y : X} (hxy : Relation.EqvGen r x y) : Relation.EqvGen s (f x) (f y)

A map that sends generators into an equivalence closure sends the whole generated relation into that closure.

theorem LeanEval.Topology.ClassificationOfSurfaces.eqvGen_iff_of_generator_maps {X : Type u_1} {Y : Type u_2} {r : X → X → Prop} {s : Y → Y → Prop} (e : X ≃ Y) (hforward : ∀ (x y : X), r x y → Relation.EqvGen s (e x) (e y)) (hbackward : ∀ (x y : Y), s x y → Relation.EqvGen r (e.symm x) (e.symm y)) (x y : X) : Relation.EqvGen r x y ↔ Relation.EqvGen s (e x) (e y)

Comparing generators in both directions, up to equivalence closure, compares the generated relations.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.eqvGenQuotientCongrRawOfGeneratorMaps {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {r : X → X → Prop} {s : Y → Y → Prop} (e : X ≃ₜ Y) (hforward : ∀ (x y : X), r x y → Relation.EqvGen s (e x) (e y)) (hbackward : ∀ (x y : Y), s x y → Relation.EqvGen r (e.symm x) (e.symm y)) : Quotient (Relation.EqvGen.setoid r) ≃ₜ Quot s

Transport generators up to equivalence closure and descend to a target raw Quot.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.closedUnitDiscHomeomorph (m : ℕ) : PolygonCell m ≃ₜ Complex.ClosedUnitDisc

The indexed polygon cell is the closed unit disk, with only a different wrapper.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.closedUnitDiscHomeomorph_side {m : ℕ} (i : Fin m) (t : ↑unitInterval) : (closedUnitDiscHomeomorph m) ((side i) t) = Complex.ClosedUnitDisc.bdyPtOfReal ((↑↑i + ↑t) / ↑m)

Under the carrier homeomorphism, side i has the benchmark's boundary parameter.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.oneFacePreRealizationHomeomorph (m : ℕ) : (PreRealization PUnit.{u_1 + 1} fun (x : PUnit.{u_1 + 1}) => m) ≃ₜ Complex.ClosedUnitDisc

The unique polygon in a one-face presentation is homeomorphic to the closed unit disk.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.oneFacePreRealizationHomeomorph_sidePoint {m : ℕ} (i : Fin m) (t : ↑unitInterval) : (oneFacePreRealizationHomeomorph m) ((have this := { face := PUnit.unit, index := i }; this).point t) = Complex.ClosedUnitDisc.bdyPtOfReal ((↑↑i + ↑t) / ↑m)

Side points in a one-face pre-realization map to the exact benchmark boundary points.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph {Edge : Type} [Fintype Edge] (word : List (SignedDart Edge)) : (oneFacePresentation Edge word).PolygonalPreRealization ≃ₜ Complex.ClosedUnitDisc

The one-face polygonal pre-realization of a boundary word is the closed unit disk.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph_sidePoint {Edge : Type} [Fintype Edge] (word : List (SignedDart Edge)) (i : Fin word.length) (t : ↑unitInterval) : (oneFacePolygonalPreRealizationHomeomorph word) (((oneFacePresentation Edge word).occurrenceSide ⟨PUnit.unit, i⟩).point t) = Complex.ClosedUnitDisc.bdyPtOfReal ((↑↑i + ↑t) / ↑word.length)

The direct one-face homeomorphism sends occurrence i to the benchmark parameter (i + t) / word.length.