Mixed partition functions: the vertex functional

The mixed partition function (Regts–Sevenster arXiv:1807.04494, Definition 5) is defined in RS/Definitions.lean. This module proves the evaluator's antisymmetry — reordering an odd list changes evalOdd by the sign of the permutation, and lists with repeated colours evaluate to zero — and the transport of the Definition 5 summand along fragment equivalences.

theorem RS.MixedFunctional.evalOdd_of_not_nodup {k ℓ : ℕ} (h : MixedFunctional k ℓ) (μ : Multiset (Fin k)) {w : List (Fin (2 * ℓ))} (hw : ¬w.Nodup) : h.evalOdd μ w = 0

Evaluation on a list with a repetition vanishes.

theorem RS.MixedFunctional.evalOdd_swap_adjacent {k ℓ : ℕ} (h : MixedFunctional k ℓ) (μ : Multiset (Fin k)) (l₁ l₂ : List (Fin (2 * ℓ))) {a b : Fin (2 * ℓ)} (hab : a ≠ b) : h.evalOdd μ (l₁ ++ b :: a :: l₂) = -h.evalOdd μ (l₁ ++ a :: b :: l₂)

Swapping distinct adjacent odd colours flips the alternating evaluation.

theorem RS.MixedFunctional.evalOdd_pair_block_swap {k ℓ : ℕ} (h : MixedFunctional k ℓ) (μ : Multiset (Fin k)) (l₁ l₂ : List (Fin (2 * ℓ))) {p₁ p₂ q₁ q₂ : Fin (2 * ℓ)} (hp₁q₁ : p₁ ≠ q₁) (hp₁q₂ : p₁ ≠ q₂) (hp₂q₁ : p₂ ≠ q₁) (hp₂q₂ : p₂ ≠ q₂) : h.evalOdd μ (l₁ ++ q₁ :: q₂ :: p₁ :: p₂ :: l₂) = h.evalOdd μ (l₁ ++ p₁ :: p₂ :: q₁ :: q₂ :: l₂)

Moving a two-element block of odd colours past another preserves the alternating evaluation.

theorem RS.MixedFunctional.evalOdd_flatMap_perm {k ℓ : ℕ} (h : MixedFunctional k ℓ) (μ : Multiset (Fin k)) {β : Type} (pairFn : β → List (Fin (2 * ℓ))) (hlen : ∀ (b : β), (pairFn b).length = 2) {l₁ l₂ : List β} (hperm : l₁.Perm l₂) (pre : List (Fin (2 * ℓ))) : h.evalOdd μ (pre ++ List.flatMap pairFn l₁) = h.evalOdd μ (pre ++ List.flatMap pairFn l₂)

The alternating evaluation is invariant under permuting a list of length-two blocks: each transposition of adjacent blocks moves an even number of elements.

theorem RS.oddPartner_invol (ℓ : ℕ) (c : Fin (2 * ℓ)) : oddPartner ℓ (oddPartner ℓ c) = c

The odd-colour pairing is an involution.

theorem RS.mem_inFlagsAt_of {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.TransitionSystem} {o : κ.Orientation} {v : W.Vertex} {f : W.Flag} (hmem : f ∈ F.flags) (hatt : W.attach f = Sum.inl v) (hin : o.isOut f = false) : f ∈ F.inFlagsAt o v

Flags attached at the vertex and incoming are in the incoming list.

noncomputable def RS.EdgeSubset.TransitionSystem.Orientation.transport {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} {κ : F.TransitionSystem} (o : κ.Orientation) : (TransitionSystem.transport e κ).Orientation

Transport of an orientation along a fragment equivalence.

Equations

• RS.EdgeSubset.TransitionSystem.Orientation.transport e o = { isOut := fun (f : W₂.Flag) => o.isOut (e.flagEquiv.symm f), match_flip := ⋯, pairing_flip := ⋯ }

