Word maps of an arbitrary pair of morphisms

BiprodPow folds the letterwise biproduct inclusions of X ⊞ Y into the mixed inclusions mixedInto and sorts them under the symmetric-group action. Its sorting arguments never use that the letters are biproduct inclusions — only monoidal coherence and naturality. This file replays that machinery at two arbitrary morphisms with a common target, f : U ⟶ Z and g : V ⟶ Z, in a monoidal category.

The letterwise fold of f and g over a word is the word map wordMap. It is natural in the letters: composing with a letterwise fold wordCongrMap of morphisms of the sources composes the letters (wordMap_natural). On a sorted word the word map is the concatenation of the pure powers of f and g (wordMap_standard), and in a symmetric category every word map, followed by the action of its sorting permutation, is that sorted concatenation — up to the isomorphism wordSortIso of the source and an arity transport at the target (wordMap_sorted).

The word powers wordPow, the letter counts popCount, the sorted words standardWord, their structural isomorphism standardMixedIso and the sorting permutations sortPerm are reused from BiprodPow unchanged: they depend only on the two source objects, never on the letter maps.

Letter maps and the word map

def RS.letterMap {A : Type u} [CategoryTheory.Category.{v, u} A] {U V Z : A} (f : U ⟶ Z) (g : V ⟶ Z) (b : Bool) : (bif b then U else V) ⟶ Z

The morphism selected by one letter: f on a true letter and g on a false one.

Equations

• RS.letterMap f g true = f
• RS.letterMap f g false = g

noncomputable def RS.wordMap {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} (f : U ⟶ Z) (g : V ⟶ Z) (n : ℕ) (w : Fin n → Bool) : wordPow U V n w ⟶ tensorPow A Z n

The word map: the fold of the letter maps of f and g over a word, by the recursion of wordPow.

Equations

• RS.wordMap f g 0 x_2 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)
• RS.wordMap f g n.succ w = CategoryTheory.MonoidalCategoryStruct.tensorHom (RS.wordMap f g n (w ∘ Fin.castSucc)) (RS.letterMap f g (w (Fin.last n)))

Naturality in the letters

def RS.letterCongr {A : Type u} [CategoryTheory.Category.{v, u} A] {U V U' V' : A} (α : U' ⟶ U) (β : V' ⟶ V) (b : Bool) : (bif b then U' else V') ⟶ bif b then U else V

The source morphism selected by one letter: α on a true letter and β on a false one.

Equations

• RS.letterCongr α β true = α
• RS.letterCongr α β false = β

theorem RS.letterCongr_letterMap {A : Type u} [CategoryTheory.Category.{v, u} A] {U V Z U' V' : A} (α : U' ⟶ U) (β : V' ⟶ V) (f : U ⟶ Z) (g : V ⟶ Z) (b : Bool) : CategoryTheory.CategoryStruct.comp (letterCongr α β b) (letterMap f g b) = letterMap (CategoryTheory.CategoryStruct.comp α f) (CategoryTheory.CategoryStruct.comp β g) b

A letter's congruence map composed with its letter map is the letter map of the composites.

noncomputable def RS.wordCongrMap {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V U' V' : A} (α : U' ⟶ U) (β : V' ⟶ V) (n : ℕ) (w : Fin n → Bool) : wordPow U' V' n w ⟶ wordPow U V n w

The letterwise congruence map between word powers on the same word: the fold of α on the true letters and β on the false ones, by the recursion of wordPow.

Equations

• RS.wordCongrMap α β 0 x_2 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)
• RS.wordCongrMap α β n.succ w = CategoryTheory.MonoidalCategoryStruct.tensorHom (RS.wordCongrMap α β n (w ∘ Fin.castSucc)) (RS.letterCongr α β (w (Fin.last n)))

theorem RS.wordMap_natural {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z U' V' : A} (α : U' ⟶ U) (β : V' ⟶ V) (f : U ⟶ Z) (g : V ⟶ Z) (n : ℕ) (w : Fin n → Bool) : CategoryTheory.CategoryStruct.comp (wordCongrMap α β n w) (wordMap f g n w) = wordMap (CategoryTheory.CategoryStruct.comp α f) (CategoryTheory.CategoryStruct.comp β g) n w

Naturality of the word map in the letters: the letterwise congruence map composed with the word map of f and g is the word map of the composed letters.

Transport and splitting

