Gallier--Xu P1 edge subdivision

This file formalizes the first primitive subdivision from Gallier--Xu, Definition 6.3. For a chosen oriented edge a, P1 globally replaces

• a by b c, and
• a⁻¹ by c⁻¹ b⁻¹.

The canonical finite implementation retains every old edge name through Fin.castSucc, uses the retained name of a for b, and uses Fin.last for the fresh edge c. A contraction deletes the fresh edge and sends every retained edge back to its old name. This contraction is a left inverse on words, including cyclic words, so P1 both preserves and reflects cyclic rotation. The selected underlying edge uses its positive stored orientation canonically. The SignedPresentationIso in P1Subdivision allows the two target edge names to be renamed and reoriented when a different orientation convention is desired.

The presentation-level construction preserves face positions, copies the multiplicity of a to both subdivided edges, and preserves ordinary validity, face-incidence connectivity, and IsGallierValid. P1Subdivision closes the canonical construction under signed presentation isomorphism.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.castSuccDart {n : ℕ} : SurfaceCellComplex.SignedDart (Fin n) → SurfaceCellComplex.SignedDart (Fin (n + 1))

Retain an old signed edge in the enlarged edge type.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.castSuccDart_pos {n : ℕ} (e : Fin n) : castSuccDart (SurfaceCellComplex.SignedDart.pos e) = SurfaceCellComplex.SignedDart.pos e.castSucc

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.castSuccDart_neg {n : ℕ} (e : Fin n) : castSuccDart (SurfaceCellComplex.SignedDart.neg e) = SurfaceCellComplex.SignedDart.neg e.castSucc

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.edgeOfDart_castSuccDart {n : ℕ} (d : SurfaceCellComplex.SignedDart (Fin n)) : edgeOfDart (castSuccDart d) = (edgeOfDart d).castSucc

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.freshEdge (n : ℕ) : Fin (n + 1)

The fresh second subedge in the canonical P1 expansion.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.freshEdge n = Fin.last n

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

The retained first subedge in the canonical P1 expansion.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.firstSubedge a = a.castSucc

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.firstSubedge_ne_freshEdge {n : ℕ} (a : Fin n) : firstSubedge a ≠ freshEdge n

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandDart {n : ℕ} (a : Fin n) : SurfaceCellComplex.SignedDart (Fin n) → List (SurfaceCellComplex.SignedDart (Fin (n + 1)))

Substitute one signed occurrence according to Gallier--Xu P1.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandDart_pos_self {n : ℕ} (a : Fin n) : expandDart a (SurfaceCellComplex.SignedDart.pos a) = [SurfaceCellComplex.SignedDart.pos (firstSubedge a), SurfaceCellComplex.SignedDart.pos (freshEdge n)]

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandDart_neg_self {n : ℕ} (a : Fin n) : expandDart a (SurfaceCellComplex.SignedDart.neg a) = [SurfaceCellComplex.SignedDart.neg (freshEdge n), SurfaceCellComplex.SignedDart.neg (firstSubedge a)]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandDart_pos_of_ne {n : ℕ} {a e : Fin n} (h : e ≠ a) : expandDart a (SurfaceCellComplex.SignedDart.pos e) = [SurfaceCellComplex.SignedDart.pos e.castSucc]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandDart_neg_of_ne {n : ℕ} {a e : Fin n} (h : e ≠ a) : expandDart a (SurfaceCellComplex.SignedDart.neg e) = [SurfaceCellComplex.SignedDart.neg e.castSucc]

@[simp]

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

P1 sends the opposite dart to the inverse of the substituted word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.castSuccDart_mem_expandDart {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) : castSuccDart d ∈ expandDart a d

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractDart {n : ℕ} : SurfaceCellComplex.SignedDart (Fin (n + 1)) → Option (SurfaceCellComplex.SignedDart (Fin n))

