Exploding a closed fragment into stars

The accompanying paper's "stars and closed graphs" (§3.2): a closed fragment is its own star union, reglued along the edge matching. The explosion is parameterized by a pairing-closed set C of cut flags: each cut flag's edge is severed, the freed half-edge becoming a pendant boundary edge of its vertex's star. At C = ∅ the explosion is the fragment itself; at C = univ it is the disjoint union of vertex stars. Regluing shrinks C one edge at a time (explodeAtGluePair, next file), giving the star decomposition by induction.

def RS.ClosedFragment.vertexOf (W : ClosedFragment) (f : W.Flag) : W.Vertex

The vertex of a flag in a closed fragment.

Equations

• W.vertexOf f = Sum.elim id Fin.elim0 (W.attach f)

theorem RS.ClosedFragment.attach_eq_vertexOf (W : ClosedFragment) (f : W.Flag) : W.attach f = Sum.inl (W.vertexOf f)

Every flag of a closed fragment attaches to its vertex.

def RS.CutClosed (W : ClosedFragment) (C : Finset W.Flag) : Prop

A pairing-closed cut set: with each flag, its partner.

Equations

• RS.CutClosed W C = ∀ f ∈ C, W.pairing f ∈ C

theorem RS.CutClosed.pairing_mem {W : ClosedFragment} {C : Finset W.Flag} (hC : CutClosed W C) {f : W.Flag} : W.pairing f ∈ C ↔ f ∈ C

Membership of the partner, from cut closure.

def RS.explodeAt (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) : Fragment ↥C

The explosion at a cut set: sever each cut flag's edge, the freed half-edge becoming a pendant boundary edge labelled by the cut flag itself.

Equations

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

One regluing step

def RS.cutErase (W : ClosedFragment) (C : Finset W.Flag) (f₀ : W.Flag) : Finset W.Flag

The shrunken cut set: the edge of f₀ restored.

Equations

• RS.cutErase W C f₀ = (C.erase f₀).erase (W.pairing f₀)

theorem RS.mem_cutErase (W : ClosedFragment) (C : Finset W.Flag) (f₀ : W.Flag) {g : W.Flag} : g ∈ cutErase W C f₀ ↔ g ∈ C ∧ g ≠ f₀ ∧ g ≠ W.pairing f₀

Erasing one edge from the cut set removes exactly its two flags.

theorem RS.cutErase_closed (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (f₀ : W.Flag) : CutClosed W (cutErase W C f₀)

The erased set is still pairing-closed, so the explosion recurses.

def RS.stepLabelI (W : ClosedFragment) (C : Finset W.Flag) (f₀ : W.Flag) (h₀ : f₀ ∈ C) : ↥C

The glued labels of the step, as labels of the explosion.

Equations

• RS.stepLabelI W C f₀ h₀ = ⟨f₀, h₀⟩

def RS.stepLabelJ (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (f₀ : W.Flag) (h₀ : f₀ ∈ C) : ↥C

The partner label of the step.

Equations

• RS.stepLabelJ W C hC f₀ h₀ = ⟨W.pairing f₀, ⋯⟩

theorem RS.stepLabel_ne (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (f₀ : W.Flag) (h₀ : f₀ ∈ C) : stepLabelI W C f₀ h₀ ≠ stepLabelJ W C hC f₀ h₀

The two labels the severed edge creates are distinct.

def RS.stepLabelEquiv (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (f₀ : W.Flag) (h₀ : f₀ ∈ C) : ↥(cutErase W C f₀) ≃ Fragment.SurvivingLabel (↥C) (stepLabelI W C f₀ h₀) (stepLabelJ W C hC f₀ h₀)

The surviving labels of the step are the shrunken cut set.

Equations

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

def RS.stepFlagEquiv (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (f₀ : W.Flag) (h₀ : f₀ ∈ C) : (explodeAt W C hC).SurvivingFlag (stepLabelI W C f₀ h₀) (stepLabelJ W C hC f₀ h₀) ≃ W.Flag ⊕ ↥(cutErase W C f₀)

The surviving flags of the step are the flags of the smaller explosion.

Equations

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

noncomputable def RS.explodeAtGluePair (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (f₀ : W.Flag) (h₀ : f₀ ∈ C) : ((explodeAt W C hC).gluePair (stepLabelI W C f₀ h₀) (stepLabelJ W C hC f₀ h₀) ⋯).Equiv ((explodeAt W (cutErase W C f₀) ⋯).relabel (stepLabelEquiv W C hC f₀ h₀))

One regluing step: gluing the two cut ends of the edge of f₀ in the explosion at C is the explosion at the shrunken cut set.

Equations

• RS.explodeAtGluePair W C hC f₀ h₀ = ⋯.mpr { flagEquiv := RS.stepFlagEquiv W C hC f₀ h₀, vertexEquiv := Equiv.refl W.Vertex, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }