Embeddings of mixed colours

An embedding preserves the order of odd colours and their symplectic partners and signs. Extending a functional by zero along such an embedding preserves its alternating evaluations on the embedded colours and annihilates inputs using any other colour.

structure RS.MixedColourEmbedding (k ℓ K L : ℕ) : Type

Compatible embeddings of the even and odd colour sets.

• even : Fin k ↪ Fin K

  The embedding of even colours.

• odd : Fin (2 * ℓ) ↪o Fin (2 * L)

  The increasing embedding of odd colours.

• partner_eq (c : Fin (2 * ℓ)) : self.odd (oddPartner ℓ c) = oddPartner L (self.odd c)

  Symplectic partners are preserved.

• sign_eq (c : Fin (2 * ℓ)) : oddPartnerSign L (self.odd c) = oddPartnerSign ℓ c

  The signs of symplectic partners are preserved.

def RS.MixedColourEmbedding.dataEmbedding {k ℓ K L : ℕ} (e : MixedColourEmbedding k ℓ K L) : Multiset (Fin k) × Finset (Fin (2 * ℓ)) ↪ Multiset (Fin K) × Finset (Fin (2 * L))

The embedding of the multiset and set data read by a mixed functional.

Equations

• e.dataEmbedding = { toFun := fun (p : Multiset (Fin k) × Finset (Fin (2 * ℓ))) => (Multiset.map (⇑e.even) p.1, Finset.map e.odd.toEmbedding p.2), inj' := ⋯ }

def RS.MixedColourEmbedding.oddInclusion {ℓ L : ℕ} (h : ℓ ≤ L) (c : Fin (2 * ℓ)) : Fin (2 * L)

Preserve first-half odd colours and shift their partners to the enlarged second half.

Equations

• RS.MixedColourEmbedding.oddInclusion h c = if hc : ↑c < ℓ then ⟨↑c, ⋯⟩ else ⟨↑c - ℓ + L, ⋯⟩

def RS.MixedColourEmbedding.ofLE {k ℓ K L : ℕ} (hk : k ≤ K) (hℓ : ℓ ≤ L) : MixedColourEmbedding k ℓ K L

Embed smaller colour spaces by retaining each first-half odd colour and moving its partner into the enlarged second half.

Equations

• RS.MixedColourEmbedding.ofLE hk hℓ = { even := Fin.castLEEmb hk, odd := OrderEmbedding.ofStrictMono (RS.MixedColourEmbedding.oddInclusion hℓ) ⋯, partner_eq := ⋯, sign_eq := ⋯ }

noncomputable def RS.MixedFunctional.extendColours {k ℓ K L : ℕ} (h : MixedFunctional k ℓ) (e : MixedColourEmbedding k ℓ K L) : MixedFunctional K L

Extension by zero to the embedded colour data.

Equations

• h.extendColours e μ F = Function.extend (⇑e.dataEmbedding) (fun (p : Multiset (Fin k) × Finset (Fin (2 * ℓ))) => h p.1 p.2) (fun (x : Multiset (Fin K) × Finset (Fin (2 * L))) => 0) (μ, F)

theorem RS.MixedFunctional.extendColours_map {k ℓ K L : ℕ} (h : MixedFunctional k ℓ) (e : MixedColourEmbedding k ℓ K L) (μ : Multiset (Fin k)) (F : Finset (Fin (2 * ℓ))) : h.extendColours e (Multiset.map (⇑e.even) μ) (Finset.map e.odd.toEmbedding F) = h μ F

The extended functional agrees with the original on embedded multisets and sets.

theorem RS.MixedFunctional.extendColours_eq_zero_of_even {k ℓ K L : ℕ} (h : MixedFunctional k ℓ) (e : MixedColourEmbedding k ℓ K L) (μ : Multiset (Fin K)) (F : Finset (Fin (2 * L))) (c : Fin K) (hc : c ∈ μ) (hout : c ∉ Set.range ⇑e.even) : h.extendColours e μ F = 0

An even colour outside the embedding makes the extended functional vanish.

theorem RS.MixedFunctional.extendColours_eq_zero_of_odd {k ℓ K L : ℕ} (h : MixedFunctional k ℓ) (e : MixedColourEmbedding k ℓ K L) (μ : Multiset (Fin K)) (F : Finset (Fin (2 * L))) (c : Fin (2 * L)) (hc : c ∈ F) (hout : c ∉ Set.range ⇑e.odd) : h.extendColours e μ F = 0

An odd colour outside the embedding makes the extended functional vanish.

theorem RS.MixedFunctional.evalOdd_extendColours_map {k ℓ K L : ℕ} (h : MixedFunctional k ℓ) (e : MixedColourEmbedding k ℓ K L) (μ : Multiset (Fin k)) (w : List (Fin (2 * ℓ))) : (h.extendColours e).evalOdd (Multiset.map (⇑e.even) μ) (List.map (⇑e.odd) w) = h.evalOdd μ w

Alternating evaluation commutes with the colour embedding.

theorem RS.MixedFunctional.evalOdd_extendColours_eq_zero_of_even {k ℓ K L : ℕ} (h : MixedFunctional k ℓ) (e : MixedColourEmbedding k ℓ K L) (μ : Multiset (Fin K)) (w : List (Fin (2 * L))) (c : Fin K) (hc : c ∈ μ) (hout : c ∉ Set.range ⇑e.even) : (h.extendColours e).evalOdd μ w = 0

Alternating evaluation vanishes if an even input colour is outside the embedding.

theorem RS.MixedFunctional.evalOdd_extendColours_eq_zero_of_odd {k ℓ K L : ℕ} (h : MixedFunctional k ℓ) (e : MixedColourEmbedding k ℓ K L) (μ : Multiset (Fin K)) (w : List (Fin (2 * L))) (c : Fin (2 * L)) (hc : c ∈ w) (hout : c ∉ Set.range ⇑e.odd) : (h.extendColours e).evalOdd μ w = 0

Alternating evaluation vanishes if an odd input colour is outside the embedding.