The free collapse descends to the module power

The collapse freeCollapse A V n : (A ⊗ V) ^ ⊗ n ⟶ A ⊗ V ^ ⊗ n of FreePow.lean multiplies all the heads of a word of free letters into a single head at the front. Here it is shown to coequalise the slot relations that present the module power of the free module A ⊗ V, so that it descends to freeCollapseDesc.

The engine is head absorption freeModShuffle A P V viewed as the laxity of the functor V ↦ A ⊗ V: it is natural, associative and unital (freeModShuffle_natural_left, freeModShuffle_assoc_inv, freeModShuffle_unit), and the collapse is its iterate. Generalised associativity of a laxity is freeCollapse_concat, the compatibility of the collapse with concatenation of words.

Given that, a slot relation is local: whiskering the ambient letters away, both legs reduce to the two-letter window ((A ⊗ V) ⊗ A) ⊗ (A ⊗ V) ⟶ A ⊗ (V ⊗ V), on which the left leg multiplies the extra scalar into the first head and the right leg into the second. The two differ by a single crossing of the two heads that are multiplied first — a braid identity of the ambient symmetric structure, freeWindow_braid — which commutativity of A absorbs.

Throughout, the module structure on A ⊗ V is freeModObj A V; the carrier is spelt (freeMod A V).X so that instance synthesis finds it.

The laws of head absorption

theorem RS.freeModShuffle_natural_left {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] {P P' : D} (f : P ⟶ P') (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)) (freeModShuffle A P' V) = CategoryTheory.CategoryStruct.comp (freeModShuffle A P V) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerRight f V))

Naturality of head absorption in the accumulated block.

theorem RS.freeModShuffle_natural_left_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] {P P' : D} (f : P ⟶ P') (V : D) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj A (CategoryTheory.MonoidalCategoryStruct.tensorObj P' V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)) (CategoryTheory.CategoryStruct.comp (freeModShuffle A P' V) h) = CategoryTheory.CategoryStruct.comp (freeModShuffle A P V) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerRight f V)) h)

Naturality of head absorption in the accumulated block.

theorem RS.freeModShuffle_assoc_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (P Q R : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj A P) (CategoryTheory.MonoidalCategoryStruct.tensorObj A Q) (CategoryTheory.MonoidalCategoryStruct.tensorObj A R)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (freeModShuffle A P Q) (CategoryTheory.MonoidalCategoryStruct.tensorObj A R)) (freeModShuffle A (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q) R)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj A P) (freeModShuffle A Q R)) (CategoryTheory.CategoryStruct.comp (freeModShuffle A P (CategoryTheory.MonoidalCategoryStruct.tensorObj Q R)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator P Q R).inv))

Associativity of head absorption, in inverse-associator form: the mirror of RS.freeModShuffle_assoc.

theorem RS.freeModShuffle_assoc_inv_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (P Q R : D) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj A (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q) R) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj A P) (CategoryTheory.MonoidalCategoryStruct.tensorObj A Q) (CategoryTheory.MonoidalCategoryStruct.tensorObj A R)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (freeModShuffle A P Q) (CategoryTheory.MonoidalCategoryStruct.tensorObj A R)) (CategoryTheory.CategoryStruct.comp (freeModShuffle A (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q) R) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj A P) (freeModShuffle A Q R)) (CategoryTheory.CategoryStruct.comp (freeModShuffle A P (CategoryTheory.MonoidalCategoryStruct.tensorObj Q R)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator P Q R).inv) h))

Associativity of head absorption, in inverse-associator form: the mirror of RS.freeModShuffle_assoc.

theorem RS.freeModShuffle_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (P : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj A P) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)))) (CategoryTheory.CategoryStruct.comp (freeModShuffle A P (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.rightUnitor P).hom)) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj A P)).hom

Unitality of head absorption.

The collapse of a concatenation

theorem RS.freeCollapse_concat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (a b : ℕ) : CategoryTheory.CategoryStruct.comp (tensorPowConcat (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) a b).hom (freeCollapse A V (a + b)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (freeCollapse A V a) (freeCollapse A V b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ A (tensorPow D V a) A (tensorPow D V b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D V a) (tensorPow D V b))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (tensorPowConcat V a b).hom)))

The collapse of a concatenation: collapsing a concatenated word is collapsing each part and multiplying the two heads.

The window of a relation slot

The descended collapse

theorem RS.freeCollapse_leg {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (V : D) {n : ℕ} (a b : ℕ) (hab : a + 2 + b = n) : CategoryTheory.CategoryStruct.comp (modPowLegM A (freeMod A V).X a b) (CategoryTheory.CategoryStruct.comp (powCast (freeMod A V).X hab) (freeCollapse A V n)) = CategoryTheory.CategoryStruct.comp (modPowLegN A (freeMod A V).X a b) (CategoryTheory.CategoryStruct.comp (powCast (freeMod A V).X hab) (freeCollapse A V n))

The collapse coequalises the slot relations: a scalar absorbed on either side of a slot ends up in the same head.

noncomputable def RS.freeCollapseDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (V : D) (n : ℕ) : modPow A (freeMod A V).X n ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A (tensorPow D V n)

The descended collapse.

Equations

• RS.freeCollapseDesc A V n = RS.modPowDesc A (RS.freeMod A V).X (RS.freeCollapse A V n) ⋯

@[simp]

theorem RS.modPowπ_freeCollapseDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (V : D) (n : ℕ) : CategoryTheory.CategoryStruct.comp (modPowπ A (freeMod A V).X n) (freeCollapseDesc A V n) = freeCollapse A V n

@[simp]

theorem RS.modPowπ_freeCollapseDesc_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (V : D) (n : ℕ) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj A (tensorPow D V n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowπ A (freeMod A V).X n) (CategoryTheory.CategoryStruct.comp (freeCollapseDesc A V n) h) = CategoryTheory.CategoryStruct.comp (freeCollapse A V n) h