Subset splitting over disjoint unions

Edge subsets of a disjoint union split componentwise: the left/right parts, their join, the round trips, and the transport of pairing-closure, Eulerian-ness, and boundary-state matching — the first layer of the multiplicativity of the corrected constrained value over disjUnion.

The parts and the join

noncomputable def RS.leftPart {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (s : Finset (W₁.disjUnion W₂).Flag) : Finset W₁.Flag

The left part of a subset of the disjoint union.

Equations

• RS.leftPart s = s.toLeft

noncomputable def RS.rightPart {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (s : Finset (W₁.disjUnion W₂).Flag) : Finset W₂.Flag

The right part of a subset of the disjoint union.

Equations

• RS.rightPart s = s.toRight

noncomputable def RS.joinParts {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (s₁ : Finset W₁.Flag) (s₂ : Finset W₂.Flag) : Finset (W₁.disjUnion W₂).Flag

The join of componentwise subsets.

Equations

• RS.joinParts s₁ s₂ = s₁.disjSum s₂

@[simp]

theorem RS.mem_leftPart {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {s : Finset (W₁.disjUnion W₂).Flag} {f : W₁.Flag} : f ∈ leftPart s ↔ Sum.inl f ∈ s

Membership in the left part of a flag set.

@[simp]

theorem RS.mem_rightPart {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {s : Finset (W₁.disjUnion W₂).Flag} {f : W₂.Flag} : f ∈ rightPart s ↔ Sum.inr f ∈ s

Membership in the right part.

@[simp]

theorem RS.inl_mem_joinParts {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {s₁ : Finset W₁.Flag} {s₂ : Finset W₂.Flag} {f : W₁.Flag} : Sum.inl f ∈ joinParts s₁ s₂ ↔ f ∈ s₁

A left flag is in a join exactly when it is in the left summand.

@[simp]

theorem RS.inr_mem_joinParts {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {s₁ : Finset W₁.Flag} {s₂ : Finset W₂.Flag} {f : W₂.Flag} : Sum.inr f ∈ joinParts s₁ s₂ ↔ f ∈ s₂

The right analogue.

theorem RS.leftPart_joinParts {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (s₁ : Finset W₁.Flag) (s₂ : Finset W₂.Flag) : leftPart (joinParts s₁ s₂) = s₁

The left part of a join is what was joined on the left.

theorem RS.rightPart_joinParts {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (s₁ : Finset W₁.Flag) (s₂ : Finset W₂.Flag) : rightPart (joinParts s₁ s₂) = s₂

And likewise on the right.

theorem RS.joinParts_parts {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (s : Finset (W₁.disjUnion W₂).Flag) : joinParts (leftPart s) (rightPart s) = s

Joining a set's two parts recovers it: the split is a bijection.

Closure transport

theorem RS.pairing_closed_iff_parts {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (s : Finset (W₁.disjUnion W₂).Flag) : (∀ f ∈ s, (W₁.disjUnion W₂).pairing f ∈ s) ↔ (∀ f ∈ leftPart s, W₁.pairing f ∈ leftPart s) ∧ ∀ f ∈ rightPart s, W₂.pairing f ∈ rightPart s

Edge-closure is componentwise, no edge crossing between the components.

Attachment over the union

Filtering a disjoint sum

Degree transport

theorem RS.deg_disjUnion_inl {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (s : Finset (W₁.disjUnion W₂).Flag) (hc : ∀ f ∈ s, (W₁.disjUnion W₂).pairing f ∈ s) (h₁ : ∀ f ∈ leftPart s, W₁.pairing f ∈ leftPart s) (v : W₁.Vertex) : { flags := s, pairing_mem := hc }.deg (Sum.inl v) = { flags := leftPart s, pairing_mem := h₁ }.deg v

The degree at a left vertex is computed in the left part.

theorem RS.deg_disjUnion_inr {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (s : Finset (W₁.disjUnion W₂).Flag) (hc : ∀ f ∈ s, (W₁.disjUnion W₂).pairing f ∈ s) (h₂ : ∀ f ∈ rightPart s, W₂.pairing f ∈ rightPart s) (v : W₂.Vertex) : { flags := s, pairing_mem := hc }.deg (Sum.inr v) = { flags := rightPart s, pairing_mem := h₂ }.deg v

The degree at a right vertex is computed in the right part.

Eulerian transport

theorem RS.eulerian_iff_parts {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (s : Finset (W₁.disjUnion W₂).Flag) (hc : ∀ f ∈ s, (W₁.disjUnion W₂).pairing f ∈ s) (h₁ : ∀ f ∈ leftPart s, W₁.pairing f ∈ leftPart s) (h₂ : ∀ f ∈ rightPart s, W₂.pairing f ∈ rightPart s) : { flags := s, pairing_mem := hc }.Eulerian ↔ { flags := leftPart s, pairing_mem := h₁ }.Eulerian ∧ { flags := rightPart s, pairing_mem := h₂ }.Eulerian

Being Eulerian is componentwise.