Letter systems and the sign transport

A MixedLetters system exhibits an object of a monoidal category as a family of letters, each of them the unit or a fixed odd line. The tensor power then decomposes into colourings, and a permutation routes a colouring to its shuffle scaled by the Koszul sign of Signs.lean. The matrix of the action of the group algebra is therefore the same in every ambient category carrying such a system, which is what makes the colour sum an obstruction that transports; the two systems it is applied to are built in Standard.lean.

• MixedLetters: the structure, with the colouring maps colourInto/colourFrom, their orthogonality and their completeness sum_colourFrom_colourInto.
• normIso, nIn, nOut: the normalised form of a word power and the colouring maps through it.
• nIn_permMor: the sign transport — a permutation carries a normalised colouring to its shuffle, scaled by parSign.
• colourSum: the colour sum of a group-algebra element, with colourSum_eq_zero and permAlg_eq_zero: an element kills the tensor power exactly when its colour sums vanish.

Letter systems

A MixedLetters system exhibits an object M as a biproduct-style family of letters, each a monoidal unit (even) or a fixed line U (odd), without asking the ambient category for biproducts: only the inclusions, projections, orthogonality and completeness are used.

@[reducible, inline]

abbrev RS.letterObj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (U : A) {K : Type} (par : K → Bool) (k : K) : A

The letter object of a label: the line U when the label is odd, the monoidal unit when it is even.

Equations

• RS.letterObj U par k = bif par k then U else CategoryTheory.MonoidalCategoryStruct.tensorUnit A

structure RS.MixedLetters {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] (K : Type) [Fintype K] (par : K → Bool) (U M : A) : Type v

A letter system on M: unit and U-letters included into and projected from M, orthonormally and completely.

• ins (k : K) : letterObj U par k ⟶ M

  The inclusion of the letter labelled k.

• prj (k : K) : M ⟶ letterObj U par k

  The projection onto the letter labelled k.

• ins_prj (k : K) : CategoryTheory.CategoryStruct.comp (self.ins k) (self.prj k) = CategoryTheory.CategoryStruct.id (letterObj U par k)

  A letter's round trip through M is the identity.

