Standard combinatorial examples

This file names the small surfaces we should keep as regression tests while the definitions mature. The examples are concrete one-face boundary-word presentations in the shared SurfaceCellComplex API. Their topology is supplied by the faithful polygonal quotient layer.

def LeanEval.Topology.ClassificationOfSurfaces.sphereNormalForm : NormalForm

The normal form for the sphere.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.sphereNormalForm = LeanEval.Topology.ClassificationOfSurfaces.NormalForm.sphere

def LeanEval.Topology.ClassificationOfSurfaces.diskNormalForm : NormalForm

The normal form for the disk: orientable genus zero with one boundary component.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.diskNormalForm = LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientable 0 1

def LeanEval.Topology.ClassificationOfSurfaces.annulusNormalForm : NormalForm

The normal form for the annulus: orientable genus zero with two boundary components.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.annulusNormalForm = LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientable 0 2

def LeanEval.Topology.ClassificationOfSurfaces.torusNormalForm : NormalForm

The normal form for the torus: orientable genus one with no boundary.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.torusNormalForm = LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientable 1 0

def LeanEval.Topology.ClassificationOfSurfaces.projectivePlaneNormalForm : NormalForm

The normal form for the projective plane: one crosscap and no boundary.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.projectivePlaneNormalForm = LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientable 1 0

def LeanEval.Topology.ClassificationOfSurfaces.mobiusStripNormalForm : NormalForm

The normal form for the Mobius strip: one crosscap and one boundary component.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.mobiusStripNormalForm = LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientable 1 1

inductive LeanEval.Topology.ClassificationOfSurfaces.DiskEdge : Type

Edge names for the disk example.

• h : DiskEdge

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instDecidableEqDiskEdge : DecidableEq DiskEdge

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.instReprDiskEdge.repr : DiskEdge → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instReprDiskEdge : Repr DiskEdge

Equations

• LeanEval.Topology.ClassificationOfSurfaces.instReprDiskEdge = { reprPrec := LeanEval.Topology.ClassificationOfSurfaces.instReprDiskEdge.repr }

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instFintypeDiskEdge : Fintype DiskEdge

Equations

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

inductive LeanEval.Topology.ClassificationOfSurfaces.AnnulusEdge : Type

Edge names for the annulus example.

• d₀ : AnnulusEdge
• c₀ : AnnulusEdge
• d₁ : AnnulusEdge
• c₁ : AnnulusEdge

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instDecidableEqAnnulusEdge : DecidableEq AnnulusEdge

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instReprAnnulusEdge : Repr AnnulusEdge

Equations

• LeanEval.Topology.ClassificationOfSurfaces.instReprAnnulusEdge = { reprPrec := LeanEval.Topology.ClassificationOfSurfaces.instReprAnnulusEdge.repr }

def LeanEval.Topology.ClassificationOfSurfaces.instReprAnnulusEdge.repr : AnnulusEdge → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instFintypeAnnulusEdge : Fintype AnnulusEdge

Equations

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

inductive LeanEval.Topology.ClassificationOfSurfaces.TorusEdge : Type

Edge names for the torus example.

• a : TorusEdge
• b : TorusEdge

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instDecidableEqTorusEdge : DecidableEq TorusEdge

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instReprTorusEdge : Repr TorusEdge

Equations

• LeanEval.Topology.ClassificationOfSurfaces.instReprTorusEdge = { reprPrec := LeanEval.Topology.ClassificationOfSurfaces.instReprTorusEdge.repr }

def LeanEval.Topology.ClassificationOfSurfaces.instReprTorusEdge.repr : TorusEdge → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instFintypeTorusEdge : Fintype TorusEdge

Equations

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

inductive LeanEval.Topology.ClassificationOfSurfaces.ProjectivePlaneEdge : Type

Edge names for the projective-plane example.

• a : ProjectivePlaneEdge

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instDecidableEqProjectivePlaneEdge : DecidableEq ProjectivePlaneEdge

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.instReprProjectivePlaneEdge.repr : ProjectivePlaneEdge → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instReprProjectivePlaneEdge : Repr ProjectivePlaneEdge

Equations

• LeanEval.Topology.ClassificationOfSurfaces.instReprProjectivePlaneEdge = { reprPrec := LeanEval.Topology.ClassificationOfSurfaces.instReprProjectivePlaneEdge.repr }

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instFintypeProjectivePlaneEdge : Fintype ProjectivePlaneEdge

Equations

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

inductive LeanEval.Topology.ClassificationOfSurfaces.MobiusStripEdge : Type

Edge names for the Mobius-strip example.

