Disk geometry for the sphere carrier

The faithful sphere presentation glues two monogons with opposite boundary directions. This file records the elementary disk geometry needed to map those two cells to opposite hemispheres: complex conjugation is a self-homeomorphism of every indexed polygon cell, and on a monogon it turns the reversed boundary parameter back into the forward parameter.

The indexed cells are also compact. The instance is transported through the existing homeomorphism with the closed unit disk, keeping this fact tied to the actual polygon carrier.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.conjHomeomorph (n : ℕ) : PolygonCell n ≃ₜ PolygonCell n

Complex conjugation as a self-homeomorphism of an indexed polygon cell.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.conjHomeomorph_apply (n : ℕ) (z : PolygonCell n) : ((conjHomeomorph n) z).val = (starRingEnd ℂ) z.val

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.conj_side_symm_monogon (t : ↑unitInterval) : (starRingEnd ℂ) ((side 0) (unitInterval.symm t)).val = ((side 0) t).val

On a monogon, conjugation changes the reversed boundary parameter into the forward one.

instance LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.instCompactSpace (n : ℕ) : CompactSpace (PolygonCell n)

Every indexed polygon cell is compact through its identification with the closed unit disk.