Polygonal quotient spaces

This file supplies the geometric foundation for realizing a finite surface cell complex. A PolygonCell n is a genuinely indexed closed disk with n labelled boundary arcs. This topological model keeps monogons and digons as genuine disks, unlike a convex hull of one or two Euclidean vertices. Its sides are circular arcs; only their interval reparameterizations are affine. A later PL bridge is therefore still needed if consumers require straight Euclidean edges.

For a family of cells, PolygonGluing.PreRealization is their disjoint union with the sum topology. A set of PolygonGluing.Identifications prescribes either the identity or the affine reversal t ↦ 1 - t between pairs of sides. PolygonGluing.setoid is the equivalence relation generated by those point identifications, and PolygonGluing.Realization has the quotient topology.

PolygonCell 0 is a disk with no marked sides. It is deliberately not identified with the empty-word sphere. The cell-complex adapter therefore presents the sphere as two oppositely oriented monogons instead of using PolygonCell 0. Keeping that choice out of this generic layer prevents a side-free disk from silently acquiring the wrong topology.

structure LeanEval.Topology.ClassificationOfSurfaces.PolygonCell (_n : ℕ) : Type

A closed disk whose boundary is divided into n labelled sides.

• val : ℂ

  The val declaration.

• property : self.val ∈ Metric.closedBall 0 1

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.instCoeOutComplex (n : ℕ) : CoeOut (PolygonCell n) ℂ

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.instCoeOutComplex n = { coe := LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.val }

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.ext {n : ℕ} {x y : PolygonCell n} (h : x.val = y.val) : x = y

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.ext_iff {n : ℕ} {x y : PolygonCell n} : x = y ↔ x.val = y.val

@[instance_reducible]

noncomputable instance LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.instTopologicalSpace (n : ℕ) : TopologicalSpace (PolygonCell n)

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.instTopologicalSpace n = TopologicalSpace.induced LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.val inferInstance

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.continuous_val {n : ℕ} : Continuous fun (x : PolygonCell n) => x.val

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.castHomeomorph {m n : ℕ} (h : m = n) : PolygonCell m ≃ₜ PolygonCell n

The side count is marking data only: changing it does not change the underlying closed disk.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.castHomeomorph h = h ▸ Homeomorph.refl (LeanEval.Topology.ClassificationOfSurfaces.PolygonCell m)

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.castHomeomorph_val {m n : ℕ} (h : m = n) (x : PolygonCell m) : ((castHomeomorph h) x).val = x.val

def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.ofCircle (n : ℕ) : C(Circle, PolygonCell n)