Contract one target dart: discard the fresh edge and retain every old edge.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractDart_pos_castSucc {n : ℕ} (e : Fin n) : contractDart (SurfaceCellComplex.SignedDart.pos e.castSucc) = some (SurfaceCellComplex.SignedDart.pos e)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractDart_neg_castSucc {n : ℕ} (e : Fin n) : contractDart (SurfaceCellComplex.SignedDart.neg e.castSucc) = some (SurfaceCellComplex.SignedDart.neg e)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractDart_pos_freshEdge (n : ℕ) : contractDart (SurfaceCellComplex.SignedDart.pos (freshEdge n)) = none

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractDart_neg_freshEdge (n : ℕ) : contractDart (SurfaceCellComplex.SignedDart.neg (freshEdge n)) = none

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord {n : ℕ} (a : Fin n) (word : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))

Apply P1 simultaneously to every occurrence in a linear representative of a cyclic word.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord a word = List.flatMap (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandDart a) word

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractWord {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) : List (SurfaceCellComplex.SignedDart (Fin n))

Contract a P1 word by deleting the fresh subedge.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractWord word = List.filterMap LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractDart word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord_nil {n : ℕ} (a : Fin n) : expandWord a [] = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord_cons {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) (word : List (SurfaceCellComplex.SignedDart (Fin n))) : expandWord a (d :: word) = expandDart a d ++ expandWord a word

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord_singleton {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) : expandWord a [d] = expandDart a d

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord_append {n : ℕ} (a : Fin n) (left right : List (SurfaceCellComplex.SignedDart (Fin n))) : expandWord a (left ++ right) = expandWord a left ++ expandWord a right

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractWord_nil {n : ℕ} : contractWord [] = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractWord_append {n : ℕ} (left right : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) : contractWord (left ++ right) = contractWord left ++ contractWord right

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractWord_expandDart {n : ℕ} (a : Fin n) (d : SurfaceCellComplex.SignedDart (Fin n)) : contractWord (expandDart a d) = [d]

Contracting one substituted occurrence returns that occurrence.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractWord_expandWord {n : ℕ} (a : Fin n) (word : List (SurfaceCellComplex.SignedDart (Fin n))) : contractWord (expandWord a word) = word

Contracting the global P1 substitution returns the original word exactly.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord_eq_nil_iff {n : ℕ} (a : Fin n) (word : List (SurfaceCellComplex.SignedDart (Fin n))) : expandWord a word = [] ↔ word = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord_inverseWord {n : ℕ} (a : Fin n) (word : List (SurfaceCellComplex.SignedDart (Fin n))) : expandWord a (inverseWord word) = inverseWord (expandWord a word)

P1 commutes with reversal of an oriented cyclic boundary word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord_isRotated {n : ℕ} {a : Fin n} {left right : List (SurfaceCellComplex.SignedDart (Fin n))} (h : left ~r right) : expandWord a left ~r expandWord a right

A list-valued substitution preserves cyclic rotation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractWord_isRotated {n : ℕ} {left right : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))} (h : left ~r right) : contractWord left ~r contractWord right

Contraction preserves cyclic rotation even when the cut passes through a subdivided pair.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expandWord_isRotated_iff {n : ℕ} (a : Fin n) (left right : List (SurfaceCellComplex.SignedDart (Fin n))) : expandWord a left ~r expandWord a right ↔ left ~r right

P1 substitution preserves and reflects cyclic rotation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.castSucc_edge_mem_expandWord {n : ℕ} {a e : Fin n} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (h : e ∈ List.map edgeOfDart word) : e.castSucc ∈ List.map edgeOfDart (expandWord a word)

The occurrence of every retained edge survives the expansion.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.count_expandWord_castSucc {n : ℕ} (a e : Fin n) (word : List (SurfaceCellComplex.SignedDart (Fin n))) : List.count e (List.map edgeOfDart word) = List.count e.castSucc (List.map edgeOfDart (expandWord a word))

Each retained edge has exactly its old word multiplicity after P1.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.count_expandWord_freshEdge {n : ℕ} (a : Fin n) (word : List (SurfaceCellComplex.SignedDart (Fin n))) : List.count a (List.map edgeOfDart word) = List.count (freshEdge n) (List.map edgeOfDart (expandWord a word))

The fresh edge receives exactly the old multiplicity of the subdivided edge.

@[reducible, inline]

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