theorem RS.wordMap_congr {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} (f : U ⟶ Z) (g : V ⟶ Z) {n : ℕ} {w w' : Fin n → Bool} (h : w = w') : wordMap f g n w = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (wordMap f g n w')

Transport of wordMap along an equality of words.

theorem RS.wordMap_split {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} (f : U ⟶ Z) (g : V ⟶ Z) (n : ℕ) (w : Fin (n + 1) → Bool) (w' : Fin n → Bool) (b : Bool) (hw : w ∘ Fin.castSucc = w') (hb : w (Fin.last n) = b) (h : wordPow U V (n + 1) w = CategoryTheory.MonoidalCategoryStruct.tensorObj (wordPow U V n w') (bif b then U else V)) : wordMap f g (n + 1) w = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) (CategoryTheory.MonoidalCategoryStruct.tensorHom (wordMap f g n w') (letterMap f g b))

Splitting wordMap at the last letter, with the recursion's word and letter replaced by given values.

theorem RS.wordMap_split_false {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} (f : U ⟶ Z) (g : V ⟶ Z) (n : ℕ) (w : Fin (n + 1) → Bool) (w' : Fin n → Bool) (hw : w ∘ Fin.castSucc = w') (hb : w (Fin.last n) = false) (h : wordPow U V (n + 1) w = CategoryTheory.MonoidalCategoryStruct.tensorObj (wordPow U V n w') V) : wordMap f g (n + 1) w = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) (CategoryTheory.MonoidalCategoryStruct.tensorHom (wordMap f g n w') g)

The last-letter split of wordMap at a false letter, with the selected object and morphism spelled as V and g.

theorem RS.wordMap_split_true {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} (f : U ⟶ Z) (g : V ⟶ Z) (n : ℕ) (w : Fin (n + 1) → Bool) (w' : Fin n → Bool) (hw : w ∘ Fin.castSucc = w') (hb : w (Fin.last n) = true) (h : wordPow U V (n + 1) w = CategoryTheory.MonoidalCategoryStruct.tensorObj (wordPow U V n w') U) : wordMap f g (n + 1) w = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) (CategoryTheory.MonoidalCategoryStruct.tensorHom (wordMap f g n w') f)

The last-letter split of wordMap at a true letter, with the selected object and morphism spelled as U and f.

The base-point map

On a sorted word, wordMap is the concatenation of the two pure powers. The gluing helpers are stated at general objects and applied by exact, so that no tensor-power arity enters the rewriting.

theorem RS.wordMap_const_true {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} (f : U ⟶ Z) (g : V ⟶ Z) (n : ℕ) : (wordMap f g n fun (x : Fin n) => true) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (tensorPowMap f n)

On an all-true word the word map is the pure power of f.

theorem RS.wordMap_standard {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} (f : U ⟶ Z) (g : V ⟶ Z) (p q : ℕ) : CategoryTheory.CategoryStruct.comp (standardMixedIso U V p q).inv (wordMap f g (p + q) (standardWord p q)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (tensorPowMap f p) (tensorPowMap g q)) (tensorPowConcat Z p q).hom

The base-point map: on a sorted word, wordMap is the concatenation of the pure powers of the two letter maps.

Sorting

Every word map is the base-point map of its sorted form, up to the symmetric-group action. The bubbling infrastructure — permMor_ofSplit, putBelow, insertTop_full and putBelow_concat — is reused from BiprodPow; the gluing helpers below replicate its private steps at general letters.

theorem RS.wordMap_sorted_exists {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} [CategoryTheory.SymmetricCategory A] (f : U ⟶ Z) (g : V ⟶ Z) (n : ℕ) (w : Fin n → Bool) : ∃ (e : wordPow U V n w ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow A U (popCount w)) (tensorPow A V (n - popCount w))), CategoryTheory.CategoryStruct.comp (wordMap f g n w) (permMor Z n (sortPerm w)) = CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (tensorPowMap f (popCount w)) (tensorPowMap g (n - popCount w))) (CategoryTheory.CategoryStruct.comp (tensorPowConcat Z (popCount w) (n - popCount w)).hom (CategoryTheory.eqToHom ⋯)))

The sorting lemma: every word map is a permuted base-point map. For each word w there is an isomorphism of the word power with U ^ ⊗ popCount w ⊗ V ^ ⊗ (n − popCount w) under which wordMap f g, followed by the action of sortPerm w, is the concatenation of the pure powers of f and g, transported along popCount w + (n − popCount w) = n at the target.

noncomputable def RS.wordSortIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} [CategoryTheory.SymmetricCategory A] (f : U ⟶ Z) (g : V ⟶ Z) (n : ℕ) (w : Fin n → Bool) : wordPow U V n w ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow A U (popCount w)) (tensorPow A V (n - popCount w))

The sorting isomorphism, chosen once and for all from the sorting lemma: wordPow U V n w against the sorted concatenation of pure powers.

Equations

• RS.wordSortIso f g n w = ⋯.choose

theorem RS.wordMap_sorted {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} [CategoryTheory.SymmetricCategory A] (f : U ⟶ Z) (g : V ⟶ Z) (n : ℕ) (w : Fin n → Bool) : CategoryTheory.CategoryStruct.comp (wordMap f g n w) (permMor Z n (sortPerm w)) = CategoryTheory.CategoryStruct.comp (wordSortIso f g n w).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (tensorPowMap f (popCount w)) (tensorPowMap g (n - popCount w))) (CategoryTheory.CategoryStruct.comp (tensorPowConcat Z (popCount w) (n - popCount w)).hom (CategoryTheory.eqToHom ⋯)))

The sorting square, for the chosen isomorphism wordSortIso: the word map of f and g, followed by the action of the sorting permutation, is the concatenation of the pure powers of f and g, up to wordSortIso at the source and the arity transport at the target.