Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.FreePow

The relative power of a free module #

Over an internal commutative monoid A in a symmetric monoidal category, the module power of the free module A ⊗ V collapses to the free module on the ambient tensor power: modPow A (A ⊗ V) (n + 1) ≅ A ⊗ tensorPow D V (n + 1). At arity zero the module power is the unit object while A ⊗ 𝟙_ D ≅ A, so the collapse starts at arity one.

Throughout, the module structure on A ⊗ V is freeModObj A V — multiplication into the head factor — installed as a local instance for the whole file; the statements of record are spelt at the carrier A ⊗ V with that instance.

The multiplication fold of a monoid power #

source
noncomputable def RS.muFold {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (n : ℕ) :
tensorPow D A n ⟶ A

The multiplication fold: the left-to-right product tensorPow D A n ⟶ A, one factor at a time; the empty product is the unit.

Equations
Instances For
    source
    @[simp]
    theorem RS.muFold_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] :
    muFold A 0 = CategoryTheory.MonObj.one

    Permutation invariance of the fold #

    source
    theorem RS.swapTop_muFold {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (n : ℕ) :
    CategoryTheory.CategoryStruct.comp (swapTop A n) (muFold A (n + 2)) = muFold A (n + 2)

    The top transposition is absorbed by the fold.

    source
    theorem RS.insertTop_muFold {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (n k : ℕ) :
    CategoryTheory.CategoryStruct.comp (insertTop A n k) (muFold A (n + 1)) = muFold A (n + 1)

    Bubbling is absorbed by the fold.

    source
    theorem RS.muFold_permMor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (n : ℕ) (σ : Equiv.Perm (Fin n)) :
    CategoryTheory.CategoryStruct.comp (permMor A n σ) (muFold A n) = muFold A n

    Permutation invariance of the fold: the fold of a commutative monoid absorbs the symmetric-group action.

    The free collapse #

    source
    noncomputable def RS.freeCollapse {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (n : ℕ) :
    tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) n ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A (tensorPow D V n)

    The free collapse: multiply all the heads of a power of free letters to the front of the word.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem RS.freeCollapse_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) :
      freeCollapse A V 0 = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
      source
      theorem RS.freeCollapse_succ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (n : ℕ) :
      freeCollapse A V (n + 1) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (freeCollapse A V n) (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)) (freeModShuffle A (tensorPow D V n) V)

      The defining recursion of the collapse.

      source
      theorem RS.freeCollapse_shuffle {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (n : ℕ) :
      freeCollapse A V n = CategoryTheory.CategoryStruct.comp (plainShuffle A V n).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight (muFold A n) (tensorPow D V n))

      The collapse through the diagonal shuffle: sorting the word and folding the heads is the collapse.

      source
      theorem RS.freeCollapse_permMor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) [CategoryTheory.IsCommMonObj A] (n : ℕ) (σ : Equiv.Perm (Fin n)) :
      CategoryTheory.CategoryStruct.comp (permMor (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) n σ) (freeCollapse A V n) = CategoryTheory.CategoryStruct.comp (freeCollapse A V n) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (permMor V n σ))

      Permutation equivariance of the collapse: sorting the free letters and then collapsing is collapsing and then sorting the ambient letters — the heads are folded by a commutative multiplication, which absorbs the permutation.