Subset correspondence for single-pair gluing

The subset-level maps underlying the single-pair gluing decomposition: lift and drop maps between flag subsets of a glued fragment W' = W.gluePair i j hij and flag subsets of the original fragment W. Separate definitions and lemma sets for the open case (the two glued boundary flags bound distinct edges, unified by rewiring) and the closed case (they bound a common edge, which closes into a free circle parameterized by a Bool).

Drop map (common to both cases)

noncomputable def RS.Fragment.dropSubset {α : Type} (W : Fragment α) (i j : α) (s : Finset W.Flag) : Finset (W.SurvivingFlag i j)

Drop a flag set from W to the surviving flags of a glue at {i, j}: keep only those flags distinct from both boundary flags.

Equations

• W.dropSubset i j s = Finset.subtype (fun (f : W.Flag) => f ≠ W.boundaryFlag i ∧ f ≠ W.boundaryFlag j) s

theorem RS.Fragment.mem_dropSubset {α : Type} {W : Fragment α} {i j : α} {s : Finset W.Flag} {f : W.SurvivingFlag i j} : f ∈ W.dropSubset i j s ↔ ↑f ∈ s

Membership in a dropped set is membership of the underlying flag.

Partner surviving flags (open case)

def RS.Fragment.partnerSurvI {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) : W.SurvivingFlag i j

In the open case, the W-partner of boundary flag i is a surviving flag (it is neither boundaryFlag i nor boundaryFlag j).

Equations

• RS.Fragment.partnerSurvI hopen = ⟨W.pairing (W.boundaryFlag i), ⋯⟩

def RS.Fragment.partnerSurvJ {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) : W.SurvivingFlag i j

In the open case, the W-partner of boundary flag j is a surviving flag.

Equations

• RS.Fragment.partnerSurvJ hopen = ⟨W.pairing (W.boundaryFlag j), ⋯⟩

@[simp]

theorem RS.Fragment.partnerSurvI_val {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) : ↑(partnerSurvI hopen) = W.pairing (W.boundaryFlag i)

The underlying flag of the first partner.

@[simp]

theorem RS.Fragment.partnerSurvJ_val {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) : ↑(partnerSurvJ hopen) = W.pairing (W.boundaryFlag j)

The underlying flag of the second partner.

noncomputable def RS.Fragment.liftSubsetOpen {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) : Finset W.Flag

Lift a surviving-flag set to W in the open case: the image under Subtype.val, together with boundary flag i iff its W-partner participates, and boundary flag j iff its W-partner participates.

Equations

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

Membership in the open-case lift