• a : MobiusStripEdge
• h : MobiusStripEdge

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instDecidableEqMobiusStripEdge : DecidableEq MobiusStripEdge

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.instReprMobiusStripEdge.repr : MobiusStripEdge → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instReprMobiusStripEdge : Repr MobiusStripEdge

Equations

• LeanEval.Topology.ClassificationOfSurfaces.instReprMobiusStripEdge = { reprPrec := LeanEval.Topology.ClassificationOfSurfaces.instReprMobiusStripEdge.repr }

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instFintypeMobiusStripEdge : Fintype MobiusStripEdge

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.diskCellComplex : SurfaceCellComplex

One-face boundary-word presentation for the disk.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.annulusCellComplex : SurfaceCellComplex

One-face boundary-word presentation for the annulus: d₀ c₀ d₀⁻¹ d₁ c₁ d₁⁻¹.

The dᵢ pairs are internal seams and the single occurrences cᵢ are the two boundary contours. This is a renaming of the genus-zero, two-contour normal form from Gallier--Xu Definition 6.5.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.torusCellComplex : SurfaceCellComplex

One-face boundary-word presentation for the torus: a b a⁻¹ b⁻¹.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.projectivePlaneCellComplex : SurfaceCellComplex

One-face boundary-word presentation for the projective plane: a a.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.mobiusStripCellComplex : SurfaceCellComplex

One-face boundary-word presentation for the Mobius strip: a a h.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.annulusCellComplex_boundary : annulusCellComplex.boundary PUnit.unit = [SurfaceCellComplex.SignedDart.pos AnnulusEdge.d₀, SurfaceCellComplex.SignedDart.pos AnnulusEdge.c₀, SurfaceCellComplex.SignedDart.neg AnnulusEdge.d₀, SurfaceCellComplex.SignedDart.pos AnnulusEdge.d₁, SurfaceCellComplex.SignedDart.pos AnnulusEdge.c₁, SurfaceCellComplex.SignedDart.neg AnnulusEdge.d₁]

The annulus has the full length-six, two-contour boundary word.

theorem LeanEval.Topology.ClassificationOfSurfaces.projectivePlaneCellComplex_isSurfaceValid : projectivePlaneCellComplex.IsSurfaceValid

Regression check: edge-orbit multiplicity accepts the non-orientable word a a.

Occurrence-pairing validity

theorem LeanEval.Topology.ClassificationOfSurfaces.diskCellComplex_occurrencePairingValid : diskCellComplex.OccurrencePairingValid

The disk word has one boundary occurrence and no internal pairings.

theorem LeanEval.Topology.ClassificationOfSurfaces.annulusCellComplex_occurrencePairingValid : annulusCellComplex.OccurrencePairingValid

The corrected annulus word has two internal seam pairs and two boundary occurrences.

theorem LeanEval.Topology.ClassificationOfSurfaces.torusCellComplex_occurrencePairingValid : torusCellComplex.OccurrencePairingValid

The torus word pairs both of its edge names internally.

theorem LeanEval.Topology.ClassificationOfSurfaces.projectivePlaneCellComplex_occurrencePairingValid : projectivePlaneCellComplex.OccurrencePairingValid

The two copies of the projective-plane edge form one internal pair.

theorem LeanEval.Topology.ClassificationOfSurfaces.mobiusStripCellComplex_occurrencePairingValid : mobiusStripCellComplex.OccurrencePairingValid

The Mobius-strip word has one internal pair and one boundary occurrence.

theorem LeanEval.Topology.ClassificationOfSurfaces.diskCellComplex_isSurfaceValid : diskCellComplex.IsSurfaceValid

Incidence validity of the disk presentation.

theorem LeanEval.Topology.ClassificationOfSurfaces.annulusCellComplex_isSurfaceValid : annulusCellComplex.IsSurfaceValid

Incidence validity of the corrected annulus presentation.

theorem LeanEval.Topology.ClassificationOfSurfaces.torusCellComplex_isSurfaceValid : torusCellComplex.IsSurfaceValid

Incidence validity of the torus presentation.

theorem LeanEval.Topology.ClassificationOfSurfaces.mobiusStripCellComplex_isSurfaceValid : mobiusStripCellComplex.IsSurfaceValid

Incidence validity of the Mobius-strip presentation.

def LeanEval.Topology.ClassificationOfSurfaces.oneTriangleTriangulation : FiniteSurfaceTriangulation PUnit.{1}

A minimal one-triangle triangulation of PUnit, used only to test the data conversion API.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.reversedSideTriangulation : FiniteSurfaceTriangulation PUnit.{1}

A one-triangle fixture with one reversed side, used to test oriented conversion.

Equations

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