The colouring model of tensor powers

The d-th tensor power of the standard super space stdSuperPair k ℓ in the pair-component model is an exponentially nested product. The colouring model flattens it: a basis vector of the power is a mixed colouring — each of the d positions carries an even colour in Fin k or an odd colour in Fin (2ℓ) — and the power is the space of functions on colourings, graded by the parity of the odd support. All the §5–6 network maps become colouring combinatorics in this model, meshing directly with the mixed partition function's Definition-5 sum.

@[reducible, inline]

abbrev RS.MixedColouring (k ℓ d : ℕ) : Type

A mixed colouring of d tensor positions: each position an even colour or an odd colour.

Equations

• RS.MixedColouring k ℓ d = (Fin d → Fin k ⊕ Fin (2 * ℓ))

@[instance_reducible]

instance RS.MixedColouring.instFintype (k ℓ d : ℕ) : Fintype (MixedColouring k ℓ d)

Colourings of finitely many slots by finitely many colours are finite in number.

Equations

• RS.MixedColouring.instFintype k ℓ d = { elems := Fintype.piFinset fun (x : Fin d) => Finset.univ, complete := ⋯ }

@[instance_reducible]

instance RS.MixedColouring.instDecidableEq (k ℓ d : ℕ) : DecidableEq (MixedColouring k ℓ d)

And can be compared.

Equations

• RS.MixedColouring.instDecidableEq k ℓ d a b = Fintype.decidablePiFintype a b

def RS.MixedColouring.oddSet {k ℓ d : ℕ} (c : MixedColouring k ℓ d) : Finset (Fin d)

The odd positions of a colouring.

Equations

• c.oddSet = {i : Fin d | (c i).isRight = true}

def RS.MixedColouring.IsEven {k ℓ d : ℕ} (c : MixedColouring k ℓ d) : Prop

A colouring is even when its odd support has even size.

Equations

• c.IsEven = Even c.oddSet.card

@[instance_reducible]

instance RS.MixedColouring.instDecidableIsEven {k ℓ d : ℕ} (c : MixedColouring k ℓ d) : Decidable c.IsEven

Whether a colouring is even is decidable.

Equations

• c.instDecidableIsEven = { decide := decide (c.oddSet.card % 2 = 0), reflects_decide := ⋯ }

noncomputable def RS.colourPower (k ℓ d : ℕ) : SuperVect

The colouring model of the d-th tensor power of the standard super space: functions on mixed colourings, graded by the parity of the odd support.

Equations

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

structure RS.SuperLinearEquiv (V W : SuperVect) : Type

A grading-preserving linear equivalence of super vector spaces.

• evenEquiv : V.even ≃ₗ[ℂ] W.even

  The even component.

• oddEquiv : V.odd ≃ₗ[ℂ] W.odd

  The odd component.

noncomputable def RS.funTensorFun (ι κ : Type) [Fintype ι] [Fintype κ] : TensorProduct ℂ (ι → ℂ) (κ → ℂ) ≃ₗ[ℂ] ι × κ → ℂ

The tensor product of function spaces on finite types is the function space on the product.

Equations

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

noncomputable def RS.superPow (V : SuperVect) : ℕ → SuperVect

The iterated monoidal power of a super vector space, new factors on the right.

Equations

• RS.superPow V 0 = RS.SuperVect.tensorUnit
• RS.superPow V d.succ = (RS.superPow V d).tensorObj V

Splitting a colouring at its last position

def RS.MixedColouring.tail {k ℓ d : ℕ} (c : MixedColouring k ℓ (d + 1)) : MixedColouring k ℓ d

The tail of a colouring: the first d positions.

Equations

• c.tail i = c i.castSucc

theorem RS.MixedColouring.oddSet_card_succ {k ℓ d : ℕ} (c : MixedColouring k ℓ (d + 1)) : c.oddSet.card = c.tail.oddSet.card + if (c (Fin.last d)).isRight = true then 1 else 0

The odd support splits at the last position.

theorem RS.MixedColouring.isEven_succ_left {k ℓ d : ℕ} (c : MixedColouring k ℓ (d + 1)) (a : Fin k) (h : c (Fin.last d) = Sum.inl a) : c.IsEven ↔ c.tail.IsEven

Parity of the extension, last position even.

theorem RS.MixedColouring.isEven_succ_right {k ℓ d : ℕ} (c : MixedColouring k ℓ (d + 1)) (b : Fin (2 * ℓ)) (h : c (Fin.last d) = Sum.inr b) : c.IsEven ↔ ¬c.tail.IsEven

Parity of the extension, last position odd.

noncomputable def RS.colouringSplit (k ℓ d : ℕ) : MixedColouring k ℓ (d + 1) ≃ MixedColouring k ℓ d × (Fin k ⊕ Fin (2 * ℓ))