Canonical presentation-level P1 expansion.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expand_edgeCount (P : FiniteCyclicPresentation) (a : P.Edge) : (expand P a).edgeCount = P.edgeCount + 1

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expand_faces_length (P : FiniteCyclicPresentation) (a : P.Edge) : (expand P a).faces.length = P.faces.length

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceEquiv (P : FiniteCyclicPresentation) (a : P.Edge) : P.Face ≃ (expand P a).Face

P1 preserves face positions.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceEquiv P a = finCongr ⋯

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceEquiv_apply_val (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) : ↑((faceEquiv P a) f) = ↑f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expand_boundary (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) : (expand P a).boundary ((faceEquiv P a) f) = expandWord a (P.boundary f)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceEdgeMultiplicity_expand_castSucc (P : FiniteCyclicPresentation) (a e : P.Edge) (f : P.Face) : P.faceEdgeMultiplicity f e = (expand P a).faceEdgeMultiplicity ((faceEquiv P a) f) (Fin.castSucc e)

P1 copies every retained edge's facewise multiplicity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.faceEdgeMultiplicity_expand_freshEdge (P : FiniteCyclicPresentation) (a : P.Edge) (f : P.Face) : P.faceEdgeMultiplicity f a = (expand P a).faceEdgeMultiplicity ((faceEquiv P a) f) (freshEdge P.edgeCount)

P1 gives the fresh edge the subdivided edge's facewise multiplicity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.edgeMultiplicity_expand_castSucc (P : FiniteCyclicPresentation) (a e : P.Edge) : P.edgeMultiplicity e = (expand P a).edgeMultiplicity (Fin.castSucc e)

P1 copies every retained edge's total multiplicity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.edgeMultiplicity_expand_freshEdge (P : FiniteCyclicPresentation) (a : P.Edge) : P.edgeMultiplicity a = (expand P a).edgeMultiplicity (freshEdge P.edgeCount)

P1 gives the fresh edge the subdivided edge's total multiplicity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.map_faceAdjacent (P : FiniteCyclicPresentation) (a : P.Edge) {f g : P.Face} (h : P.FaceAdjacent f g) : (expand P a).FaceAdjacent ((faceEquiv P a) f) ((faceEquiv P a) g)

P1 sends source face adjacency to target face adjacency.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expand_isSurfaceValid (P : FiniteCyclicPresentation) (a : P.Edge) (h : P.IsSurfaceValid) : (expand P a).IsSurfaceValid

P1 preserves ordinary finite-presentation incidence validity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expand_isConnected (P : FiniteCyclicPresentation) (a : P.Edge) (h : P.IsConnected) : (expand P a).IsConnected

P1 preserves connectedness of the face-edge incidence graph.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expand_isGallierValid (P : FiniteCyclicPresentation) (a : P.Edge) (h : P.IsGallierValid) : (expand P a).IsGallierValid

P1 preserves the regular and exceptional branches of Gallier validity.

The exceptional branch is impossible here because selecting a already supplies an edge.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1Subdivision (P Q : FiniteCyclicPresentation) : Prop

A Gallier--Xu P1 subdivision, closed under signed relabeling and cyclic face rotation.

This is a syntactic move relation and deliberately does not bundle source validity. The preservation theorems below transport validity and connectivity when those hypotheses are available.

Equations

• P.P1Subdivision Q = ∃ (a : P.Edge), Nonempty ((LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.expand P a).SignedPresentationIso Q)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1Subdivision.canonical (P : FiniteCyclicPresentation) (a : P.Edge) : P.P1Subdivision (P1.expand P a)

The canonical expansion is a P1 subdivision.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1Subdivision.isSurfaceValid {P Q : FiniteCyclicPresentation} (hPQ : P.P1Subdivision Q) (h : P.IsSurfaceValid) : Q.IsSurfaceValid

P1 subdivisions preserve ordinary incidence validity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1Subdivision.isConnected {P Q : FiniteCyclicPresentation} (hPQ : P.P1Subdivision Q) (h : P.IsConnected) : Q.IsConnected

P1 subdivisions preserve face-incidence connectivity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1Subdivision.isGallierValid {P Q : FiniteCyclicPresentation} (hPQ : P.P1Subdivision Q) (h : P.IsGallierValid) : Q.IsGallierValid

P1 subdivisions preserve Gallier validity.