Combinatorial invariance

The first module of Part II. It introduces the abstract record of a matched cellulation, the notion of a geometric realization of that record, and proves that everything a realization inherits from the record is the same for two realizations of one record — lem:combinatorial-invariance.

Per the blueprint's citation index this lemma has no internal prerequisites: the whole point of the design is that the combinatorial content of the cellulation machinery is separated from all of the geometry, so this can be built while the Jordan curve theorem is still unproved.

What is defined here, and how faithful it is

CellStructure is the abstract record of def:matched-cellulation: the finite cell sets in each dimension, the endpoint maps, the outer subcomplex, the boundary walks, and the subcell relation. Cells of all three dimensions are names drawn from one type γ; the 0- and 1-cells are the vertices and the edges of an abstract multigraph skel : Graph γ γ, the 2-cells are a set faces, and the three collections are disjoint. What is deliberately not in the record: the parent maps (they belong to a refinement — a pair of stages — not to a stage), and any compatibility between sub and the realizations (that is assertion (ix) of lem:cellulation-invariants, and the blueprint is explicit that ≼_abs "enters as a raw datum"). No reflexivity or transitivity of sub is assumed; the one lemma that needs transitivity takes it as a hypothesis.

CellStructure.Realization is one of the two geometric realizations. The repository's plane graphs have V(G) : Set Plane — vertices are points — so the drawn skeleton cannot literally be the abstract graph. It is instead the pushforward S.skel.map pos along the positions of the 0-cells, with pos injective on V(S.skel). This is the representation choice of the module, and the alternative — carrying an abstract graph isomorphism as data — was rejected because with the pushforward "the two skeleta realize the same abstract graph" is a definitional identity rather than a theorem, which is exactly what the blueprint's proof of part (a) asserts.

The price of the choice is paid here, once: Graph.isTwoConnected_map_iff and Graph.connected_map_iff transport connectivity along an injective relabelling of the vertices, so that 2-connectivity of the drawn graph — which is what def:admissible-graph requires — transfers between the realizations. Those two, and the walk and vertex-deletion lemmas they rest on, are general facts about Graph.map in the root Graph namespace and belong in Schoenflies/Graph/ if a second consumer appears.

SkeletonHomeo is g : |Γ| → |Γ'| of def:matched-pair, as a set-level homeomorphism with its inverse supplied as data (so that no finiteness hypothesis is needed to invert it). Clause 3 of def:matched-pair is recorded in the weaker form "g carries each drawn edge onto the corresponding drawn edge", which is all that is used and which the full clause implies.

The three parts of the lemma

Only part (b) has topological content. Parts (a) and (c) are, under this representation, either definitional identities or one-line consequences of the fact that the index sets involved are fields of the single structure both realizations realize; that is precisely the blueprint's argument ("all the data in (c) belong to the common abstract cell structure"), and the statements below are shaped so that a consumer gets the geometric conclusion on both sides from one combinatorial hypothesis.

Blueprint

• Schoenflies.CellStructure — the abstract record of def:matched-cellulation.
• Schoenflies.CellStructure.Realization — one of its two geometric realizations.
• Schoenflies.CellStructure.Realization.nonboundary — the open nonboundary part |Γ| \ C of def:admissible-graph.
• Schoenflies.CellStructure.Realization.star — the closed star St(σ) = ⋃_{σ ≼ τ} closure τ.
• Schoenflies.CellStructure.SkeletonHomeo — the skeleton homeomorphism of def:matched-pair.
• Schoenflies.CellStructure.combinatorial_invariance — lem:combinatorial-invariance, assembled from:
  • (a) Realization.graph_eq_map, Realization.edgeSet_graph_congr, Realization.isTwoConnected_congr, SkeletonHomeo.image_outerSet;
  • (b) SkeletonHomeo.image_nonboundary, SkeletonHomeo.isConnected_nonboundary_iff;
  • (c) Realization.star_mono, Realization.star_transfer, Realization.star_subset_of_sub, outerEdge_face_corresponds.