Splitting a colouring at its last position.

Equations

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

theorem RS.MixedColouring.isEven_split {k ℓ d : ℕ} (c : MixedColouring k ℓ (d + 1)) : c.IsEven ↔ Sum.elim (fun (x : Fin k) => c.tail.IsEven) (fun (x : Fin (2 * ℓ)) => ¬c.tail.IsEven) (c (Fin.last d))

Parity through the split.

def RS.subtypeProdFst {A X : Type} (Q : A → Prop) : { p : A × X // Q p.1 } ≃ { a : A // Q a } × X

A subtype of a product by a condition on the first factor.

Equations

• RS.subtypeProdFst Q = { toFun := fun (p : { p : A × X // Q p.1 }) => (⟨(↑p).1, ⋯⟩, (↑p).2), invFun := fun (q : { a : A // Q a } × X) => ⟨(↑q.1, q.2), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

noncomputable def RS.evenSplitEquiv (k ℓ d : ℕ) : { c : MixedColouring k ℓ (d + 1) // c.IsEven } ≃ { c : MixedColouring k ℓ d // c.IsEven } × Fin k ⊕ { c : MixedColouring k ℓ d // ¬c.IsEven } × Fin (2 * ℓ)

The even colourings of d + 1 positions split by the last colour: an even colour on an even tail, or an odd colour on an odd tail.

Equations

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

noncomputable def RS.oddSplitEquiv (k ℓ d : ℕ) : { c : MixedColouring k ℓ (d + 1) // ¬c.IsEven } ≃ { c : MixedColouring k ℓ d // ¬c.IsEven } × Fin k ⊕ { c : MixedColouring k ℓ d // c.IsEven } × Fin (2 * ℓ)

The odd colourings of d + 1 positions split by the last colour: an even colour on an odd tail, or an odd colour on an even tail.

Equations

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

The equivalence with the iterated power

noncomputable def RS.SuperLinearEquiv.refl (V : SuperVect) : SuperLinearEquiv V V

The identity super linear equivalence.

Equations

• RS.SuperLinearEquiv.refl V = { evenEquiv := LinearEquiv.refl ℂ V.even, oddEquiv := LinearEquiv.refl ℂ V.odd }

noncomputable def RS.SuperLinearEquiv.trans {U V W : SuperVect} (e : SuperLinearEquiv U V) (e' : SuperLinearEquiv V W) : SuperLinearEquiv U W

Composition of super linear equivalences.

Equations

• e.trans e' = { evenEquiv := e.evenEquiv ≪≫ₗ e'.evenEquiv, oddEquiv := e.oddEquiv ≪≫ₗ e'.oddEquiv }

noncomputable def RS.SuperLinearEquiv.tensorCongr {V V' W W' : SuperVect} (e : SuperLinearEquiv V V') (e' : SuperLinearEquiv W W') : SuperLinearEquiv (V.tensorObj W) (V'.tensorObj W')

The tensor of super linear equivalences.

Equations

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

@[instance_reducible]

instance RS.colourZeroEvenUnique (k ℓ : ℕ) : Unique { c : MixedColouring k ℓ 0 // c.IsEven }

At d = 0 there is exactly one even colouring, the empty one.

Equations

• RS.colourZeroEvenUnique k ℓ = { default := ⟨default, ⋯⟩, uniq := ⋯ }

instance RS.colourZeroOddEmpty (k ℓ : ℕ) : IsEmpty { c : MixedColouring k ℓ 0 // ¬c.IsEven }

And no odd one: the zeroth power is purely even.

noncomputable def RS.colourPowerZero (k ℓ : ℕ) : SuperLinearEquiv SuperVect.tensorUnit (colourPower k ℓ 0)

The base of the recursion: the zeroth power is the colouring model of zero positions.

Equations

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

noncomputable def RS.colourPowerStep (k ℓ d : ℕ) : SuperLinearEquiv ((colourPower k ℓ d).tensorObj (stdSuperPair k ℓ)) (colourPower k ℓ (d + 1))

The step of the recursion: tensoring the colouring model with the standard space extends the colourings by one position.

Equations

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

noncomputable def RS.colourPowerEquiv (k ℓ d : ℕ) : SuperLinearEquiv (superPow (stdSuperPair k ℓ) d) (colourPower k ℓ d)

The colouring model of the iterated power: the d-th monoidal power of the standard super space is the colouring model.

Equations

• RS.colourPowerEquiv k ℓ 0 = RS.colourPowerZero k ℓ
• RS.colourPowerEquiv k ℓ d.succ = ((RS.colourPowerEquiv k ℓ d).tensorCongr (RS.SuperLinearEquiv.refl (RS.stdSuperPair k ℓ))).trans (RS.colourPowerStep k ℓ d)