Transporting a skeleton homeomorphism across an edge subdivision

Schoenflies/RealizeSubdiv.lean builds SubdivData.realize, the realization of a subdivided cell structure, and closes with the observation that it does not move the realized 1-skeleton (SubdivData.skeletonSet_realize). It also names what was missing: a CellStructure.SkeletonHomeo between two realizations does not, by itself, carry the half arcs of a subdivided edge onto each other. That gap is what Schoenflies/ArcMonotone.lean fills, and this module spends.

SubdivData.realizeHomeo is the transported homeomorphism. As a point map it is unchanged — realizeHomeo_toFun is rfl — which is exactly what CellStructure.LimitTower.skelHomeo_succ in Schoenflies/LimitMap.lean asks for ("an edge subdivision leaves the skeleton map unchanged as a point map"), and through it Schoenflies.StageSequence.

The target parameter, and the two orientations

Subdividing at parameter t on the source side means subdividing at the parameter on the target side where R₂.drawing d.edge sits at g.toFun (R₁.drawing d.edge t). That is SubdivData.targetParam, a plain def built from Schoenflies.transferParam; a caller never has to guess it, and SubdivData.drawing_targetParam is its defining property.

RealizeSubdiv.lean warns that IsDrawing.edge_param is orientation-free, so drawing e 0 may be either end of e, and reads the orientation off with SubdivData.leftParam. The same issue arises here on the R₂ side, and it is not forced: the two realizations are independent data, so nothing prevents R₁ from drawing d.edge from d.left and R₂ from drawing it from d.right. This module does not assume otherwise. It does not need a second case distinction either, because the transfer map handles it:

SubdivData.targetParam_leftParam : targetParam (leftParam R₁) = leftParam R₂

holds whatever the two orientations are — g carries R₁.pos d.left to R₂.pos d.left, and leftParam R₂ is by definition the parameter sitting there. Correspondingly the arc identity imported from ArcMonotone is stated over uIcc, which is unordered, so the two halves match up without either orientation ever being named. The one place the orientations do surface is SubdivData.targetParam_ends, which records that the pair (targetParam 0, targetParam 1) is (0, 1) or (1, 0) — the input ArcMonotone.param_mem_Ioo_of_ends needs to know the new target parameter is interior.

Blueprint

• def:matched-pair, clause 3 — the transported edgeArc_image at the two new 1-cells is precisely "on each corresponding pair of edges, g restricts to a chosen homeomorphism between them, matching endpoints", propagated through operation 1.
• def:generated-structure, operation 1 (edge subdivision) — "the corresponding point is inserted into the corresponding edge"; SubdivData.targetParam is "corresponding".

Declarations:

• Schoenflies.CellStructure.SubdivData.arcMatch_edge — the drawn subdivided edge, its image, and g between them, as an ArcMatch.
• Schoenflies.CellStructure.SubdivData.targetParam — the corresponding parameter on the target side, with drawing_targetParam, targetParam_leftParam, targetParam_rightParam, targetParam_ends, targetParam_mem_Ioo.
• Schoenflies.CellStructure.SubdivData.realizeHomeo — the transported skeleton homeomorphism, with realizeHomeo_toFun / realizeHomeo_invFun / realizeHomeo_eqOn.

The drawn subdivided edge, on both sides