theorem RS.Fragment.boundaryFlagI_not_mem_image {α : Type} {W : Fragment α} {i j : α} (s' : Finset (W.SurvivingFlag i j)) : W.boundaryFlag i ∉ Finset.image Subtype.val s'

The first glued boundary flag is not the image of any surviving flag.

theorem RS.Fragment.boundaryFlagJ_not_mem_image {α : Type} {W : Fragment α} {i j : α} (s' : Finset (W.SurvivingFlag i j)) : W.boundaryFlag j ∉ Finset.image Subtype.val s'

Nor is the second.

theorem RS.Fragment.surviving_val_mem_liftOpen_iff {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (f : W.SurvivingFlag i j) : ↑f ∈ liftSubsetOpen hopen s' ↔ f ∈ s'

On surviving flags an open lift is membership in the set it lifts.

theorem RS.Fragment.boundaryFlagI_mem_liftOpen_iff {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) : W.boundaryFlag i ∈ liftSubsetOpen hopen s' ↔ partnerSurvI hopen ∈ s'

The open lift carries the first glued boundary flag exactly when the set carries its partner: rewiring joins the two edges into one, so their flags stand or fall together.

theorem RS.Fragment.boundaryFlagJ_mem_liftOpen_iff {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) : W.boundaryFlag j ∈ liftSubsetOpen hopen s' ↔ partnerSurvJ hopen ∈ s'

The same at the second glued boundary flag.

Round trips (open case)

theorem RS.Fragment.dropSubset_liftSubsetOpen {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) : W.dropSubset i j (liftSubsetOpen hopen s') = s'

Dropping an open lift is the identity.

theorem RS.Fragment.liftSubsetOpen_dropSubset {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s : Finset W.Flag) (hcl : ∀ f ∈ s, W.pairing f ∈ s) : liftSubsetOpen hopen (W.dropSubset i j s) = s

Lifting the drop of an edge-closed set is the identity: nothing is lost across an open glue.

Forward closure transport (open case)

theorem RS.Fragment.liftSubsetOpen_pairing_closed {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (hcl : ∀ f ∈ s', rewire hopen f ∈ s') (f : W.Flag) : f ∈ liftSubsetOpen hopen s' → W.pairing f ∈ liftSubsetOpen hopen s'

The open lift of a rewire-closed set is edge-closed.

Closed case

noncomputable def RS.Fragment.liftSubsetClosed {α : Type} {W : Fragment α} {i j : α} (s' : Finset (W.SurvivingFlag i j)) (b : Bool) : Finset W.Flag

Lift a surviving-flag set to W in the closed case: the image under Subtype.val, together with both boundary flags i and j iff the Bool b is true (the closed-off circle-edge participates).

Equations

• RS.Fragment.liftSubsetClosed s' b = Finset.image Subtype.val s' ∪ if b = true then {W.boundaryFlag i, W.boundaryFlag j} else ∅

Membership in the closed-case lift

theorem RS.Fragment.surviving_val_mem_liftClosed_iff {α : Type} {W : Fragment α} {i j : α} (s' : Finset (W.SurvivingFlag i j)) (b : Bool) (f : W.SurvivingFlag i j) : ↑f ∈ liftSubsetClosed s' b ↔ f ∈ s'

On surviving flags a closed lift is membership in the set it lifts, whatever the circle bit.

theorem RS.Fragment.boundaryFlagI_mem_liftClosed_iff {α : Type} {W : Fragment α} {i j : α} (_hij : i ≠ j) (s' : Finset (W.SurvivingFlag i j)) (b : Bool) : W.boundaryFlag i ∈ liftSubsetClosed s' b ↔ b = true

The closed lift carries the first glued boundary flag exactly when the circle bit is set: the closed cut's own edge is either taken whole or not at all.

theorem RS.Fragment.boundaryFlagJ_mem_liftClosed_iff {α : Type} {W : Fragment α} {i j : α} (_hij : i ≠ j) (s' : Finset (W.SurvivingFlag i j)) (b : Bool) : W.boundaryFlag j ∈ liftSubsetClosed s' b ↔ b = true

The same at the second glued boundary flag, on the same bit.

Round trips (closed case)

theorem RS.Fragment.dropSubset_liftSubsetClosed {α : Type} {W : Fragment α} {i j : α} (s' : Finset (W.SurvivingFlag i j)) (b : Bool) : W.dropSubset i j (liftSubsetClosed s' b) = s'

Dropping a closed lift is the identity.

theorem RS.Fragment.liftSubsetClosed_dropSubset {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (s : Finset W.Flag) (hcl : ∀ f ∈ s, W.pairing f ∈ s) : liftSubsetClosed (W.dropSubset i j s) (decide (W.boundaryFlag i ∈ s)) = s

Lifting the drop of an edge-closed set, at the bit recording whether the set took the closed edge, is the identity.

Closure transport (closed case)

noncomputable def RS.Fragment.closedPairingSubtype {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (f : W.SurvivingFlag i j) : W.SurvivingFlag i j

The pairing of the closed glued fragment, as an explicit surviving-flag function.

Equations

• RS.Fragment.closedPairingSubtype hclosed f = ⟨W.pairing ↑f, ⋯⟩

@[simp]

theorem RS.Fragment.liftSubsetClosed_pairing_closed {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (b : Bool) (hcl : ∀ f ∈ s', closedPairingSubtype hclosed f ∈ s') (g : W.Flag) : g ∈ liftSubsetClosed s' b → W.pairing g ∈ liftSubsetClosed s' b

The closed lift of a pairing-closed set is edge-closed.

theorem RS.Fragment.dropSubset_pairing_closed_of_closed {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (s : Finset W.Flag) (hcl : ∀ f ∈ s, W.pairing f ∈ s) (f : W.SurvivingFlag i j) : f ∈ W.dropSubset i j s → closedPairingSubtype hclosed f ∈ W.dropSubset i j s

The drop of an edge-closed set is closed under the glued fragment's pairing.

Eulerian transport

theorem RS.Fragment.vertex_flag_surviving {α : Type} {W : Fragment α} {i j : α} (f : W.Flag) (v : W.Vertex) (hv : W.attach f = Sum.inl v) : f ≠ W.boundaryFlag i ∧ f ≠ W.boundaryFlag j

Vertex-attached flags are surviving flags: a flag attached to an internal vertex cannot be a boundary flag.

theorem RS.Fragment.deg_liftSubsetOpen_eq {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (v : W.Vertex) : {f ∈ liftSubsetOpen hopen s' | W.attach f = Sum.inl v}.card = {f ∈ s' | W.glueAttach i j f = Sum.inl v}.card

Vertex degrees are preserved by the open-case lift.

theorem RS.Fragment.deg_liftSubsetClosed_eq {α : Type} {W : Fragment α} {i j : α} (s' : Finset (W.SurvivingFlag i j)) (b : Bool) (v : W.Vertex) : {f ∈ liftSubsetClosed s' b | W.attach f = Sum.inl v}.card = {f ∈ s' | W.glueAttach i j f = Sum.inl v}.card

Vertex degrees are preserved by the closed-case lift.

State compatibility