Polygonal realization of Gallier--Xu P1

The boundary of every source face is assigned weight two at occurrences of the subdivided edge and weight one everywhere else. WeightedCircle turns those weights into the exact boundary homeomorphism required by P1, and radial extension gives the corresponding disk homeomorphism.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.dartWeight {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) : ℕ

The number of target sides replacing one source dart.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.dartWeight a d = if LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.edgeOfDart d = a then 2 else 1

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceWeights (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) : List ℕ

The P1 subdivision weights around one face boundary.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceWeights_length (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) : (faceWeights P a f).length = (P.boundary f).length

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceWeights_positive (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) : WeightedCircle.Positive (faceWeights P a f)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceWeights_ne_nil (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) (validP : P.IsSurfaceValid) : faceWeights P a f ≠ []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.length_expandDart_eq_dartWeight {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) : (expandDart a d).length = dartWeight a d

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord_length_eq_sum_map_dartWeight {n : ℕ} (a : Fin n) (word : List (SurfaceCellComplex.SignedDart (Fin n))) : (expandWord a word).length = (List.map (dartWeight a) word).sum

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord_length_eq_sum_faceWeights (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) : (expandWord a (P.boundary f)).length = (faceWeights P a f).sum

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceWeights_sum (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) : (faceWeights P a f).sum = ((expand P a).boundary ((faceEquiv P a) f)).length

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedStartIndex (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) (i : Fin (P.boundary f).length) : Fin ((expand P a).boundary ((faceEquiv P a) f)).length

The first target side replacing source side i.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedStartIndex_val (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) (i : Fin (P.boundary f).length) : ↑(expandedStartIndex P a f i) = (List.take (↑i) (faceWeights P a f)).sum

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.firstExpandedOccurrence (P : FiniteCyclicPresentation) (a : P.Edge) (o : P.BoundaryOccurrence) : (expand P a).BoundaryOccurrence

Transport a source occurrence to the first target occurrence in its expanded block.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord_getElem_expandedStart {n : ℕ} (a : Fin n) (word : List (SurfaceCellComplex.SignedDart (Fin n))) (i : Fin word.length) : (expandWord a word)[(List.take (↑i) (List.map (dartWeight a) word)).sum]? = (expandDart a (word.get i))[0]?

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandDart_length_pos {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) : 0 < (expandDart a d).length

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.dartWeight_eq_two_iff {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) : dartWeight a d = 2 ↔ edgeOfDart d = a

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.dartWeight_eq_one_iff {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) : dartWeight a d = 1 ↔ edgeOfDart d ≠ a

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord_getElem_expandedOffset {n : ℕ} (a : Fin n) (word : List (SurfaceCellComplex.SignedDart (Fin n))) (i : Fin word.length) (k : ℕ) (hk : k < (expandDart a (word.get i)).length) : (expandWord a word)[(List.take (↑i) (List.map (dartWeight a) word)).sum + k]? = (expandDart a (word.get i))[k]?

More generally, lookup inside an expanded block agrees with lookup in the substituted dart-word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.firstExpandedOccurrence_dart (P : FiniteCyclicPresentation) (a : P.Edge) (o : P.BoundaryOccurrence) : (firstExpandedOccurrence P a o).dart = (expandDart a o.dart).get ⟨0, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.sum_take_add_get_le_sum {weights : List ℕ} (i : Fin weights.length) : (List.take (↑i) weights).sum + weights.get i ≤ weights.sum

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.sum_take_add_one_lt_sum_of_get_eq_two {weights : List ℕ} (i : Fin weights.length) (hget : weights.get i = 2) : (List.take (↑i) weights).sum + 1 < weights.sum

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.BlockPosition (weights : List ℕ) : Type

A position in the concatenation of blocks whose lengths are weights.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.BlockPosition weights = ((i : Fin weights.length) × Fin (weights.get i))

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.blockPosition {weights : List ℕ} (p : BlockPosition weights) : ℕ

Linear position of a block-local index.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.blockPosition p = (List.take (↑p.fst) weights).sum + ↑p.snd

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.blockPosition_injective (weights : List ℕ) : Function.Injective blockPosition

