Vertex-local in-sets and the incoming-flag sign

The vocabulary the orientation-change analysis is written in: at a vertex, the participating flags attached to it and marked incoming form a finite set, of which EdgeSubset.relInFlagsAt is the sorted enumeration; each such flag carries an odd-pairing sign, and the odd-colour pair it contributes is read off by two maps.

Flipping the colours on a set S negates the sign at the flags of S and leaves the others alone, which is what makes the flip analysis a product of independent local factors.

The in-set at a vertex

noncomputable def RS.relInSetAt {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₀ : F.RelTransitionSystem} (o₀ : κ₀.Orientation) (vv : W.Vertex) : Finset W.Flag

The in-set at a vertex over a relative orientation: the participating flags attached to the vertex and marked incoming.

Equations

• RS.relInSetAt o₀ vv = {f ∈ F.flags | W.attach f = Sum.inl vv ∧ o₀.isOut f = false}

theorem RS.mem_relInSetAt {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₀ : F.RelTransitionSystem} {o₀ : κ₀.Orientation} {vv : W.Vertex} {g : W.Flag} : g ∈ relInSetAt o₀ vv ↔ g ∈ F.flags ∧ W.attach g = Sum.inl vv ∧ o₀.isOut g = false

Membership in the in-set at a vertex, unfolded.

theorem RS.relInSetAt_subset_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₀ : F.RelTransitionSystem} {o₀ : κ₀.Orientation} {vv : W.Vertex} {g : W.Flag} (hg : g ∈ relInSetAt o₀ vv) : g ∈ F.internalFlags

An in-flag at a vertex is an internal flag.

theorem RS.relInFlagsAt_coe {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₀ : F.RelTransitionSystem} (o₀ : κ₀.Orientation) (vv : W.Vertex) : ↑(F.relInFlagsAt o₀ vv) = (relInSetAt o₀ vv).val

EdgeSubset.relInFlagsAt enumerates the in-set at a vertex.

The odd-colour pair at an internal flag

noncomputable def RS.pairA {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} (φ : F.CoreOddColouring ℓ) (f : ↥F.internalFlags) : Fin (2 * ℓ)

The flag's own odd colour.

Equations

• RS.pairA φ f = ↑φ ⟨↑f, ⋯⟩

noncomputable def RS.pairB {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} {κ₀ : F.RelTransitionSystem} (φ : F.CoreOddColouring ℓ) (f : ↥F.internalFlags) : Fin (2 * ℓ)

The odd colour opposite the flag's transition partner.

Equations

• RS.pairB φ f = RS.oddPartner ℓ (↑φ ⟨κ₀.match_ ↑f, ⋯⟩)

theorem RS.evalOdd_flatMap_rev {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (μ : Multiset (Fin k)) {β : Type u_1} (pa pb : β → Fin (2 * ℓ)) (l : List β) (pre : List (Fin (2 * ℓ))) : hM.evalOdd μ (pre ++ List.flatMap (fun (f : β) => [pb f, pa f]) l) = (-1) ^ l.length * hM.evalOdd μ (pre ++ List.flatMap (fun (f : β) => [pa f, pb f]) l)

Reversing every odd pair of a list multiplies the odd evaluation by (−1) per pair.

The incoming-flag sign

noncomputable def RS.inSign {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} (φ : F.CoreOddColouring ℓ) (g : W.Flag) : ℤ

The odd-pairing sign an incoming flag carries, extended by one off the core.

Equations

• RS.inSign φ g = if hg : g ∈ F.coreFlags then RS.oddPartnerSign ℓ (↑φ ⟨g, hg⟩) else 1

theorem RS.inSign_flip_of_mem {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} {S : Finset W.Flag} {φ φ' : F.CoreOddColouring ℓ} (hφ' : ∀ (g : ↥F.coreFlags), ↑φ' g = if ↑g ∈ S then oddPartner ℓ (↑φ g) else ↑φ g) {g : W.Flag} (hg : g ∈ S) (hcore : g ∈ F.coreFlags) : inSign φ' g = -inSign φ g

Flipping the colours on S negates the sign at a flag of S.

theorem RS.inSign_flip_of_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} {S : Finset W.Flag} {φ φ' : F.CoreOddColouring ℓ} (hφ' : ∀ (g : ↥F.coreFlags), ↑φ' g = if ↑g ∈ S then oddPartner ℓ (↑φ g) else ↑φ g) {g : W.Flag} (hg : g ∉ S) : inSign φ' g = inSign φ g

Flipping the colours on S leaves the sign off S alone.

theorem RS.inSign_mul_self {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} (φ : F.CoreOddColouring ℓ) (g : W.Flag) : inSign φ g * inSign φ g = 1

The sign is a square root of one.

theorem RS.inSign_pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} (φ : F.CoreOddColouring ℓ) {g : W.Flag} (hg : g ∈ F.coreFlags) : inSign φ (W.pairing g) = inSign φ g

Paired flags carry the same sign.

The core odd data in this vocabulary

theorem RS.coreOddPairFn_eq' {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} {κ₀ : F.RelTransitionSystem} (φ : F.CoreOddColouring ℓ) : F.coreOddPairFn κ₀ φ = fun (f : ↥F.internalFlags) => [pairA φ f, pairB φ f]

The odd pair an internal flag contributes, in terms of the two pair maps.

theorem RS.signFn_eq {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} {κ₀ : F.RelTransitionSystem} (φ : F.CoreOddColouring ℓ) (f : ↥F.internalFlags) : F.coreOddSignFn κ₀ φ f = inSign φ (κ₀.match_ ↑f)

The sign an internal flag contributes is the incoming sign at its transition partner.

theorem RS.signAt_eq_prod {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} {κ₀ : F.RelTransitionSystem} (o₀ : κ₀.Orientation) (φ : F.CoreOddColouring ℓ) (vv : W.Vertex) : F.coreOddSignAt o₀ φ vv = ∏ g ∈ relInSetAt o₀ vv, inSign φ (κ₀.match_ g)

The odd-pairing sign at a vertex is the product of the incoming signs over the in-set.