The skeleton homeomorphism across a 2-cell split #
Schoenflies/RealizeSplit.lean builds one realization of S.splitFace d from a realization
R of S and a drawing of the ear as a polygonal crosscut. A matched cellulation is two
realizations of one abstract structure together with the skeleton homeomorphism between them
(def:matched-pair clause 3), so the split has to be performed on both sides at once and the
skeleton homeomorphism has to be carried across. That is what this module does.
Blueprint #
def:matched-pair, clause 3 — the chosen homeomorphismg : |Γ| → |Γ'|, recorded asSchoenflies.CellStructure.SkeletonHomeo, extended across one split.def:generated-structure, operation 2 — the 2-cell split, whose two realizations are the output ofSchoenflies.CellStructure.SplitData.realize.
What is constructed #
Schoenflies.CellStructure.SplitData.skeletonSet_realize— the split's realized 1-skeleton is the old one together with the drawn ear, as a point set. Everything else rests on this.Schoenflies.CellStructure.SplitData.EarHomeo— the chosen homeomorphism between the two drawn ears (see the next section).Schoenflies.CellStructure.SplitData.EarHomeo.symm— the same chosen matching with source and target reversed, used by finite-transfer direction (b).Schoenflies.CellStructure.SplitData.splitMap/splitInvMap— the transported map and its inverse, as plain functionsPlane → Plane:gon the old skeleton, the ear map off it.Schoenflies.CellStructure.SplitData.splitHomeo— theSkeletonHomeobetween the two split realizations. Adefwith lemmas, not an∃-packaged bundle.Schoenflies.CellStructure.SplitData.splitHomeo_eqOn— the transported map agrees withgon the whole old skeleton. This is exactlySchoenflies.StageSequence.skelHomeo_succat a split step, and it is the reason the construction is "extendgby the ear map" rather than "rebuild a homeomorphism from scratch".
How the ear map is presented, and why #
Two shapes were available.
(a) As data: a map Plane → Plane (with an inverse) carrying the drawn source ear onto the
drawn target ear, vertex to corresponding vertex and edge arc to corresponding edge arc.
(b) Built edge by edge from the two EarCrosscuts, by composing one edge's parametrization
with the inverse of the other's.
This module takes (a), as EarHomeo. The reason is the consumer, not the construction:
def:matched-pair clause 3 says that g restricts to a fixed chosen homeomorphism on each
corresponding pair of cells, so a caller assembling a matched pair is holding such a chosen
homeomorphism already — for the old cells it is g itself, and for the ear's cells it is
whatever the producer of the two crosscuts chose. Shape (b) would manufacture a second,
different homeomorphism from the two parametrizations, and the caller would then have to prove
that its own choice agrees with the manufactured one. It would also silently fix an orientation
of every ear edge: Graph.IsDrawing.edge_param is orientation-free, so earDraw₁ f 0 and
earDraw₂ f 0 need not be the ends that correspond, and (b) would need the SubdivData.leftParam
trick of Schoenflies/RealizeSubdiv.lean replayed per edge.
Every field of EarHomeo is therefore something the caller supplies, and none of them mentions
R₁, R₂ or g: the ear map is a statement about the two drawn ears alone. In particular
no compatibility hypothesis between m and g is asked for, because none is needed: at the
ear's two ends m.toFun and g.toFun are forced to agree, both being pinned to
R₂.pos d.source and R₂.pos d.target — m by earPos_apply together with the two pos_source
/ pos_target clauses of the two EarCrosscuts, and g by its own pos_apply. That is
EarHomeo.toFun_pos_source / toFun_pos_target below.
The proof, in one paragraph #
The new skeleton is a union of two closed sets — the old realized skeleton
(Realization.isCompact_skeletonSet) and the drawn ear, which is an arc
(EarCrosscut.isArcBetween_earSet) and hence compact. Continuity of the transported map is the
pasting lemma Schoenflies.Plane.continuousOn_union_of_isClosed on those two pieces; the two
pieces meet exactly in the ear's two ends (EarCrosscut.earSet_inter_skeletonSet, which is
SplitData.vertexSet_inter made geometric), and there the two prescriptions agree. Injectivity
and the two inverse laws are injectivity on each piece plus the fact that the images also meet
only in the two images of the ends — for which the target-side
EarCrosscut.earSet_inter_skeletonSet is again what is spent. pos_apply and edgeArc_image
split into the old cells, where g's own fields serve verbatim, and the ear's cells, where
EarHomeo's two matching clauses are the statement.
What is not here #
The subdivision analogue — the transported skeleton homeomorphism across an edge
subdivision — is deliberately absent. It is being built concurrently on branch
wt/arc-monotone, where the missing ingredient (a homeomorphism between two arcs fixing their
ends is monotone, hence carries initial subarcs to initial subarcs — see the section
"What is not here" of Schoenflies/RealizeSubdiv.lean) is the actual content. Nothing below
depends on it, and nothing below should be duplicated there: this module is the split case only.
The general lemma this needed #
Graph.pointSet_congr — the point set of a plane graph depends on the drawing only through the
arcs of the graph's own edges. It is stated in the root Graph namespace next to
Graph.pointSet_union (which lives in Schoenflies/FaceCycles.lean); if a second consumer
appears it belongs there or in Schoenflies/Graph/Drawing.lean.
The point set of a plane graph only sees the arcs of its own edges. Two drawings that
agree, arc for arc, on E(G) give G the same point set. This is what makes the split's
splitDrawing — which is R.drawing on the old edges and earDraw on the ear's — restrict on
each half of the union to the drawing that half came with.
A realized 0-cell is a point of the realized 1-skeleton. The inlined form of this
appears at least four times on main (SkeletonHomeo.symm, Realization.disjoint_skeleton
arguments in Schoenflies/RealizeSplit.lean, …); it belongs next to
Realization.skeletonSet in Schoenflies/CombinatorialInvariance.lean.
The realized 1-skeleton of a split #
A 2-cell split adds the drawn ear to the drawn 1-skeleton and changes nothing else. This is the
geometric statement the whole module rests on: it turns every clause of SkeletonHomeo, which
quantifies over the new skeleton, into a pair of clauses over the two closed pieces.
The realized 1-skeleton after a 2-cell split is the old one together with the drawn ear.
EarCrosscut.splitGraph_eq says the new drawn graph is the union of the old one with the drawn
ear; Graph.pointSet_union splits the point set of that union; and Graph.pointSet_congr
replaces the split drawing by the drawing each half came with.
A 2-cell split only grows the realized 1-skeleton. This is the field
Schoenflies.StageSequence.skeletonSet_mono at a split step.
The drawn ear is closed: it is a simple arc, hence compact.
The chosen homeomorphism between the two drawn ears #
The chosen homeomorphism between two drawings of one abstract ear.
This is def:matched-pair clause 3 restricted to the cells the split creates: a homeomorphism
between the two drawn ears which matches corresponding vertices and corresponding edges. It is
data, not a proposition, and it mentions neither realization: everything it says is a statement
about the two drawings of d.ear.
earPos_apply and edgeArc_image are the two matching clauses. Together they force
toFun '' (source ear) = (target ear) (EarHomeo.image_earSet), which is why no separate
surjectivity clause is asked for. The inverse is supplied as data, exactly as in
CellStructure.SkeletonHomeo, so that no compactness argument is needed to speak of a
homeomorphism.
The map.
Its inverse.
- continuousOn_toFun : ContinuousOn self.toFun (d.earSet earPos₁ earDraw₁)
The map is continuous on the source ear.
- continuousOn_invFun : ContinuousOn self.invFun (d.earSet earPos₂ earDraw₂)
The inverse is continuous on the target ear.
- leftInvOn : Set.LeftInvOn self.invFun self.toFun (d.earSet earPos₁ earDraw₁)
The inverse undoes the map.
- rightInvOn : Set.RightInvOn self.invFun self.toFun (d.earSet earPos₂ earDraw₂)
The map undoes the inverse.
Corresponding vertices of the ear correspond.
- edgeArc_image ⦃f : γ⦄ : f ∈ d.ear.edgeSet → self.toFun '' Graph.edgeArc earDraw₁ f = Graph.edgeArc earDraw₂ f
Corresponding edges of the ear correspond.
Instances For
The chosen map carries the source ear onto the target ear. The point set of a drawn graph is its vertices together with its edge arcs, and the two matching clauses handle those two halves.
The inverse carries the target ear back into the source ear. Not a field: every point of the target ear is the image of a point of the source ear, and there the inverse is a left inverse.
Reverse a chosen matching of two realized ears. Direction (b) of finite transfer first
constructs the ear on the target side, so it naturally obtains the matching in the opposite
direction from the one consumed by GeneratedPair.split.
Equations
Instances For
At the ear's source end the chosen map is pinned to the old 0-cell's target position.
This — with SkeletonHomeo.pos_apply — is why no compatibility hypothesis between the ear map
and g has to be asked for.
The transported map #
The transported skeleton map: g on the old realized skeleton, the chosen ear map off
it. Written with a test on the old skeleton rather than on the ear so that agreement with g
— splitHomeo_eqOn, i.e. StageSequence.skelHomeo_succ — holds by definition.
Equations
- Schoenflies.CellStructure.SplitData.splitMap g m x = if x ∈ R₁.skeletonSet then g.toFun x else m.toFun x
Instances For
The transported inverse, by the same recipe on the target side.
Equations
- Schoenflies.CellStructure.SplitData.splitInvMap g m y = if y ∈ R₂.skeletonSet then g.invFun y else m.invFun y
Instances For
On the drawn ear the transported map is the chosen ear map — including at the two ends, where the two prescriptions agree because both are pinned to the target position of the old 0-cell.
On the drawn target ear the transported inverse is the chosen ear map's inverse.
A point of the source ear off the old skeleton is carried off the old target skeleton. The image lies on the target ear, and the target ear meets the target skeleton only in the two ends — whose preimages under the (injective) ear map are the two ends on the source side, which are on the source skeleton.
The mirror statement on the target side, for the inverse.
The skeleton homeomorphism across the split #
The skeleton homeomorphism, transported across a 2-cell split.
Given two realizations of one abstract cell structure, the skeleton homeomorphism g between
them, a drawing of the ear as a polygonal crosscut on each side, and the chosen homeomorphism
between the two drawn ears, this is the skeleton homeomorphism between the two split
realizations — def:matched-pair clause 3 for the structure S.splitFace d.
It is an extension of g, not a new map: splitHomeo_eqOn says it agrees with g on the
whole old realized skeleton, which is precisely the field StageSequence.skelHomeo_succ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The transported map agrees with g on the whole old realized skeleton.
This is the field Schoenflies.StageSequence.skelHomeo_succ at a 2-cell split step: consecutive
skeleton maps agree wherever both are defined. It holds by definition, which is the point of
building the map by extension rather than by rebuilding.
On the drawn ear the transported map is the chosen ear map — the other half of
def:matched-pair clause 3 for a split.