• ins_prj_ne {k k' : K} : k ≠ k' → CategoryTheory.CategoryStruct.comp (self.ins k) (self.prj k') = 0

  Distinct letters' round trips vanish.

• total : ∑ k : K, CategoryTheory.CategoryStruct.comp (self.prj k) (self.ins k) = CategoryTheory.CategoryStruct.id M

  The projections and inclusions decompose the identity.

noncomputable def RS.MixedLetters.colourInto {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (n : ℕ) (c : Fin n → K) : wordPow U (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) n (par ∘ c) ⟶ tensorPow A M n

The inclusion of a colouring: the fold of the letterwise inclusions into the tensor power, in slot order.

Equations

• S.colourInto 0 x_2 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)
• S.colourInto n.succ c = CategoryTheory.MonoidalCategoryStruct.tensorHom (S.colourInto n (c ∘ Fin.castSucc)) (S.ins (c (Fin.last n)))

noncomputable def RS.MixedLetters.colourFrom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (n : ℕ) (c : Fin n → K) : tensorPow A M n ⟶ wordPow U (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) n (par ∘ c)

The projection onto a colouring: the fold of the letterwise projections from the tensor power.

Equations

• S.colourFrom 0 x_2 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)
• S.colourFrom n.succ c = CategoryTheory.MonoidalCategoryStruct.tensorHom (S.colourFrom n (c ∘ Fin.castSucc)) (S.prj (c (Fin.last n)))

theorem RS.MixedLetters.colourInto_succ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (n : ℕ) (c : Fin (n + 1) → K) : S.colourInto (n + 1) c = CategoryTheory.MonoidalCategoryStruct.tensorHom (S.colourInto n (c ∘ Fin.castSucc)) (S.ins (c (Fin.last n)))

The defining recursion of colourInto.

theorem RS.MixedLetters.colourInto_colourFrom_same {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (n : ℕ) (c : Fin n → K) : CategoryTheory.CategoryStruct.comp (S.colourInto n c) (S.colourFrom n c) = CategoryTheory.CategoryStruct.id (wordPow U (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) n (par ∘ c))

Same-colouring round trip: a colouring included into the power and projected back is unchanged.

theorem RS.MixedLetters.colourInto_colourFrom_ne {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} [CategoryTheory.MonoidalPreadditive A] (S : MixedLetters K par U M) (n : ℕ) {c c' : Fin n → K} : c ≠ c' → CategoryTheory.CategoryStruct.comp (S.colourInto n c) (S.colourFrom n c') = 0

Distinct-colouring round trips vanish.

theorem RS.MixedLetters.sum_colourFrom_colourInto {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} [CategoryTheory.MonoidalPreadditive A] (S : MixedLetters K par U M) (n : ℕ) : ∑ c : Fin n → K, CategoryTheory.CategoryStruct.comp (S.colourFrom n c) (S.colourInto n c) = CategoryTheory.CategoryStruct.id (tensorPow A M n)

Completeness of the colouring decomposition: the round trips through the colourings sum to the identity of the power.

Normalising word powers

Every word power of U and the unit normalises, by unitors alone, to the pure power of U counted by the word. Reading the colouring inclusions and projections through this normal form confines every transport to powers of U indexed by counts.

noncomputable def RS.tailIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (U : A) (k : ℕ) (b : Bool) : CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow A U k) (bif b then U else CategoryTheory.MonoidalCategoryStruct.tensorUnit A) ≅ tensorPow A U (k + bif b then 1 else 0)

Absorbing one letter into a power of U: a U-letter extends the power, a unit letter is stripped by the right unitor.

Equations

• RS.tailIso U k true = CategoryTheory.Iso.refl (RS.tensorPow A U (k + 1))
• RS.tailIso U k false = CategoryTheory.MonoidalCategoryStruct.rightUnitor (RS.tensorPow A U k)

noncomputable def RS.normIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (U : A) (n : ℕ) (w : Fin n → Bool) : wordPow U (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) n w ≅ tensorPow A U (popCount w)

The normalisation of a word power: strip the unit letters by unitors, leaving the power of U of the word's count.

Equations

• One or more equations did not get rendered due to their size.
• RS.normIso U 0 w = CategoryTheory.eqToIso ⋯

The normalised colouring maps

noncomputable def RS.MixedLetters.nIn {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (n : ℕ) (c : Fin n → K) : tensorPow A U (popCount (par ∘ c)) ⟶ tensorPow A M n

The normalised inclusion of a colouring: the colouring inclusion, read off the U-power normal form of its word power.

Equations

• S.nIn n c = CategoryTheory.CategoryStruct.comp (RS.normIso U n (par ∘ c)).inv (S.colourInto n c)

noncomputable def RS.MixedLetters.nOut {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (n : ℕ) (c : Fin n → K) : tensorPow A M n ⟶ tensorPow A U (popCount (par ∘ c))

The normalised projection onto a colouring.

Equations

• S.nOut n c = CategoryTheory.CategoryStruct.comp (S.colourFrom n c) (RS.normIso U n (par ∘ c)).hom

theorem RS.MixedLetters.colourInto_eq_nIn {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (n : ℕ) (c : Fin n → K) : S.colourInto n c = CategoryTheory.CategoryStruct.comp (normIso U n (par ∘ c)).hom (S.nIn n c)

The colouring inclusion factors through its normalised form.

theorem RS.MixedLetters.nIn_nOut_same {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (n : ℕ) (c : Fin n → K) : CategoryTheory.CategoryStruct.comp (S.nIn n c) (S.nOut n c) = CategoryTheory.CategoryStruct.id (tensorPow A U (popCount (par ∘ c)))

Same-colouring round trip of the normalised maps.

theorem RS.MixedLetters.nIn_nOut_ne {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} [CategoryTheory.MonoidalPreadditive A] (S : MixedLetters K par U M) (n : ℕ) {c c' : Fin n → K} (h : c ≠ c') : CategoryTheory.CategoryStruct.comp (S.nIn n c) (S.nOut n c') = 0

Distinct-colouring round trips of the normalised maps vanish.

theorem RS.MixedLetters.nIn_succ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (n : ℕ) (c : Fin (n + 1) → K) : S.nIn (n + 1) c = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (tailIso U (popCount (par ∘ c ∘ Fin.castSucc)) (par (c (Fin.last n)))).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom (S.nIn n (c ∘ Fin.castSucc)) (S.ins (c (Fin.last n)))))

The recursion of the normalised inclusion: strip the top letter.

theorem RS.MixedLetters.nIn_congr {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) {n : ℕ} {c c' : Fin n → K} (h : c = c') (hp : popCount (par ∘ c) = popCount (par ∘ c')) : S.nIn n c = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (S.nIn n c')

Transport of the normalised inclusion along an equality of colourings.

Reindexing along the generators

theorem RS.extPerm_inv {n : ℕ} (τ : Equiv.Perm (Fin n)) : (extPerm τ)⁻¹ = extPerm τ⁻¹

Extension to one more slot commutes with inversion.

theorem RS.permIndex_extPerm_castSucc {K : Type u_1} {n : ℕ} (τ : Equiv.Perm (Fin n)) (c : Fin (n + 1) → K) : permIndex (extPerm τ) c ∘ Fin.castSucc = permIndex τ (c ∘ Fin.castSucc)

Reindexing along a top-fixing permutation restricts below the top slot.

theorem RS.permIndex_extPerm_last {K : Type u_1} {n : ℕ} (τ : Equiv.Perm (Fin n)) (c : Fin (n + 1) → K) : permIndex (extPerm τ) c (Fin.last n) = c (Fin.last n)

Reindexing along a top-fixing permutation fixes the top letter.

theorem RS.topSwap_inv {n : ℕ} : topSwap⁻¹ = topSwap

The top transposition is its own inverse.

theorem RS.permIndex_topSwap_last {K : Type u_1} {n : ℕ} (c : Fin (n + 2) → K) : permIndex topSwap c (Fin.last (n + 1)) = c (Fin.last n).castSucc

Reindexing along the top transposition, top letter.

theorem RS.permIndex_topSwap_castSucc_last {K : Type u_1} {n : ℕ} (c : Fin (n + 2) → K) : permIndex topSwap c (Fin.last n).castSucc = c (Fin.last (n + 1))

Reindexing along the top transposition, second letter.

theorem RS.permIndex_topSwap_low {K : Type u_1} {n : ℕ} (c : Fin (n + 2) → K) : permIndex topSwap c ∘ Fin.castSucc ∘ Fin.castSucc = c ∘ Fin.castSucc ∘ Fin.castSucc

Reindexing along the top transposition, lower letters.

The braiding on a pair of letters

The sign transport of the permutation action

The heart of the comparison: on the normal form, the action of a permutation is the transport between the shuffled colourings, scaled by the combinatorial Koszul sign — the same scalar in every ambient category.

@[simp]

theorem RS.MixedLetters.tailIso_false {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U : A} (k : ℕ) : tailIso U k false = CategoryTheory.MonoidalCategoryStruct.rightUnitor (tensorPow A U k)

The unit-letter absorption, spelled.

@[simp]

theorem RS.MixedLetters.tailIso_true {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U : A} (k : ℕ) : tailIso U k true = CategoryTheory.Iso.refl (tensorPow A U (k + 1))

The U-letter absorption, spelled.

theorem RS.MixedLetters.popCount_split {K : Type} {par : K → Bool} {n : ℕ} (c : Fin (n + 1) → K) : popCount (par ∘ c) = popCount (par ∘ c ∘ Fin.castSucc) + bif par (c (Fin.last n)) then 1 else 0

The letter count of a colouring splits off the last letter, in the composite spelling.

theorem RS.MixedLetters.popCount_permIndex' {K : Type} {par : K → Bool} {n : ℕ} (σ : Equiv.Perm (Fin n)) (c : Fin n → K) : popCount (par ∘ c) = popCount (par ∘ permIndex σ c)

Reindexing preserves letter counts, in the composite spelling.

theorem RS.MixedLetters.nIn_split {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (n : ℕ) (c : Fin (n + 1) → K) (c' : Fin n → K) (k : K) (hc : c ∘ Fin.castSucc = c') (hk : c (Fin.last n) = k) (h : popCount (par ∘ c) = popCount (par ∘ c') + bif par k then 1 else 0) : S.nIn (n + 1) c = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (tailIso U (popCount (par ∘ c')) (par k)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom (S.nIn n c') (S.ins k)))

Splitting the normalised inclusion at the last letter, with the tail and last letter replaced by given values.

theorem RS.MixedLetters.nIn_permMor {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (hβ : (β_ U U).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj U U)) {n : ℕ} (σ : Equiv.Perm (Fin n)) (c : Fin n → K) (h : popCount (par ∘ c) = popCount (par ∘ permIndex σ c)) : CategoryTheory.CategoryStruct.comp (S.nIn n c) (permMor M n σ) = parSign σ (par ∘ c) • CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (S.nIn n (permIndex σ c))

The sign transport of the permutation action: on normal forms, a permutation acts on a colouring of a letter system by the transport to the shuffled colouring, scaled by the combinatorial Koszul sign of the shuffle.

The colour sum

The matrix coefficient of a group-algebra element between two colourings: the sum of its coefficients over the permutations routing the one colouring to the other, weighted by the Koszul sign. It is purely combinatorial — the same scalar in every ambient category carrying a letter system.

noncomputable def RS.colourSum {K : Type} [DecidableEq K] (par : K → Bool) {n : ℕ} (x : SymGroupAlgebra n) (c d : Fin n → K) : ℂ

The colour sum: the signed coefficient sum of a group-algebra element over the permutations carrying c to d.

Equations

• RS.colourSum par x c d = ∑ σ : Equiv.Perm (Fin n) with RS.permIndex σ c = d, x.coeff σ * RS.parSign σ (par ∘ c)

theorem RS.colourSum_eq_zero_of_ne {K : Type} [DecidableEq K] (par : K → Bool) {n : ℕ} (x : SymGroupAlgebra n) {c d : Fin n → K} (h : popCount (par ∘ c) ≠ popCount (par ∘ d)) : colourSum par x c d = 0

The colour sum vanishes between colourings of different counts.

theorem RS.MixedLetters.nIn_permAlg_nOut {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] {K : Type} [Fintype K] [DecidableEq K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (hβ : (β_ U U).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj U U)) {n : ℕ} (x : SymGroupAlgebra n) (c d : Fin n → K) : CategoryTheory.CategoryStruct.comp (S.nIn n c) (CategoryTheory.CategoryStruct.comp ((permAlg M n) x) (S.nOut n d)) = if hpop : popCount (par ∘ c) = popCount (par ∘ d) then colourSum par x c d • CategoryTheory.eqToHom ⋯ else 0

The entry formula: between two colourings, the normalised matrix entry of a group-algebra element is the colour sum times the count transport.

theorem RS.MixedLetters.colourFrom_eq_nOut {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] {K : Type} [Fintype K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (n : ℕ) (d : Fin n → K) : S.colourFrom n d = CategoryTheory.CategoryStruct.comp (S.nOut n d) (normIso U n (par ∘ d)).inv

The colouring projection factors through its normalised form.

theorem RS.MixedLetters.colourSum_eq_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] {K : Type} [Fintype K] [DecidableEq K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (hβ : (β_ U U).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj U U)) (hU : ∀ (k : ℕ), CategoryTheory.CategoryStruct.id (tensorPow A U k) ≠ 0) {n : ℕ} {x : SymGroupAlgebra n} (hx : (permAlg M n) x = 0) (c d : Fin n → K) : colourSum par x c d = 0

Extraction: if a group-algebra element acts as zero on the tensor power of the mixed object, all its colour sums vanish — provided no power of the odd line is a zero object.

theorem RS.MixedLetters.permAlg_eq_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] {K : Type} [Fintype K] [DecidableEq K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (hβ : (β_ U U).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj U U)) {n : ℕ} {x : SymGroupAlgebra n} (hx : ∀ (c d : Fin n → K), colourSum par x c d = 0) : (permAlg M n) x = 0

Reconstruction: if all colour sums of a group-algebra element vanish, it acts as zero on the tensor power of the mixed object.