Distinct block-local positions have distinct linear positions.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceWeights_get (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) (i : Fin (P.boundary f).length) : (faceWeights P a f).get (Fin.cast ⋯ i) = dartWeight a ((P.boundary f).get i)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedOffsetIndex (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) (i : Fin (P.boundary f).length) (k : Fin (dartWeight a ((P.boundary f).get i))) : Fin ((expand P a).boundary ((faceEquiv P a) f)).length

A target-side index inside the expanded block of source side i.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedOffsetIndex_val (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) (i : Fin (P.boundary f).length) (k : Fin (dartWeight a ((P.boundary f).get i))) : ↑(expandedOffsetIndex P a f i k) = (List.take (↑i) (faceWeights P a f)).sum + ↑k

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.ExpandedSourcePosition (P : FiniteCyclicPresentation) (a : P.Edge) : Type

A source occurrence together with one of the one or two target sides replacing it.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedOccurrenceAt (P : FiniteCyclicPresentation) (a : P.Edge) (p : ExpandedSourcePosition P a) : (expand P a).BoundaryOccurrence

Transport a block-local source position to its target boundary occurrence.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedOccurrenceAt_injective (P : FiniteCyclicPresentation) (a : P.Edge) : Function.Injective (expandedOccurrenceAt P a)

The block-local occurrence transport is injective: expanded blocks never overlap.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedOccurrenceAt_dart (P : FiniteCyclicPresentation) (a : P.Edge) (p : ExpandedSourcePosition P a) : (expandedOccurrenceAt P a p).dart = (expandDart a p.fst.dart).get (Fin.cast ⋯ p.snd)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.isBoundaryEdge_expand_castSucc_iff (P : FiniteCyclicPresentation) (a e : P.Edge) : (expand P a).IsBoundaryEdge (Fin.castSucc e) ↔ P.IsBoundaryEdge e

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.isBoundaryEdge_expand_freshEdge_iff (P : FiniteCyclicPresentation) (a : P.Edge) : (expand P a).IsBoundaryEdge (freshEdge P.edgeCount) ↔ P.IsBoundaryEdge a

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedSubedge {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) (k : Fin (dartWeight a d)) : Fin (n + 1)

The target edge at a block-local offset.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.isBoundaryEdge_expandedSubedge_iff (P : FiniteCyclicPresentation) (a : P.Edge) (d : P.Dart) (k : Fin (dartWeight a d)) : (expand P a).IsBoundaryEdge (expandedSubedge a d k) ↔ P.IsBoundaryEdge (edgeOfDart d)

Each target subedge has the same boundary/internal status as its source edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedOccurrenceAt_not_boundary (P : FiniteCyclicPresentation) (a : P.Edge) (p : ExpandedSourcePosition P a) (h : ¬P.IsBoundaryEdge p.fst.edge) : ¬(expand P a).IsBoundaryEdge (expandedOccurrenceAt P a p).edge

Every target subedge has the same boundary/internal status as its source edge.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.zeroOffset {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) : Fin (dartWeight a d)

The first local target-side offset always exists.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.zeroOffset a d = ⟨0, ⋯⟩

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.oneOffset {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) (hselected : edgeOfDart d = a) : Fin (dartWeight a d)

A selected source side has a second local target-side offset.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.oneOffset a d hselected = ⟨1, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.dartWeight_flip {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) : dartWeight a d.flip = dartWeight a d

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedSubdart {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) (k : Fin (dartWeight a d)) : SurfaceCellComplex.SignedDart (Fin (n + 1))

The signed target dart at a block-local offset.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedSubdart a d k = (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandDart a d)[↑k]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.reverseOffset {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) (k : Fin (dartWeight a d)) : Fin (dartWeight a d.flip)

Reverse a block-local offset after reversing the source dart.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.reverseOffset a d k = ⟨LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.dartWeight a d - (↑k + 1), ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedSubdart_flip_reverseOffset {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) (k : Fin (dartWeight a d)) : expandedSubdart a d.flip (reverseOffset a d k) = (expandedSubdart a d k).flip

Reversing a source dart reverses the expanded block and flips its signed darts.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.BoundaryPairing.target_edge_eq_source_edge {P : FiniteCyclicPresentation} (pairing : P.BoundaryPairing) : pairing.target.edge = pairing.source.edge

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedOccurrenceAt_dart_eq_expandedSubdart (P : FiniteCyclicPresentation) (a : P.Edge) (p : ExpandedSourcePosition P a) : (expandedOccurrenceAt P a p).dart = expandedSubdart a p.fst.dart p.snd

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.samePairedOffset {P : FiniteCyclicPresentation} (a : P.Edge) (pairing : P.BoundaryPairing) (hcompatible : pairing.target.dart = pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) : Fin (dartWeight a pairing.target.dart)