• Graph.isTwoConnected_map_iff, Graph.connected_map_iff — connectivity is invariant under an injective relabelling of the vertices; the transport that the pushforward representation of a realization needs.

theorem Graph.IsWalk.map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} {u v : α} {W : List β} (f : α → α') (h : G.IsWalk u W v) : (Graph.map f G).IsWalk (f u) W (f v)

theorem Graph.Reaches.map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} {u v : α} (f : α → α') (h : G.Reaches u v) : (Graph.map f G).Reaches (f u) (f v)

theorem Graph.Connected.map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} (f : α → α') (h : G.Connected) : (Graph.map f G).Connected

theorem Graph.HasThreeVertices.map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} {f : α → α'} (hf : Set.InjOn f G.vertexSet) (h : G.HasThreeVertices) : (Graph.map f G).HasThreeVertices

theorem Graph.map_deleteVerts_singleton {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} {f : α → α'} {x : α} (hf : Set.InjOn f G.vertexSet) (hx : x ∈ G.vertexSet) : (map f G).deleteVerts {f x} = map f (G.deleteVerts {x})

Deleting a vertex commutes with an injective relabelling of the vertices.

theorem Graph.IsTwoConnected.map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} {f : α → α'} (hf : Set.InjOn f G.vertexSet) (h : G.IsTwoConnected) : (Graph.map f G).IsTwoConnected

theorem Graph.map_map_invFunOn {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} {f : α → α'} [Nonempty α] (hf : Set.InjOn f G.vertexSet) : map (Function.invFunOn f G.vertexSet) (map f G) = G

An injective relabelling can be undone: Function.invFunOn inverts it on the vertex set.

theorem Graph.connected_map_iff {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} {f : α → α'} (hf : Set.InjOn f G.vertexSet) : (map f G).Connected ↔ G.Connected

theorem Graph.isTwoConnected_map_iff {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} {f : α → α'} (hf : Set.InjOn f G.vertexSet) : (map f G).IsTwoConnected ↔ G.IsTwoConnected

The point set of a subgraph

theorem Graph.pointSet_mono {δ : Type u_4} {H K : Graph Schoenflies.Plane δ} {drawing : δ → ℝ → Schoenflies.Plane} (h : H ≤ K) : H.pointSet drawing ⊆ K.pointSet drawing

structure Schoenflies.CellStructure (γ : Type u_2) : Type u_2

The abstract record of a matched cellulation (def:matched-cellulation), stripped to the data every consumer of combinatorial invariance reads.

The cells of all three dimensions are names drawn from one type γ: the 0-cells are the vertices of the skeleton, the 1-cells are its edges, and the 2-cells are faces. The three collections are required to be disjoint, so "the dimension of a cell" is well defined without being a field.

sub is the abstract subcell relation ≼_abs. The blueprint is explicit that it "enters as a raw datum" and imposes no compatibility with the realizations: that compatibility is assertion (ix) of lem:cellulation-invariants, proved elsewhere and for generated structures only. No reflexivity or transitivity is assumed here either; the two lemmas below that need transitivity take it as a hypothesis.

• skel : Graph γ γ

  The abstract 1-skeleton: its vertices are the 0-cells, its edges the 1-cells.

• faces : Set γ

  The 2-cells.

• outerGraph : Graph γ γ

  The distinguished outer cycle, as a subgraph of the skeleton.

• outerGraph_le : self.outerGraph ≤ self.skel

  The outer cycle is part of the skeleton.

• boundary : γ → List γ

  The cyclic boundary walk of each 2-cell, as a list of edge names. Raw datum: the blueprint lists it in the record of a matched cellulation and updates it explicitly under the two constructors.

• sub : γ → γ → Prop

  The abstract subcell relation ≼_abs.

• finite_vertexSet : self.skel.vertexSet.Finite

  Finitely many 0-cells.

• finite_edgeSet : self.skel.edgeSet.Finite

  Finitely many 1-cells.

• finite_faces : self.faces.Finite

  Finitely many 2-cells.

• disjoint_vertexSet_edgeSet : Disjoint self.skel.vertexSet self.skel.edgeSet

  A name is not both a 0-cell and a 1-cell.

• disjoint_faces_vertexSet : Disjoint self.faces self.skel.vertexSet

  A name is not both a 2-cell and a 0-cell.

• disjoint_faces_edgeSet : Disjoint self.faces self.skel.edgeSet

  A name is not both a 2-cell and a 1-cell.

def Schoenflies.CellStructure.cells {γ : Type u_1} (S : CellStructure γ) : Set γ

All cells of the structure.

Equations

• S.cells = S.skel.vertexSet ∪ S.skel.edgeSet ∪ S.faces

def Schoenflies.CellStructure.outerCells {γ : Type u_1} (S : CellStructure γ) : Set γ

The cells of the distinguished outer cycle: its vertices and its edges.

Equations

• S.outerCells = S.outerGraph.vertexSet ∪ S.outerGraph.edgeSet

def Schoenflies.CellStructure.supercells {γ : Type u_1} (S : CellStructure γ) (σ : γ) : Set γ

The supercells of a cell: the index set of its closed star.

Equations

• S.supercells σ = {τ : γ | S.sub σ τ}

def Schoenflies.CellStructure.MeetsOuter {γ : Type u_1} (S : CellStructure γ) (τ : γ) : Prop

A cell is incident with the outer cycle when some outer cell is a subcell of it. This is the middle, purely combinatorial condition of lem:outer-incidence.

Equations

• S.MeetsOuter τ = ∃ κ ∈ S.outerCells, S.sub κ τ

theorem Schoenflies.CellStructure.mem_supercells {γ : Type u_1} (S : CellStructure γ) {σ τ : γ} : τ ∈ S.supercells σ ↔ S.sub σ τ

theorem Schoenflies.CellStructure.supercells_subset_of_sub {γ : Type u_1} (S : CellStructure γ) (htrans : ∀ ⦃a b c : γ⦄, S.sub a b → S.sub b c → S.sub a c) {σ τ : γ} (h : S.sub σ τ) : S.supercells τ ⊆ S.supercells σ

Realizations

structure Schoenflies.CellStructure.Realization {γ : Type u_1} (S : CellStructure γ) : Type u_1

A geometric realization of the abstract structure: a position for each 0-cell, a parametrization for each 1-cell, and a point set for every open cell.

The drawn graph is S.skel.map pos — literally the pushforward of the one abstract skeleton. That is what makes "two realizations of the same abstract graph" a matter of definition rather than of a transported isomorphism.

Nothing is required of cell on a 2-cell. What it would have to satisfy — that the open 2-cell is the bounded complementary region of the Jordan curve of its boundary walk — is assertion (vii) of lem:cellulation-invariants, which is not available at this point in the development and which combinatorial invariance does not use.

• pos : γ → Plane

  Where each 0-cell sits.

• drawing : γ → ℝ → Plane

  How each 1-cell runs.

• injOn_pos : Set.InjOn self.pos S.skel.vertexSet

  Distinct 0-cells sit at distinct points.

• isDrawing : (Graph.map self.pos S.skel).IsDrawing self.drawing

  The positions and parametrizations draw the skeleton in the plane.

• cell : γ → Set Plane

  The point set of each open cell.

• cell_vertex ⦃v : γ⦄ : v ∈ S.skel.vertexSet → self.cell v = {self.pos v}

  A 0-cell is realized by its point.

• cell_edge ⦃e x y : γ⦄ : S.skel.IsLink e x y → self.cell e = Graph.edgeArc self.drawing e \ {self.pos x, self.pos y}

  A 1-cell is realized by its open arc: the drawn arc minus its two endpoints.

def Schoenflies.CellStructure.Realization.graph {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : Graph Plane γ

The drawn skeleton: the pushforward of the abstract skeleton along the positions.

Equations

• R.graph = Graph.map R.pos S.skel

@[simp]

theorem Schoenflies.CellStructure.Realization.vertexSet_graph {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : R.graph.vertexSet = R.pos '' S.skel.vertexSet

@[simp]

theorem Schoenflies.CellStructure.Realization.edgeSet_graph {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : R.graph.edgeSet = S.skel.edgeSet

instance Schoenflies.CellStructure.Realization.finite_graph {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : R.graph.Finite

def Schoenflies.CellStructure.Realization.skeletonSet {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : Set Plane

The realized 1-skeleton |Γ|.

Equations

• R.skeletonSet = R.graph.pointSet R.drawing

def Schoenflies.CellStructure.Realization.outerSet {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : Set Plane

The realized outer cycle: C in the source realization, S in the target one.

Equations

• R.outerSet = (Graph.map R.pos S.outerGraph).pointSet R.drawing

def Schoenflies.CellStructure.Realization.nonboundary {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : Set Plane

The open nonboundary part |Γ| \ C of def:admissible-graph.

Equations

• R.nonboundary = R.skeletonSet \ R.outerSet

def Schoenflies.CellStructure.Realization.star {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (σ : γ) : Set Plane

The closed star of a cell: the union of the closures of its supercells. The index set is abstract; only the summands are geometric.

Equations

• R.star σ = ⋃ τ ∈ S.supercells σ, closure (R.cell τ)

theorem Schoenflies.CellStructure.Realization.outerSet_subset_skeletonSet {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : R.outerSet ⊆ R.skeletonSet

theorem Schoenflies.CellStructure.Realization.isCompact_skeletonSet {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : IsCompact R.skeletonSet

theorem Schoenflies.CellStructure.Realization.cell_subset_skeletonSet {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {κ : γ} (hκ : κ ∈ S.skel.vertexSet ∪ S.skel.edgeSet) : R.cell κ ⊆ R.skeletonSet

An open 0-cell or 1-cell is part of the realized skeleton: a 0-cell is realized by a drawn vertex, a 1-cell by part of a drawn edge.

Hoisted here because Schoenflies/LimitMap.lean and Schoenflies/FiniteTransfer.lean each proved it independently and the duplicate gate caught the collision — two alpha-equivalent Props pass Lean's import checker under proof irrelevance, so a clean build would not have.

The skeleton homeomorphism

structure Schoenflies.CellStructure.SkeletonHomeo {γ : Type u_1} {S : CellStructure γ} (R₁ R₂ : S.Realization) : Type

The skeleton homeomorphism g : |Γ| → |Γ'| of def:matched-pair, between two realizations of one abstract cell structure.

Clause 3 of def:matched-pair — "on each corresponding pair of edges, g restricts to a fixed chosen homeomorphism between them, matching endpoints" — is recorded here in the weaker form edgeArc_image, which says only that g carries each drawn edge onto the corresponding drawn edge. That is all combinatorial invariance uses, and it is implied by the stronger clause.

Clause 2 of def:matched-pair, g = u on C, is not recorded: the boundary homeomorphism u is not part of a cell structure. A consumer that needs the identification carries it alongside; nothing here depends on it.

The inverse is supplied as data rather than produced from compactness, so that no finiteness hypothesis is needed to speak of a homeomorphism; a producer holding u⁻¹ has it anyway.

• toFun : Plane → Plane

  The map.

• invFun : Plane → Plane

  Its inverse.

• continuousOn_toFun : ContinuousOn self.toFun R₁.skeletonSet

  The map is continuous on the skeleton.

• continuousOn_invFun : ContinuousOn self.invFun R₂.skeletonSet

  The inverse is continuous on the other skeleton.

• leftInvOn : Set.LeftInvOn self.invFun self.toFun R₁.skeletonSet

  The inverse undoes the map.

• rightInvOn : Set.RightInvOn self.invFun self.toFun R₂.skeletonSet

  The map undoes the inverse.

• pos_apply ⦃v : γ⦄ : v ∈ S.skel.vertexSet → self.toFun (R₁.pos v) = R₂.pos v

  Corresponding 0-cells correspond.

• edgeArc_image ⦃e : γ⦄ : e ∈ S.skel.edgeSet → self.toFun '' Graph.edgeArc R₁.drawing e = Graph.edgeArc R₂.drawing e

  Corresponding 1-cells correspond.

theorem Schoenflies.CellStructure.SkeletonHomeo.image_pointSet_map {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (g : SkeletonHomeo R₁ R₂) {H : Graph γ γ} (hH : H ≤ S.skel) : g.toFun '' (Graph.map R₁.pos H).pointSet R₁.drawing = (Graph.map R₂.pos H).pointSet R₂.drawing

g carries the realization of any subcomplex of the skeleton onto the realization of the same subcomplex on the other side. Used for the whole skeleton and for the outer cycle.

theorem Schoenflies.CellStructure.SkeletonHomeo.image_skeletonSet {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (g : SkeletonHomeo R₁ R₂) : g.toFun '' R₁.skeletonSet = R₂.skeletonSet

theorem Schoenflies.CellStructure.SkeletonHomeo.image_outerSet {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (g : SkeletonHomeo R₁ R₂) : g.toFun '' R₁.outerSet = R₂.outerSet

The outer cycle corresponds — part (a) of lem:combinatorial-invariance, at the level of the two realizations.

theorem Schoenflies.CellStructure.SkeletonHomeo.injOn {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (g : SkeletonHomeo R₁ R₂) : Set.InjOn g.toFun R₁.skeletonSet

def Schoenflies.CellStructure.SkeletonHomeo.symm {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (g : SkeletonHomeo R₁ R₂) : SkeletonHomeo R₂ R₁

The homeomorphism run backwards.

Equations

• g.symm = { toFun := g.invFun, invFun := g.toFun, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, leftInvOn := ⋯, rightInvOn := ⋯, pos_apply := ⋯, edgeArc_image := ⋯ }

@[simp]

theorem Schoenflies.CellStructure.SkeletonHomeo.symm_toFun {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (g : SkeletonHomeo R₁ R₂) : g.symm.toFun = g.invFun

theorem Schoenflies.CellStructure.SkeletonHomeo.image_nonboundary {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (g : SkeletonHomeo R₁ R₂) : g.toFun '' R₁.nonboundary = R₂.nonboundary

The open nonboundary part corresponds — the geometric half of part (b) of lem:combinatorial-invariance. The skeleton homeomorphism carries the outer cycle onto the outer cycle, hence restricts to a bijection of the two open nonboundary parts.

theorem Schoenflies.CellStructure.SkeletonHomeo.isConnected_nonboundary_iff {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (g : SkeletonHomeo R₁ R₂) : IsConnected R₁.nonboundary ↔ IsConnected R₂.nonboundary

Connectedness of the open nonboundary part is invariant — part (b) of lem:combinatorial-invariance. This is the one clause with genuine topological content: it is what makes admissibility (def:admissible-graph) transfer between the two realizations.

theorem Schoenflies.CellStructure.SkeletonHomeo.isPreconnected_nonboundary_iff {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (g : SkeletonHomeo R₁ R₂) : IsPreconnected R₁.nonboundary ↔ IsPreconnected R₂.nonboundary

Combinatorial invariance

theorem Schoenflies.CellStructure.Realization.graph_eq_map {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : R.graph = Graph.map R.pos S.skel

The abstract skeleton is one graph — part (a) of lem:combinatorial-invariance. Both drawn skeleta are pushforwards of S.skel, so in particular they carry the same edge names.

theorem Schoenflies.CellStructure.Realization.edgeSet_graph_congr {γ : Type u_1} {S : CellStructure γ} (R₁ R₂ : S.Realization) : R₁.graph.edgeSet = R₂.graph.edgeSet

theorem Schoenflies.CellStructure.Realization.connected_congr {γ : Type u_1} {S : CellStructure γ} (R₁ R₂ : S.Realization) : R₁.graph.Connected ↔ R₂.graph.Connected

Connectedness of the skeleton is invariant — part (a).

theorem Schoenflies.CellStructure.Realization.isTwoConnected_congr {γ : Type u_1} {S : CellStructure γ} (R₁ R₂ : S.Realization) : R₁.graph.IsTwoConnected ↔ R₂.graph.IsTwoConnected

2-connectivity of the skeleton is invariant — part (a) of lem:combinatorial-invariance, and the clause the finite-transfer theorem cites when it concludes that a reproduced realization "has the same 2-connectivity" as the given one.

theorem Schoenflies.CellStructure.Realization.star_mono {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) {σ τ : γ} (h : S.supercells σ ⊆ S.supercells τ) : R.star σ ⊆ R.star τ

The closed star is a union over an index set that belongs to the abstract structure, so an inclusion of index sets gives an inclusion of stars in every realization. This is what part (c) of lem:combinatorial-invariance means by "all star-containment statements induced by refinement".

theorem Schoenflies.CellStructure.Realization.star_transfer {γ : Type u_1} {S : CellStructure γ} (R₁ R₂ : S.Realization) {σ τ : γ} (h : S.supercells σ ⊆ S.supercells τ) : R₁.star σ ⊆ R₁.star τ ∧ R₂.star σ ⊆ R₂.star τ

The same combinatorial hypothesis yields the geometric containment on both sides.

theorem Schoenflies.CellStructure.Realization.star_subset_of_sub {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (htrans : ∀ ⦃a b c : γ⦄, S.sub a b → S.sub b c → S.sub a c) {σ τ : γ} (h : S.sub σ τ) : R.star τ ⊆ R.star σ

A subcell has the larger star, once the abstract relation is known to be transitive.

def Schoenflies.CellStructure.OuterEdgeUniqueFace {γ : Type u_1} (S : CellStructure γ) : Prop

The clause "every outer edge is a subcell of exactly one 2-cell" — assertion (vi) of lem:cellulation-invariants — as a property of the abstract structure alone.

Equations

• S.OuterEdgeUniqueFace = ∀ ⦃e : γ⦄, e ∈ S.outerGraph.edgeSet → ∃! F : γ, F ∈ S.faces ∧ S.sub e F

theorem Schoenflies.CellStructure.outerEdge_face_corresponds {γ : Type u_1} {S : CellStructure γ} (h : S.OuterEdgeUniqueFace) {e : γ} (he : e ∈ S.outerGraph.edgeSet) : ∃ F ∈ S.faces, S.sub e F ∧ ∀ T ∈ S.faces, S.sub e T → T = F

The 2-cell incident with an outer edge is combinatorial — part (c) of lem:combinatorial-invariance. There is nothing to transport: the witness is a single abstract cell F, and the two realizations realize that one cell as R₁.cell F and R₂.cell F.

theorem Schoenflies.CellStructure.combinatorial_invariance {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (g : SkeletonHomeo R₁ R₂) : (R₁.graph.edgeSet = R₂.graph.edgeSet ∧ (R₁.graph.IsTwoConnected ↔ R₂.graph.IsTwoConnected) ∧ g.toFun '' R₁.outerSet = R₂.outerSet) ∧ (g.toFun '' R₁.nonboundary = R₂.nonboundary ∧ (IsConnected R₁.nonboundary ↔ IsConnected R₂.nonboundary)) ∧ ∀ (σ τ : γ), S.supercells σ ⊆ S.supercells τ → R₁.star σ ⊆ R₁.star τ ∧ R₂.star σ ⊆ R₂.star τ

Combinatorial invariance (lem:combinatorial-invariance), assembled.

Given two realizations of one generated matched cell structure and the skeleton homeomorphism between them:

• (a) the two drawn skeleta are pushforwards of the same abstract graph S.skel, they carry the same edge names, 2-connectivity holds for one iff it holds for the other, and the realized outer cycles correspond under g;
• (b) the realized open nonboundary parts correspond under g, so one is connected iff the other is;
• (c) an inclusion of supercell sets — a statement of the common abstract structure — gives the corresponding star containment in both realizations.

The subcell relation, the parent maps and the collection of supercells of a cell do not appear in the conclusion because under this representation they are not two objects to be compared: they are fields of the single S that both realizations are realizations of.