The unit circle included in a polygonal cell.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.ofCircle n = { toFun := fun (z : Circle) => { val := ↑z, property := ⋯ }, continuous_toFun := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.sideAngle {n : ℕ} (i : Fin n) (t : ↑unitInterval) : ℝ

The angle swept out by side i at parameter t.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.sideAngle i t = 2 * Real.pi * (↑↑i + ↑t) / ↑n

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.continuous_sideAngle {n : ℕ} (i : Fin n) : Continuous (sideAngle i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.side {n : ℕ} (i : Fin n) : C(↑unitInterval, PolygonCell n)

Side i of an n-sided cell, parameterized in boundary order.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.reversedSide {n : ℕ} (i : Fin n) : C(↑unitInterval, PolygonCell n)

Side i traversed in the opposite direction.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.reversedSide_apply {n : ℕ} (i : Fin n) (t : ↑unitInterval) : (reversedSide i) t = (side i) (unitInterval.symm t)

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.castHomeomorph_side {m n : ℕ} (h : m = n) (i : Fin m) (t : ↑unitInterval) : (castHomeomorph h) ((side i) t) = (side (Fin.cast h i)) t

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.reversedSide_zero {n : ℕ} (i : Fin n) : (reversedSide i) 0 = (side i) 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.reversedSide_one {n : ℕ} (i : Fin n) : (reversedSide i) 1 = (side i) 0

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.side_one_eq_rotate_zero {n : ℕ} (i : Fin n) : (side i) 1 = (side ((finRotate n) i)) 0

Consecutive sides meet at their common cyclic endpoint.

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.side_mem_sphere {n : ℕ} (i : Fin n) (t : ↑unitInterval) : ((side i) t).val ∈ Metric.sphere 0 1

Every side lies on the boundary circle of its polygonal cell.

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.exists_side_eq_of_mem_sphere {n : ℕ} (hn : 0 < n) (x : PolygonCell n) (hx : x.val ∈ Metric.sphere 0 1) : ∃ (i : Fin n) (t : ↑unitInterval), (side i) t = x

Every boundary point of a cell with at least one side belongs to a marked side.

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.mem_sphere_iff_exists_side {n : ℕ} (hn : 0 < n) (x : PolygonCell n) : x.val ∈ Metric.sphere 0 1 ↔ ∃ (i : Fin n) (t : ↑unitInterval), (side i) t = x

Boundary membership is equivalent to membership in one of the marked sides.

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.iUnion_range_side {n : ℕ} (hn : 0 < n) : ⋃ (i : Fin n), Set.range ⇑(side i) = {x : PolygonCell n | x.val ∈ Metric.sphere 0 1}

The marked sides cover exactly the boundary circle of a nonzero-sided cell.

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.side_zero_eq_side_one_monogon (i : Fin 1) : (side i) 0 = (side i) 1

The unique side of a monogon is a loop.

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.side_zero_one_eq_side_one_zero_digon : (side 0) 1 = (side 1) 0

The two sides of a digon meet at their middle vertex.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.PreRealization (Face : Type u) (sideCount : Face → ℕ) : Type u

The disjoint union of a family of polygonal cells.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.PreRealization Face sideCount = ((f : Face) × LeanEval.Topology.ClassificationOfSurfaces.PolygonCell (sideCount f))

structure LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.Side (Face : Type u) (sideCount : Face → ℕ) : Type u

A labelled side in a family of polygonal cells.

• face : Face

  The face declaration.

• index : Fin (sideCount self.face)

  The index declaration.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.Side.point {Face : Type u} {sideCount : Face → ℕ} (s : Side Face sideCount) (t : ↑unitInterval) : PreRealization Face sideCount

A point on a labelled side, included in the disjoint union.

Equations

• s.point t = ⟨s.face, (LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.side s.index) t⟩

inductive LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.ParameterDirection : Type

The two affine self-homeomorphisms of the unit interval used to glue polygon sides.

• same : ParameterDirection
• opposite : ParameterDirection

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.instDecidableEqParameterDirection : DecidableEq ParameterDirection

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.instDecidableEqParameterDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.instReprParameterDirection : Repr ParameterDirection

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.instReprParameterDirection = { reprPrec := LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.instReprParameterDirection.repr }

def LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.instReprParameterDirection.repr : ParameterDirection → ℕ → Std.Format

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.ParameterDirection.homeomorph : ParameterDirection → ↑unitInterval ≃ₜ ↑unitInterval

The affine interval homeomorphism associated to a parameter direction.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.ParameterDirection.same.homeomorph = Homeomorph.refl ↑unitInterval
• LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.ParameterDirection.opposite.homeomorph = unitInterval.symmHomeomorph

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.ParameterDirection.homeomorph_same : same.homeomorph = Homeomorph.refl ↑unitInterval

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.ParameterDirection.homeomorph_opposite : opposite.homeomorph = unitInterval.symmHomeomorph

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.ParameterDirection.homeomorph_same_apply (t : ↑unitInterval) : same.homeomorph t = t

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.ParameterDirection.homeomorph_opposite_apply (t : ↑unitInterval) : opposite.homeomorph t = unitInterval.symm t

structure LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.Identification (Face : Type u) (sideCount : Face → ℕ) : Type u

Instructions for identifying two polygon sides with an affine parameter map.

• source : Side Face sideCount

  The source declaration.

• target : Side Face sideCount

  The target declaration.

• direction : ParameterDirection

  The direction declaration.

def LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.Identification.parameter {Face : Type u} {sideCount : Face → ℕ} (identification : Identification Face sideCount) : ↑unitInterval ≃ₜ ↑unitInterval

The affine parameter homeomorphism of a side identification.

Equations

• identification.parameter = identification.direction.homeomorph

def LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.Identification.sameDirection {Face : Type u} {sideCount : Face → ℕ} (source target : Side Face sideCount) : Identification Face sideCount

Identify two sides with the same parameter direction.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.Identification.oppositeDirection {Face : Type u} {sideCount : Face → ℕ} (source target : Side Face sideCount) : Identification Face sideCount

Identify two sides with the parameter direction reversed.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.Identification.parameter_sameDirection {Face : Type u} {sideCount : Face → ℕ} (source target : Side Face sideCount) : (sameDirection source target).parameter = Homeomorph.refl ↑unitInterval

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.Identification.parameter_oppositeDirection {Face : Type u} {sideCount : Face → ℕ} (source target : Side Face sideCount) : (oppositeDirection source target).parameter = unitInterval.symmHomeomorph

inductive LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.Generator {Face : Type u} {sideCount : Face → ℕ} (identifications : Set (Identification Face sideCount)) : PreRealization Face sideCount → PreRealization Face sideCount → Prop

The elementary point identifications prescribed by a collection of side gluings.

• glue {Face : Type u} {sideCount : Face → ℕ} {identifications : Set (Identification Face sideCount)} (identification : Identification Face sideCount) (h : identification ∈ identifications) (t : ↑unitInterval) : Generator identifications (identification.source.point t) (identification.target.point (identification.parameter t))

def LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.setoid {Face : Type u} {sideCount : Face → ℕ} (identifications : Set (Identification Face sideCount)) : Setoid (PreRealization Face sideCount)

The equivalence relation generated by the prescribed side identifications.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.setoid identifications = Relation.EqvGen.setoid (LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.Generator identifications)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.setoid_empty {Face : Type u} {sideCount : Face → ℕ} : setoid ∅ = ⊥

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.related_of_mem {Face : Type u} {sideCount : Face → ℕ} {identifications : Set (Identification Face sideCount)} (identification : Identification Face sideCount) (h : identification ∈ identifications) (t : ↑unitInterval) : (setoid identifications) (identification.source.point t) (identification.target.point (identification.parameter t))

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.Realization {Face : Type u} {sideCount : Face → ℕ} (identifications : Set (Identification Face sideCount)) : Type u

The quotient of the polygonal disjoint union by the generated side identifications.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.Realization identifications = Quotient (LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.setoid identifications)

def LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.mk {Face : Type u} {sideCount : Face → ℕ} (identifications : Set (Identification Face sideCount)) : PreRealization Face sideCount → Realization identifications

The quotient map from the disjoint union to the glued realization.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.mk identifications = Quotient.mk'

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.continuous_mk {Face : Type u} {sideCount : Face → ℕ} (identifications : Set (Identification Face sideCount)) : Continuous (mk identifications)

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.isQuotientMap_mk {Face : Type u} {sideCount : Face → ℕ} (identifications : Set (Identification Face sideCount)) : Topology.IsQuotientMap (mk identifications)

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.mk_source_eq_mk_target {Face : Type u} {sideCount : Face → ℕ} {identifications : Set (Identification Face sideCount)} (identification : Identification Face sideCount) (h : identification ∈ identifications) (t : ↑unitInterval) : mk identifications (identification.source.point t) = mk identifications (identification.target.point (identification.parameter t))

A prescribed side gluing identifies the corresponding points in the quotient.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.realizationCongr {Face₁ : Type u} {sideCount₁ : Face₁ → ℕ} {Face₂ : Type u} {sideCount₂ : Face₂ → ℕ} {identifications₁ : Set (Identification Face₁ sideCount₁)} {identifications₂ : Set (Identification Face₂ sideCount₂)} (e : PreRealization Face₁ sideCount₁ ≃ₜ PreRealization Face₂ sideCount₂) (h : ∀ (x y : PreRealization Face₁ sideCount₁), (setoid identifications₁) x y ↔ (setoid identifications₂) (e x) (e y)) : Realization identifications₁ ≃ₜ Realization identifications₂

A relation-preserving homeomorphism descends to polygonal realizations.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.realizationCongr e h = Homeomorph.Quotient.congr e h

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.realizationCongrRight {Face : Type u} {sideCount : Face → ℕ} {identifications₁ identifications₂ : Set (Identification Face sideCount)} (h : ∀ (x y : PreRealization Face sideCount), (setoid identifications₁) x y ↔ (setoid identifications₂) x y) : Realization identifications₁ ≃ₜ Realization identifications₂

Equal generated relations give homeomorphic realizations on a fixed pre-space.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.realizationCongrRight h = Homeomorph.Quotient.congrRight h