Transport a block-local offset across an equal-dart pairing.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.samePairedOffset a pairing hcompatible k = Fin.cast ⋯ k

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.oppositePairedOffset {P : FiniteCyclicPresentation} (a : P.Edge) (pairing : P.BoundaryPairing) (hcompatible : pairing.target.dart = SurfaceCellComplex.SignedDart.flip pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) : Fin (dartWeight a pairing.target.dart)

Transport a block-local offset across a flipped-dart pairing.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedSubdart_cast_eq {n : ℕ} (a : Fin n) {d₁ d₂ : SurfaceCellComplex.SignedDart (Fin n)} (h : d₂ = d₁) (k : Fin (dartWeight a d₁)) : expandedSubdart a d₂ (Fin.cast ⋯ k) = expandedSubdart a d₁ k

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedSubdart_cast_flip {n : ℕ} (a : Fin n) {d₁ d₂ : SurfaceCellComplex.SignedDart (Fin n)} (h : d₂ = d₁.flip) (k : Fin (dartWeight a d₁)) : expandedSubdart a d₂ (Fin.cast ⋯ (reverseOffset a d₁ k)) = (expandedSubdart a d₁ k).flip

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedSubdart_samePairedOffset {P : FiniteCyclicPresentation} (a : P.Edge) (pairing : P.BoundaryPairing) (hcompatible : pairing.target.dart = pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) : expandedSubdart a pairing.target.dart (samePairedOffset a pairing hcompatible k) = expandedSubdart a pairing.source.dart k

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedSubdart_oppositePairedOffset {P : FiniteCyclicPresentation} (a : P.Edge) (pairing : P.BoundaryPairing) (hcompatible : pairing.target.dart = SurfaceCellComplex.SignedDart.flip pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) : expandedSubdart a pairing.target.dart (oppositePairedOffset a pairing hcompatible k) = (expandedSubdart a pairing.source.dart k).flip

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedPairingSame (P : FiniteCyclicPresentation) (a : P.Edge) (pairing : P.BoundaryPairing) (hcompatible : pairing.target.dart = pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) : (expand P a).BoundaryPairing

Each same-direction old pairing expands to corresponding target-subedge pairings.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedPairingOpposite (P : FiniteCyclicPresentation) (a : P.Edge) (pairing : P.BoundaryPairing) (hcompatible : pairing.target.dart = SurfaceCellComplex.SignedDart.flip pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) : (expand P a).BoundaryPairing

Each opposite-direction old pairing expands to reversed target-subedge pairings.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.secondExpandedIndex (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) (i : Fin (P.boundary f).length) (hselected : edgeOfDart ((P.boundary f).get i) = a) : Fin ((expand P a).boundary ((faceEquiv P a) f)).length

The second target side replacing a selected source occurrence.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.secondExpandedIndex_val (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) (i : Fin (P.boundary f).length) (hselected : edgeOfDart ((P.boundary f).get i) = a) : ↑(secondExpandedIndex P a f i hselected) = (List.take (↑i) (faceWeights P a f)).sum + 1

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.secondExpandedOccurrence (P : FiniteCyclicPresentation) (a : P.Edge) (o : P.BoundaryOccurrence) (hselected : o.edge = a) : (expand P a).BoundaryOccurrence

