The disjoint union: colour and value splitting #
The colouring sum and the through-summand of a union split into the two components.
Joining even colourings #
noncomputable def
RS.joinEvenVal
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k : ℕ}
(ψ₁ : (leftSub F).EvenColouring k)
(ψ₂ : (rightSub F).EvenColouring k)
:
The underlying map of the join of two even colourings: each non-participating flag takes its own component's colour.
Equations
Instances For
theorem
RS.joinEvenVal_inl
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k : ℕ}
(ψ₁ : (leftSub F).EvenColouring k)
(ψ₂ : (rightSub F).EvenColouring k)
(g : W₁.Flag)
(hg : Sum.inl g ∉ F.flags)
(hg' : g ∉ (leftSub F).flags)
:
The join reads the left colouring at a left flag.
theorem
RS.joinEvenVal_inr
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k : ℕ}
(ψ₁ : (leftSub F).EvenColouring k)
(ψ₂ : (rightSub F).EvenColouring k)
(g : W₂.Flag)
(hg : Sum.inr g ∉ F.flags)
(hg' : g ∉ (rightSub F).flags)
:
The join reads the right colouring at a right flag.
noncomputable def
RS.joinEven
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k : ℕ}
(ψ₁ : (leftSub F).EvenColouring k)
(ψ₂ : (rightSub F).EvenColouring k)
:
F.EvenColouring k
The join of two component even colourings as an even colouring of the union subset.
Equations
- RS.joinEven ψ₁ ψ₂ = ⟨RS.joinEvenVal ψ₁ ψ₂, ⋯⟩
Instances For
noncomputable def
RS.joinEvenEquiv
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
(F : EdgeSubset (W₁.disjUnion W₂))
(k : ℕ)
:
Even colourings of a union subset are pairs of even colourings of the two restrictions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Joining core odd colourings #
noncomputable def
RS.joinCoreVal
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{ℓ : ℕ}
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
:
The underlying map of the join of two core odd colourings: each core flag takes its own component's colour.
Equations
Instances For
theorem
RS.joinCoreVal_inl
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{ℓ : ℕ}
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
(g : W₁.Flag)
(hg : Sum.inl g ∈ F.coreFlags)
(hg' : g ∈ (leftSub F).coreFlags)
:
The core join reads the left colouring at a left flag.
theorem
RS.joinCoreVal_inr
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{ℓ : ℕ}
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
(g : W₂.Flag)
(hg : Sum.inr g ∈ F.coreFlags)
(hg' : g ∈ (rightSub F).coreFlags)
:
The core join reads the right colouring at a right flag.
noncomputable def
RS.joinCore
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{ℓ : ℕ}
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
:
F.CoreOddColouring ℓ
The join of two component core odd colourings as a core odd colouring of the union subset.
Equations
- RS.joinCore φ₁ φ₂ = ⟨RS.joinCoreVal φ₁ φ₂, ⋯⟩
Instances For
noncomputable def
RS.joinCoreEquiv
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
(F : EdgeSubset (W₁.disjUnion W₂))
(ℓ : ℕ)
:
Core odd colourings of a union subset are pairs of core odd colourings of the two restrictions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Boundary-match transfer #
theorem
RS.genEvenBoundaryMatch_join
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k ℓ : ℕ}
{st : GenBoundaryState k ℓ (α ⊕ β)}
(hbnd : genBoundarySubsetMatches (W₁.disjUnion W₂) F.flags st)
(hbnd₁ : genBoundarySubsetMatches W₁ (leftSub F).flags fun (a : α) => st (Sum.inl a))
(hbnd₂ : genBoundarySubsetMatches W₂ (rightSub F).flags fun (b : β) => st (Sum.inr b))
(ψ₁ : (leftSub F).EvenColouring k)
(ψ₂ : (rightSub F).EvenColouring k)
:
genEvenBoundaryMatch F st hbnd (joinEven ψ₁ ψ₂) ↔ genEvenBoundaryMatch (leftSub F) (fun (a : α) => st (Sum.inl a)) hbnd₁ ψ₁ ∧ genEvenBoundaryMatch (rightSub F) (fun (b : β) => st (Sum.inr b)) hbnd₂ ψ₂
A join of even colourings meets the union's boundary constraint exactly when both components meet theirs.
theorem
RS.coreOddBoundaryMatch_join
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k ℓ : ℕ}
{st : GenBoundaryState k ℓ (α ⊕ β)}
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
:
F.coreOddBoundaryMatch st (joinCore φ₁ φ₂) ↔ (leftSub F).coreOddBoundaryMatch (fun (a : α) => st (Sum.inl a)) φ₁ ∧ (rightSub F).coreOddBoundaryMatch (fun (b : β) => st (Sum.inr b)) φ₂
A join of core odd colourings meets the union's boundary constraint exactly when both components meet theirs.
Even colour multisets at component vertices #
noncomputable def
RS.leftComplEmb
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
(F : EdgeSubset (W₁.disjUnion W₂))
:
The left injection embeds the left restriction's non-participating flags into the union's.
Equations
Instances For
noncomputable def
RS.rightComplEmb
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
(F : EdgeSubset (W₁.disjUnion W₂))
:
The right injection embeds the right restriction's non-participating flags into the union's.
Equations
Instances For
theorem
RS.evenColours_aux_inl
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k : ℕ}
(ψ₁ : (leftSub F).EvenColouring k)
(ψ₂ : (rightSub F).EvenColouring k)
(v : W₁.Vertex)
(S : Finset { f : (W₁.disjUnion W₂).Flag // f ∉ F.flags })
(T : Finset { g : W₁.Flag // g ∉ (leftSub F).flags })
(hS : ∀ (x : { f : (W₁.disjUnion W₂).Flag // f ∉ F.flags }), x ∈ S ↔ (W₁.disjUnion W₂).attach ↑x = Sum.inl (Sum.inl v))
(hT : ∀ (y : { g : W₁.Flag // g ∉ (leftSub F).flags }), y ∈ T ↔ W₁.attach ↑y = Sum.inl v)
:
At a left vertex, the join's colour multiset over the flags there is the left colouring's.
theorem
RS.evenColours_aux_inr
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k : ℕ}
(ψ₁ : (leftSub F).EvenColouring k)
(ψ₂ : (rightSub F).EvenColouring k)
(v : W₂.Vertex)
(S : Finset { f : (W₁.disjUnion W₂).Flag // f ∉ F.flags })
(T : Finset { g : W₂.Flag // g ∉ (rightSub F).flags })
(hS : ∀ (x : { f : (W₁.disjUnion W₂).Flag // f ∉ F.flags }), x ∈ S ↔ (W₁.disjUnion W₂).attach ↑x = Sum.inl (Sum.inr v))
(hT : ∀ (y : { g : W₂.Flag // g ∉ (rightSub F).flags }), y ∈ T ↔ W₂.attach ↑y = Sum.inl v)
:
At a right vertex, the join's colour multiset over the flags there is the right colouring's.
theorem
RS.evenColoursAt_join_inl
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k : ℕ}
(ψ₁ : (leftSub F).EvenColouring k)
(ψ₂ : (rightSub F).EvenColouring k)
(v : W₁.Vertex)
:
The join's even colours at a left vertex are the left colouring's.
theorem
RS.evenColoursAt_join_inr
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k : ℕ}
(ψ₁ : (leftSub F).EvenColouring k)
(ψ₂ : (rightSub F).EvenColouring k)
(v : W₂.Vertex)
:
The join's even colours at a right vertex are the right colouring's.
In-flag lists at component vertices #
theorem
RS.relInFlagsAt_join_perm_inl
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{κ₁ : (leftSub F).RelTransitionSystem}
{κ₂ : (rightSub F).RelTransitionSystem}
(o₁ : κ₁.Orientation)
(o₂ : κ₂.Orientation)
(v : W₁.Vertex)
:
(F.relInFlagsAt (prodOrient o₁ o₂) (Sum.inl v)).Perm (List.map Sum.inl ((leftSub F).relInFlagsAt o₁ v))
At a left vertex, the product orientation's in-flags are the left factor's, injected — up to the enumeration order.
theorem
RS.relInFlagsAt_join_perm_inr
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{κ₁ : (leftSub F).RelTransitionSystem}
{κ₂ : (rightSub F).RelTransitionSystem}
(o₁ : κ₁.Orientation)
(o₂ : κ₂.Orientation)
(v : W₂.Vertex)
:
(F.relInFlagsAt (prodOrient o₁ o₂) (Sum.inr v)).Perm (List.map Sum.inr ((rightSub F).relInFlagsAt o₂ v))
At a right vertex, the product orientation's in-flags are the right factor's, injected — up to the enumeration order.
theorem
RS.mem_internal_of_mem_map_inl
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{κ₁ : (leftSub F).RelTransitionSystem}
{o₁ : κ₁.Orientation}
{v : W₁.Vertex}
{f : (W₁.disjUnion W₂).Flag}
(hf : f ∈ List.map Sum.inl ((leftSub F).relInFlagsAt o₁ v))
:
An injected left in-flag is an internal flag of the union subset.
theorem
RS.mem_internal_of_mem_map_inr
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{κ₂ : (rightSub F).RelTransitionSystem}
{o₂ : κ₂.Orientation}
{v : W₂.Vertex}
{f : (W₁.disjUnion W₂).Flag}
(hf : f ∈ List.map Sum.inr ((rightSub F).relInFlagsAt o₂ v))
:
An injected right in-flag is an internal flag of the union subset.
pmap helpers (mirrors MixedPartition) #
theorem
RS.pmap_flatMap_congr'
{β' : Type u_1}
{β₁ : Type u_2}
{β₂ : Type u_3}
{γ' : Type u_4}
{p₁ p₂ : β' → Prop}
(f₁ : (b : β') → p₁ b → β₁)
(f₂ : (b : β') → p₂ b → β₂)
(G₁ : β₁ → List γ')
(G₂ : β₂ → List γ')
(l : List β')
(H₁ : ∀ b ∈ l, p₁ b)
(H₂ : ∀ b ∈ l, p₂ b)
(hpt : ∀ b ∈ l, ∀ (h₁ : p₁ b) (h₂ : p₂ b), G₁ (f₁ b h₁) = G₂ (f₂ b h₂))
:
Two pmap-then-flatMap passes over one list agree when they
agree elementwise.
Vertex-local core data at component vertices #
theorem
RS.coreOddSignFn_join_inl
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{ℓ : ℕ}
{κ₁ : (leftSub F).RelTransitionSystem}
{κ₂ : (rightSub F).RelTransitionSystem}
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
(g : W₁.Flag)
(hg' : Sum.inl g ∈ F.internalFlags)
(hg : g ∈ (leftSub F).internalFlags)
:
The join's odd sign at a left internal flag is the left factor's.
theorem
RS.coreOddSignFn_join_inr
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{ℓ : ℕ}
{κ₁ : (leftSub F).RelTransitionSystem}
{κ₂ : (rightSub F).RelTransitionSystem}
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
(g : W₂.Flag)
(hg' : Sum.inr g ∈ F.internalFlags)
(hg : g ∈ (rightSub F).internalFlags)
:
The join's odd sign at a right internal flag is the right factor's.
theorem
RS.coreOddPairFn_join_inl
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{ℓ : ℕ}
{κ₁ : (leftSub F).RelTransitionSystem}
{κ₂ : (rightSub F).RelTransitionSystem}
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
(g : W₁.Flag)
(hg' : Sum.inl g ∈ F.internalFlags)
(hg : g ∈ (leftSub F).internalFlags)
:
The join's odd pair at a left internal flag is the left factor's, injected.
theorem
RS.coreOddPairFn_join_inr
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{ℓ : ℕ}
{κ₁ : (leftSub F).RelTransitionSystem}
{κ₂ : (rightSub F).RelTransitionSystem}
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
(g : W₂.Flag)
(hg' : Sum.inr g ∈ F.internalFlags)
(hg : g ∈ (rightSub F).internalFlags)
:
The join's odd pair at a right internal flag is the right factor's, injected.
theorem
RS.coreOddSignAt_join_inl
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{ℓ : ℕ}
{κ₁ : (leftSub F).RelTransitionSystem}
{κ₂ : (rightSub F).RelTransitionSystem}
(o₁ : κ₁.Orientation)
(o₂ : κ₂.Orientation)
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
(v : W₁.Vertex)
:
The join's odd-pairing sign at a left vertex is the left factor's.
theorem
RS.coreOddSignAt_join_inr
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{ℓ : ℕ}
{κ₁ : (leftSub F).RelTransitionSystem}
{κ₂ : (rightSub F).RelTransitionSystem}
(o₁ : κ₁.Orientation)
(o₂ : κ₂.Orientation)
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
(v : W₂.Vertex)
:
F.coreOddSignAt (prodOrient o₁ o₂) (joinCore φ₁ φ₂) (Sum.inr v) = (rightSub F).coreOddSignAt o₂ φ₂ v
The join's odd-pairing sign at a right vertex is the right factor's.
theorem
RS.evalOdd_coreOddListAt_join_inl
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(μ : Multiset (Fin k))
{κ₁ : (leftSub F).RelTransitionSystem}
{κ₂ : (rightSub F).RelTransitionSystem}
(o₁ : κ₁.Orientation)
(o₂ : κ₂.Orientation)
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
(v : W₁.Vertex)
:
h.evalOdd μ (F.coreOddListAt (prodOrient o₁ o₂) (joinCore φ₁ φ₂) (Sum.inl v)) = h.evalOdd μ ((leftSub F).coreOddListAt o₁ φ₁ v)
The vertex functional's odd evaluation at a left vertex reads the left factor's odd list.
theorem
RS.evalOdd_coreOddListAt_join_inr
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(μ : Multiset (Fin k))
{κ₁ : (leftSub F).RelTransitionSystem}
{κ₂ : (rightSub F).RelTransitionSystem}
(o₁ : κ₁.Orientation)
(o₂ : κ₂.Orientation)
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
(v : W₂.Vertex)
:
h.evalOdd μ (F.coreOddListAt (prodOrient o₁ o₂) (joinCore φ₁ φ₂) (Sum.inr v)) = h.evalOdd μ ((rightSub F).coreOddListAt o₂ φ₂ v)
The vertex functional's odd evaluation at a right vertex reads the right factor's odd list.
The colouring-sum factorization #
theorem
RS.joinEvenEquiv_apply
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k : ℕ}
(ψ₁ : (leftSub F).EvenColouring k)
(ψ₂ : (rightSub F).EvenColouring k)
:
The even-colouring equivalence is the join.
theorem
RS.joinCoreEquiv_apply
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{ℓ : ℕ}
(φ₁ : (leftSub F).CoreOddColouring ℓ)
(φ₂ : (rightSub F).CoreOddColouring ℓ)
:
The core-colouring equivalence is the join.
theorem
RS.colouringSum_split
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
{F : EdgeSubset (W₁.disjUnion W₂)}
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(st : GenBoundaryState k ℓ (α ⊕ β))
(hbnd : genBoundarySubsetMatches (W₁.disjUnion W₂) F.flags st)
(hbnd₁ : genBoundarySubsetMatches W₁ (leftSub F).flags fun (a : α) => st (Sum.inl a))
(hbnd₂ : genBoundarySubsetMatches W₂ (rightSub F).flags fun (b : β) => st (Sum.inr b))
{κ₁ : (leftSub F).RelTransitionSystem}
{κ₂ : (rightSub F).RelTransitionSystem}
(o₁ : κ₁.Orientation)
(o₂ : κ₂.Orientation)
:
(∑ ψ : F.EvenColouring k,
if genEvenBoundaryMatch F st hbnd ψ then
∑ φ : F.CoreOddColouring ℓ,
if F.coreOddBoundaryMatch st φ then
∏ v : (W₁.disjUnion W₂).Vertex,
↑(F.coreOddSignAt (prodOrient o₁ o₂) φ v) * h.evalOdd (F.evenColoursAt ψ v) (F.coreOddListAt (prodOrient o₁ o₂) φ v)
else 0
else 0) = (∑ ψ : (leftSub F).EvenColouring k,
if genEvenBoundaryMatch (leftSub F) (fun (a : α) => st (Sum.inl a)) hbnd₁ ψ then
∑ φ : (leftSub F).CoreOddColouring ℓ,
if (leftSub F).coreOddBoundaryMatch (fun (a : α) => st (Sum.inl a)) φ then
∏ v : W₁.Vertex,
↑((leftSub F).coreOddSignAt o₁ φ v) * h.evalOdd ((leftSub F).evenColoursAt ψ v) ((leftSub F).coreOddListAt o₁ φ v)
else 0
else 0) * ∑ ψ : (rightSub F).EvenColouring k,
if genEvenBoundaryMatch (rightSub F) (fun (b : β) => st (Sum.inr b)) hbnd₂ ψ then
∑ φ : (rightSub F).CoreOddColouring ℓ,
if (rightSub F).coreOddBoundaryMatch (fun (b : β) => st (Sum.inr b)) φ then
∏ v : W₂.Vertex,
↑((rightSub F).coreOddSignAt o₂ φ v) * h.evalOdd ((rightSub F).evenColoursAt ψ v) ((rightSub F).coreOddListAt o₂ φ v)
else 0
else 0
The colouring sum factors: a colouring of the union is a pair of componentwise colourings, and the summand is their product.