noncomputable def RS.EdgeSubset.transportComplEquiv {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) (F : EdgeSubset W₁) : { f : W₁.Flag // f ∉ F.flags } ≃ { f : W₂.Flag // f ∉ ((transport e) F).flags }

The complement flag equivalence of a transported edge subset.

Equations

• RS.EdgeSubset.transportComplEquiv e F = e.flagEquiv.subtypeEquiv ⋯

noncomputable def RS.EdgeSubset.EvenColouring.transport {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} {k : ℕ} (ψ : F.EvenColouring k) : ((EdgeSubset.transport e) F).EvenColouring k

Transport of even colourings along a fragment equivalence.

Equations

• RS.EdgeSubset.EvenColouring.transport e ψ = ⟨fun (f : { f : W₂.Flag // f ∉ ((RS.EdgeSubset.transport e) F).flags }) => ↑ψ ((RS.EdgeSubset.transportComplEquiv e F).symm f), ⋯⟩

noncomputable def RS.EdgeSubset.OddColouring.transport {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} {ℓ : ℕ} (φ : F.OddColouring ℓ) : ((EdgeSubset.transport e) F).OddColouring ℓ

Transport of odd colourings along a fragment equivalence.

Equations

• RS.EdgeSubset.OddColouring.transport e φ = ⟨fun (f : ↥((RS.EdgeSubset.transport e) F).flags) => ↑φ ((RS.EdgeSubset.transportFlagsEquiv e F).symm f), ⋯⟩

theorem RS.EdgeSubset.evenColoursAt_transport {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} {k : ℕ} (ψ : F.EvenColouring k) (v : W₁.Vertex) : ((transport e) F).evenColoursAt (EvenColouring.transport e ψ) (e.vertexEquiv v) = F.evenColoursAt ψ v

The even-colour multiset is preserved by transport.

theorem RS.EdgeSubset.inFlagsAt_transport_perm {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} {κ : F.TransitionSystem} (o : κ.Orientation) (v : W₁.Vertex) : (((transport e) F).inFlagsAt (TransitionSystem.Orientation.transport e o) (e.vertexEquiv v)).Perm (List.map (⇑e.flagEquiv) (F.inFlagsAt o v))

The transported in-flag list is a permutation of the image of the original: both enumerate the same transported filter set.

theorem RS.EdgeSubset.OddColouring.transport_apply {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} {ℓ : ℕ} (φ : F.OddColouring ℓ) (g : W₁.Flag) (hg : g ∈ F.flags) (hg' : e.flagEquiv g ∈ ((EdgeSubset.transport e) F).flags) : ↑(transport e φ) ⟨e.flagEquiv g, hg'⟩ = ↑φ ⟨g, hg⟩

A transported odd colouring evaluated at a transported flag is the original colour.

theorem RS.EdgeSubset.TransitionSystem.transport_match {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} (κ : F.TransitionSystem) (g : W₁.Flag) : (transport e κ).match_ (e.flagEquiv g) = e.flagEquiv (κ.match_ g)

The transported matching at a transported flag is the transported matched flag.

theorem RS.EdgeSubset.oddPairFn_transport {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} {ℓ : ℕ} (κ : F.TransitionSystem) (φ : F.OddColouring ℓ) (f : ↥F.flags) (hf : e.flagEquiv ↑f ∈ ((transport e) F).flags) : ((transport e) F).oddPairFn (TransitionSystem.transport e κ) (OddColouring.transport e φ) ⟨e.flagEquiv ↑f, hf⟩ = F.oddPairFn κ φ f

The odd pair at a transported flag under transported data is the original odd pair.

theorem RS.EdgeSubset.oddSignFn_transport {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} {ℓ : ℕ} (κ : F.TransitionSystem) (φ : F.OddColouring ℓ) (f : ↥F.flags) (hf : e.flagEquiv ↑f ∈ ((transport e) F).flags) : ((transport e) F).oddSignFn (TransitionSystem.transport e κ) (OddColouring.transport e φ) ⟨e.flagEquiv ↑f, hf⟩ = F.oddSignFn κ φ f

The odd sign at a transported flag under transported data is the original odd sign.

theorem RS.EdgeSubset.oddSignAt_transport {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} {ℓ : ℕ} {κ : F.TransitionSystem} (o : κ.Orientation) (φ : F.OddColouring ℓ) (v : W₁.Vertex) : ((transport e) F).oddSignAt (TransitionSystem.Orientation.transport e o) (OddColouring.transport e φ) (e.vertexEquiv v) = F.oddSignAt o φ v

The odd sign at a vertex is preserved by transport.

theorem RS.EdgeSubset.evalOdd_oddListAt_transport {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} {k ℓ : ℕ} (h : MixedFunctional k ℓ) (μ : Multiset (Fin k)) {κ : F.TransitionSystem} (o : κ.Orientation) (φ : F.OddColouring ℓ) (v : W₁.Vertex) : h.evalOdd μ (((transport e) F).oddListAt (TransitionSystem.Orientation.transport e o) (OddColouring.transport e φ) (e.vertexEquiv v)) = h.evalOdd μ (F.oddListAt o φ v)

The alternating evaluation of the odd list at a vertex is preserved by transport: the in-flag order changes only by moving whole pairs, and pair blocks move evenly.

noncomputable def RS.EdgeSubset.EvenColouring.transportEquiv {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) (F : EdgeSubset W₁) (k : ℕ) : F.EvenColouring k ≃ ((EdgeSubset.transport e) F).EvenColouring k

Transport of even colourings as an equivalence.

Equations

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

noncomputable def RS.EdgeSubset.OddColouring.transportEquiv {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) (F : EdgeSubset W₁) (ℓ : ℕ) : F.OddColouring ℓ ≃ ((EdgeSubset.transport e) F).OddColouring ℓ

Transport of odd colourings as an equivalence.

Equations

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

theorem RS.EdgeSubset.mixedSummand_transport {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} {k ℓ : ℕ} (h : MixedFunctional k ℓ) {κ : F.TransitionSystem} (o : κ.Orientation) : ((transport e) F).mixedSummand h (TransitionSystem.Orientation.transport e o) = F.mixedSummand h o

Transport invariance of the Definition 5 summand: the summand of a transported edge subset with transported transition system and orientation is the original summand.

theorem RS.oddPartnerSign_oddPartner (ℓ : ℕ) (i : Fin (2 * ℓ)) : oddPartnerSign ℓ (oddPartner ℓ i) = -oddPartnerSign ℓ i

The partner sign flips across the pairing.

theorem RS.oddPartnerSign_mul_self (ℓ : ℕ) (i : Fin (2 * ℓ)) : oddPartnerSign ℓ i * oddPartnerSign ℓ i = 1

The partner sign squares to one.