Transport a selected source occurrence to the second occurrence in its expanded block.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.secondExpandedOccurrence_dart (P : FiniteCyclicPresentation) (a : P.Edge) (o : P.BoundaryOccurrence) (hselected : o.edge = a) : (secondExpandedOccurrence P a o hselected).dart = (expandDart a o.dart).get ⟨1, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceCircleHomeomorph (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (f : P.Face) : Circle ≃ₜ Circle

The exact weighted homeomorphism between the source and P1-expanded face boundaries.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceHomeomorph (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (f : P.Face) : PolygonCell (P.boundary f).length ≃ₜ PolygonCell ((expand P a).boundary ((faceEquiv P a) f)).length

Radially extend the weighted boundary map to the whole face disk.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) : P.PolygonalPreRealization ≃ₜ (expand P a).PolygonalPreRealization

P1 acts facewise on the polygonal pre-realization.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph_apply_fst (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (x : P.PolygonalPreRealization) : ((preHomeomorph P a validP) x).fst = (faceEquiv P a) x.fst

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceHomeomorph_ofCircle (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (f : P.Face) (z : Circle) : (faceHomeomorph P a validP f) ((PolygonCell.ofCircle (P.boundary f).length) z) = (PolygonCell.ofCircle ((expand P a).boundary ((faceEquiv P a) f)).length) ((faceCircleHomeomorph P a validP f) z)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceHomeomorph_side (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (f : P.Face) (i : Fin (P.boundary f).length) (t : ↑unitInterval) : (faceHomeomorph P a validP f) ((PolygonCell.side i) t) = (PolygonCell.ofCircle ((expand P a).boundary ((faceEquiv P a) f)).length) (Circle.exp (2 * Real.pi / ↑((expand P a).boundary ((faceEquiv P a) f)).length * (↑(List.take (↑i) (faceWeights P a f)).sum + ↑((faceWeights P a f).get (Fin.cast ⋯ i)) * ↑t)))

Exact boundary-coordinate formula for the facewise P1 map.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceHomeomorph_side_of_not_selected (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (f : P.Face) (i : Fin (P.boundary f).length) (hnot : edgeOfDart ((P.boundary f).get i) ≠ a) (t : ↑unitInterval) : (faceHomeomorph P a validP f) ((PolygonCell.side i) t) = (PolygonCell.side (expandedStartIndex P a f i)) t

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.firstHalfParameter (t : ↑unitInterval) (h : ↑t ≤ 1 / 2) : ↑unitInterval

Rescale the first half of a source side to a complete target side.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.firstHalfParameter t h = ⟨2 * ↑t, ⋯⟩

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.secondHalfParameter (t : ↑unitInterval) (h : 1 / 2 ≤ ↑t) : ↑unitInterval

Rescale the second half of a source side to a complete target side.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.secondHalfParameter t h = ⟨2 * ↑t - 1, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.firstHalfParameter_val (t : ↑unitInterval) (h : ↑t ≤ 1 / 2) : ↑(firstHalfParameter t h) = 2 * ↑t

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.secondHalfParameter_val (t : ↑unitInterval) (h : 1 / 2 ≤ ↑t) : ↑(secondHalfParameter t h) = 2 * ↑t - 1

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceHomeomorph_side_firstHalf (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (f : P.Face) (i : Fin (P.boundary f).length) (hselected : edgeOfDart ((P.boundary f).get i) = a) (t : ↑unitInterval) (ht : ↑t ≤ 1 / 2) : (faceHomeomorph P a validP f) ((PolygonCell.side i) t) = (PolygonCell.side (expandedStartIndex P a f i)) (firstHalfParameter t ht)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceHomeomorph_side_secondHalf (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (f : P.Face) (i : Fin (P.boundary f).length) (hselected : edgeOfDart ((P.boundary f).get i) = a) (t : ↑unitInterval) (ht : 1 / 2 ≤ ↑t) : (faceHomeomorph P a validP f) ((PolygonCell.side i) t) = (PolygonCell.side (secondExpandedIndex P a f i hselected)) (secondHalfParameter t ht)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph_occurrenceSide_of_not_selected (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (o : P.BoundaryOccurrence) (hnot : o.edge ≠ a) (t : ↑unitInterval) : (preHomeomorph P a validP) ((P.occurrenceSide o).point t) = ((expand P a).occurrenceSide (expandedOccurrenceAt P a ⟨o, zeroOffset a o.dart⟩)).point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph_occurrenceSide_firstHalf (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (o : P.BoundaryOccurrence) (hselected : o.edge = a) (t : ↑unitInterval) (ht : ↑t ≤ 1 / 2) : (preHomeomorph P a validP) ((P.occurrenceSide o).point t) = ((expand P a).occurrenceSide (expandedOccurrenceAt P a ⟨o, zeroOffset a o.dart⟩)).point (firstHalfParameter t ht)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph_occurrenceSide_secondHalf (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (o : P.BoundaryOccurrence) (hselected : o.edge = a) (t : ↑unitInterval) (ht : 1 / 2 ≤ ↑t) : (preHomeomorph P a validP) ((P.occurrenceSide o).point t) = ((expand P a).occurrenceSide (expandedOccurrenceAt P a ⟨o, oneOffset a o.dart hselected⟩)).point (secondHalfParameter t ht)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.samePairedOffset_val {P : FiniteCyclicPresentation} (a : P.Edge) (pairing : P.BoundaryPairing) (hcompatible : pairing.target.dart = pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) : ↑(samePairedOffset a pairing hcompatible k) = ↑k

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.oppositePairedOffset_val {P : FiniteCyclicPresentation} (a : P.Edge) (pairing : P.BoundaryPairing) (hcompatible : pairing.target.dart = SurfaceCellComplex.SignedDart.flip pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) : ↑(oppositePairedOffset a pairing hcompatible k) = dartWeight a pairing.source.dart - (↑k + 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.symm_firstHalfParameter (t : ↑unitInterval) (ht : ↑t ≤ 1 / 2) : unitInterval.symm (firstHalfParameter t ht) = secondHalfParameter (unitInterval.symm t) ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.symm_secondHalfParameter (t : ↑unitInterval) (ht : 1 / 2 ≤ ↑t) : unitInterval.symm (secondHalfParameter t ht) = firstHalfParameter (unitInterval.symm t) ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedPairingSame_related (P : FiniteCyclicPresentation) (a : P.Edge) (validQ : (expand P a).IsSurfaceValid) (pairing : P.BoundaryPairing) (hcompatible : pairing.target.dart = pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) (u : ↑unitInterval) : ((expand P a).PolygonalGluingRel validQ) (((expand P a).occurrenceSide (expandedOccurrenceAt P a ⟨pairing.source, k⟩)).point u) (((expand P a).occurrenceSide (expandedOccurrenceAt P a ⟨pairing.target, samePairedOffset a pairing hcompatible k⟩)).point u)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedPairingOpposite_related (P : FiniteCyclicPresentation) (a : P.Edge) (validQ : (expand P a).IsSurfaceValid) (pairing : P.BoundaryPairing) (hcompatible : pairing.target.dart = SurfaceCellComplex.SignedDart.flip pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) (u : ↑unitInterval) : ((expand P a).PolygonalGluingRel validQ) (((expand P a).occurrenceSide (expandedOccurrenceAt P a ⟨pairing.source, k⟩)).point u) (((expand P a).occurrenceSide (expandedOccurrenceAt P a ⟨pairing.target, oppositePairedOffset a pairing hcompatible k⟩)).point (unitInterval.symm u))

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph_generator_related (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (pairing : P.BoundaryPairing) (t : ↑unitInterval) : ((expand P a).PolygonalGluingRel ⋯) ((preHomeomorph P a validP) (pairing.identification.source.point t)) ((preHomeomorph P a validP) (pairing.identification.target.point (pairing.identification.parameter t)))

The facewise P1 map sends every source gluing generator into the target generated relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.card_expandedSourcePosition (P : FiniteCyclicPresentation) (a : P.Edge) : Fintype.card (ExpandedSourcePosition P a) = Fintype.card (expand P a).BoundaryOccurrence

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedOccurrenceEquiv (P : FiniteCyclicPresentation) (a : P.Edge) : ExpandedSourcePosition P a ≃ (expand P a).BoundaryOccurrence

Expanded source blocks enumerate all target boundary occurrences.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedOccurrenceEquiv_apply (P : FiniteCyclicPresentation) (a : P.Edge) (p : ExpandedSourcePosition P a) : (expandedOccurrenceEquiv P a) p = expandedOccurrenceAt P a p

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractExpandedEdge {n : ℕ} (a : Fin n) : Fin (n + 1) → Fin n

Contract either target subedge back to its source edge.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractExpandedEdge a i = Fin.lastCases a id i

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractExpandedEdge_castSucc {n : ℕ} (a e : Fin n) : contractExpandedEdge a e.castSucc = e

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractExpandedEdge_freshEdge {n : ℕ} (a : Fin n) : contractExpandedEdge a (freshEdge n) = a

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractExpandedEdge_expandedSubedge {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) (k : Fin (dartWeight a d)) : contractExpandedEdge a (expandedSubedge a d k) = edgeOfDart d

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.sourceEdge_eq_of_expandedSubedge_eq {n : ℕ} (a : Fin n) {d e : SurfaceCellComplex.SignedDart (Fin n)} {k : Fin (dartWeight a d)} {l : Fin (dartWeight a e)} (h : expandedSubedge a d k = expandedSubedge a e l) : edgeOfDart d = edgeOfDart e

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedSubedge_injective_offset {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) : Function.Injective (expandedSubedge a d)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedOccurrenceAt_edge (P : FiniteCyclicPresentation) (a : P.Edge) (p : ExpandedSourcePosition P a) : (expandedOccurrenceAt P a p).edge = expandedSubedge a p.fst.dart p.snd

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedSourcePosition_eq_of_fst_eq_of_subedge_eq (P : FiniteCyclicPresentation) (a : P.Edge) (p q : ExpandedSourcePosition P a) (hfst : p.fst = q.fst) (hedge : expandedSubedge a p.fst.dart p.snd = expandedSubedge a q.fst.dart q.snd) : p = q

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandedSourcePosition_mk_transport (P : FiniteCyclicPresentation) (a : P.Edge) {o o' : P.BoundaryOccurrence} (h : o = o') (k : Fin (dartWeight a o'.dart)) : ⟨o, ⋯ ▸ k⟩ = ⟨o', k⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.BoundaryPairing.direction_eq_of_source_target_eq {P : FiniteCyclicPresentation} (p q : P.BoundaryPairing) (hsource : p.source = q.source) (htarget : p.target = q.target) : p.direction = q.direction

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.BoundaryPairing.eq_of_source_target_direction_eq {P : FiniteCyclicPresentation} (p q : P.BoundaryPairing) (hsource : p.source = q.source) (htarget : p.target = q.target) (hdirection : p.direction = q.direction) : p = q

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.exists_eq_expandedPairing (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (q : (expand P a).BoundaryPairing) : (∃ (r : P.BoundaryPairing) (_ : r.direction = PolygonGluing.ParameterDirection.same) (hcompatible : r.target.dart = r.source.dart) (k : Fin (dartWeight a r.source.dart)), q = expandedPairingSame P a r hcompatible k) ∨ ∃ (r : P.BoundaryPairing) (_ : r.direction = PolygonGluing.ParameterDirection.opposite) (hcompatible : r.target.dart = SurfaceCellComplex.SignedDart.flip r.source.dart) (k : Fin (dartWeight a r.source.dart)), q = expandedPairingOpposite P a r hcompatible k

Every target pairing is one of the subedge pairings expanded from a unique old pairing.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.dartWeight_pos {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) : 0 < dartWeight a d

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.unexpandParameter {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) (k : Fin (dartWeight a d)) (u : ↑unitInterval) : ↑unitInterval

Convert a target subedge-local parameter back to the original source-side parameter.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.unexpandParameter_val {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) (k : Fin (dartWeight a d)) (u : ↑unitInterval) : ↑(unexpandParameter a d k u) = (↑↑k + ↑u) / ↑(dartWeight a d)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceHomeomorph_side_unexpand (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (f : P.Face) (i : Fin (P.boundary f).length) (k : Fin (dartWeight a ((P.boundary f).get i))) (u : ↑unitInterval) : (faceHomeomorph P a validP f) ((PolygonCell.side i) (unexpandParameter a ((P.boundary f).get i) k u)) = (PolygonCell.side (expandedOffsetIndex P a f i k)) u

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph_occurrenceSide_unexpand (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (p : ExpandedSourcePosition P a) (u : ↑unitInterval) : (preHomeomorph P a validP) ((P.occurrenceSide p.fst).point (unexpandParameter a p.fst.dart p.snd u)) = ((expand P a).occurrenceSide (expandedOccurrenceAt P a p)).point u

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph_symm_expandedOccurrenceAt (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (p : ExpandedSourcePosition P a) (u : ↑unitInterval) : (preHomeomorph P a validP).symm (((expand P a).occurrenceSide (expandedOccurrenceAt P a p)).point u) = (P.occurrenceSide p.fst).point (unexpandParameter a p.fst.dart p.snd u)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.unexpandParameter_cast_eq {n : ℕ} (a : Fin n) {d₁ d₂ : SurfaceCellComplex.SignedDart (Fin n)} (h : d₂ = d₁) (k : Fin (dartWeight a d₁)) (u : ↑unitInterval) : unexpandParameter a d₂ (Fin.cast ⋯ k) u = unexpandParameter a d₁ k u

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.unexpandParameter_flip_reverse {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) (k : Fin (dartWeight a d)) (u : ↑unitInterval) : unexpandParameter a d.flip (reverseOffset a d k) (unitInterval.symm u) = unitInterval.symm (unexpandParameter a d k u)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.unexpandParameter_samePairedOffset {P : FiniteCyclicPresentation} (a : P.Edge) (pairing : P.BoundaryPairing) (hcompatible : pairing.target.dart = pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) (u : ↑unitInterval) : unexpandParameter a pairing.target.dart (samePairedOffset a pairing hcompatible k) u = unexpandParameter a pairing.source.dart k u

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.unexpandParameter_oppositePairedOffset {P : FiniteCyclicPresentation} (a : P.Edge) (pairing : P.BoundaryPairing) (hcompatible : pairing.target.dart = SurfaceCellComplex.SignedDart.flip pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) (u : ↑unitInterval) : unexpandParameter a pairing.target.dart (oppositePairedOffset a pairing hcompatible k) (unitInterval.symm u) = unitInterval.symm (unexpandParameter a pairing.source.dart k u)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph_symm_expandedPairingSame_generator_related (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (pairing : P.BoundaryPairing) (hdirection : pairing.direction = PolygonGluing.ParameterDirection.same) (hcompatible : pairing.target.dart = pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) (u : ↑unitInterval) : (P.PolygonalGluingRel validP) ((preHomeomorph P a validP).symm ((expandedPairingSame P a pairing hcompatible k).identification.source.point u)) ((preHomeomorph P a validP).symm ((expandedPairingSame P a pairing hcompatible k).identification.target.point ((expandedPairingSame P a pairing hcompatible k).identification.parameter u)))

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph_symm_expandedPairingOpposite_generator_related (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (pairing : P.BoundaryPairing) (hdirection : pairing.direction = PolygonGluing.ParameterDirection.opposite) (hcompatible : pairing.target.dart = SurfaceCellComplex.SignedDart.flip pairing.source.dart) (k : Fin (dartWeight a pairing.source.dart)) (u : ↑unitInterval) : (P.PolygonalGluingRel validP) ((preHomeomorph P a validP).symm ((expandedPairingOpposite P a pairing hcompatible k).identification.source.point u)) ((preHomeomorph P a validP).symm ((expandedPairingOpposite P a pairing hcompatible k).identification.target.point ((expandedPairingOpposite P a pairing hcompatible k).identification.parameter u)))

Descent to the faithful polygonal quotient

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph_symm_generator_related (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (pairing : (expand P a).BoundaryPairing) (t : ↑unitInterval) : (P.PolygonalGluingRel validP) ((preHomeomorph P a validP).symm (pairing.identification.source.point t)) ((preHomeomorph P a validP).symm (pairing.identification.target.point (pairing.identification.parameter t)))

The inverse facewise map sends every target gluing generator into the source generated relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph_related (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) {x y : P.PolygonalPreRealization} (hxy : (P.PolygonalGluingRel validP) x y) : ((expand P a).PolygonalGluingRel ⋯) ((preHomeomorph P a validP) x) ((preHomeomorph P a validP) y)

The facewise P1 homeomorphism preserves the complete source gluing relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph_symm_related (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) {x y : (expand P a).PolygonalPreRealization} (hxy : ((expand P a).PolygonalGluingRel ⋯) x y) : (P.PolygonalGluingRel validP) ((preHomeomorph P a validP).symm x) ((preHomeomorph P a validP).symm y)

The inverse facewise P1 homeomorphism preserves the complete target gluing relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.preHomeomorph_related_iff (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) (x y : P.PolygonalPreRealization) : (P.PolygonalGluingRel validP) x y ↔ ((expand P a).PolygonalGluingRel ⋯) ((preHomeomorph P a validP) x) ((preHomeomorph P a validP) y)

The selected P1 pre-realization homeomorphism identifies the two generated gluing relations exactly.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.realizationHomeomorph (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) : P.PolygonalRealization validP ≃ₜ (expand P a).PolygonalRealization ⋯

Canonical P1 expansion preserves the faithful polygonal realization.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.polygonallyEquivalent (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) : P.PolygonallyEquivalent (expand P a) validP ⋯

Propositional realization-invariance form for the canonical P1 expansion.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1Subdivision.preservesPolygonalRealization : PreservesPolygonalRealization

Every P1 subdivision, including signed relabeling of the canonical target, preserves the faithful polygonal realization.