theorem Schoenflies.CellStructure.SubdivData.edgeArc_subset_skeletonSet {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : R.drawing d.edge '' unitInterval ⊆ R.skeletonSet

theorem Schoenflies.CellStructure.SubdivData.arcMatch_edge {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (d : S.SubdivData) (g : SkeletonHomeo R₁ R₂) : ArcMatch (R₁.drawing d.edge) (R₂.drawing d.edge) g.toFun

The subdivided edge is drawn on both sides, and g carries one drawing onto the other. Everything the arc-monotonicity machinery needs, assembled from fields of R₁, R₂ and g; no new hypothesis.

The corresponding parameter on the target side

noncomputable def Schoenflies.CellStructure.SubdivData.targetParam {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (d : S.SubdivData) (g : SkeletonHomeo R₁ R₂) (t : ℝ) : ℝ

The parameter at which the target drawing sits at the image of the source point.

A def, not an existential: the subdivided target realization is d.realize R₂ (d.targetParam g t) _, and every lemma below refers to it by name.

Equations

• d.targetParam g t = Schoenflies.transferParam (R₁.drawing d.edge) (R₂.drawing d.edge) g.toFun t

theorem Schoenflies.CellStructure.SubdivData.targetParam_mem_I {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (d : S.SubdivData) (g : SkeletonHomeo R₁ R₂) {t : ℝ} (ht : t ∈ unitInterval) : d.targetParam g t ∈ unitInterval

theorem Schoenflies.CellStructure.SubdivData.drawing_targetParam {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (d : S.SubdivData) (g : SkeletonHomeo R₁ R₂) {t : ℝ} (ht : t ∈ unitInterval) : R₂.drawing d.edge (d.targetParam g t) = g.toFun (R₁.drawing d.edge t)

The defining property of the target parameter.

theorem Schoenflies.CellStructure.SubdivData.targetParam_leftParam {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (d : S.SubdivData) (g : SkeletonHomeo R₁ R₂) : d.targetParam g (d.leftParam R₁) = d.leftParam R₂

The endpoint of the subdivided edge at d.left corresponds to the endpoint at d.left, whichever way round either realization happens to draw the edge.

theorem Schoenflies.CellStructure.SubdivData.targetParam_rightParam {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (d : S.SubdivData) (g : SkeletonHomeo R₁ R₂) : d.targetParam g (d.rightParam R₁) = d.rightParam R₂

…and likewise at d.right.

theorem Schoenflies.CellStructure.SubdivData.targetParam_ends {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (d : S.SubdivData) (g : SkeletonHomeo R₁ R₂) : d.targetParam g 0 = 0 ∧ d.targetParam g 1 = 1 ∨ d.targetParam g 0 = 1 ∧ d.targetParam g 1 = 0

The two endpoint parameters go to the two endpoint parameters, in one order or the other. This is the only statement in the file that mentions the orientations at all, and it is here only because interiority of the new target parameter needs it.

theorem Schoenflies.CellStructure.SubdivData.targetParam_mem_Ioo {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (d : S.SubdivData) (g : SkeletonHomeo R₁ R₂) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : d.targetParam g t ∈ Set.Ioo 0 1

An interior source parameter has an interior target parameter — so the target realization can be subdivided at it.

theorem Schoenflies.CellStructure.SubdivData.image_edge_uIcc {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (d : S.SubdivData) (g : SkeletonHomeo R₁ R₂) {s u : ℝ} (hs : s ∈ unitInterval) (hu : u ∈ unitInterval) : g.toFun '' R₁.drawing d.edge '' Set.uIcc s u = R₂.drawing d.edge '' Set.uIcc (d.targetParam g s) (d.targetParam g u)

g carries a piece of the drawn edge onto the corresponding piece. The whole content of Schoenflies/ArcMonotone.lean, specialized to the subdivided edge.

The transported skeleton homeomorphism

noncomputable def Schoenflies.CellStructure.SubdivData.realizeHomeo {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (d : S.SubdivData) (g : SkeletonHomeo R₁ R₂) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : SkeletonHomeo (d.realize R₁ t ht) (d.realize R₂ (d.targetParam g t) ⋯)

The skeleton homeomorphism, transported across an edge subdivision.

The point map is untouched: a subdivision does not move the realized 1-skeleton (skeletonSet_realize), so six of the eight fields are the old ones read through that equality. The two that are not — pos_apply at the new 0-cell and edgeArc_image at the two new 1-cells — are drawing_targetParam and image_edge_uIcc.

Equations

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

@[simp]

theorem Schoenflies.CellStructure.SubdivData.realizeHomeo_toFun {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (d : S.SubdivData) (g : SkeletonHomeo R₁ R₂) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : (d.realizeHomeo g ht).toFun = g.toFun

@[simp]

theorem Schoenflies.CellStructure.SubdivData.realizeHomeo_invFun {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (d : S.SubdivData) (g : SkeletonHomeo R₁ R₂) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : (d.realizeHomeo g ht).invFun = g.invFun

theorem Schoenflies.CellStructure.SubdivData.realizeHomeo_eqOn {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (d : S.SubdivData) (g : SkeletonHomeo R₁ R₂) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) {A : Set Plane} : Set.EqOn (d.realizeHomeo g ht).toFun g.toFun A

The transported map is the old one as a point map — the form CellStructure.LimitTower.skelHomeo_succ consumes.