The relative tensor of two free modules #

The relative tensor product of the free modules on two objects is the free module on their tensor product. The comparison is the shuffle: multiply the two algebra factors, having carried the first generator past the second algebra factor.

the shuffle RS.freeModShuffle of RS/Classical/Deligne/ModTensor.lean, Mathlib's middle-four interchange tensorμ followed by multiplication;
freeModTensorIso: the resulting isomorphism of R-modules modTensorMod R (freeMod R V) (freeMod R W) ≅ freeMod R (V ⊗ W).
modTensorπ_freeModTensorIso and freeModTensorIso_gpair: the isomorphism computes the projection, hence the pairing RS.gpair, as the shuffle.

Coherence for the shuffle #

source

def RS.freeModSlide {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R V : D) :

CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj R V) R ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj R R) V

The braided coherence morphism carrying a generator past a scalar: (R ⊗ V) ⊗ R ⟶ (R ⊗ R) ⊗ V.

Equations

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

Instances For

source

theorem RS.freeModSlide_whiskerRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R V W : D) :

The middle-four interchange at a free pair, cut open along the last factor: it is the slide of the generator past the scalar, whiskered by that factor.

source

theorem RS.freeModSlide_tensorμ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R V W : D) :

Associativity of the shuffle: sliding and then interchanging against a third scalar agrees with interchanging against the product of the last two scalars. This is the coherence behind the balance relation of the relative tensor product.

source

theorem RS.tensorμ_whiskerLeft_shuffle {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R V W : D) :

Equivariance of the shuffle: acting on the leading scalar and then interchanging agrees with interchanging and then acting. This is the coherence behind the linearity of the comparison.

source

Interchanging against a unit scalar is a reassociation.

The shuffle #

source

theorem RS.whiskerRight_mul_tensorμ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] (V W : D) :

Multiplying the leading scalars moves through the interchange.

source

theorem RS.whiskerLeft_mul_tensorμ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] (V W : D) :

Multiplying the trailing scalars moves through the interchange.

source

theorem RS.whiskerLeft_one_tensorμ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] (V W : D) :

The trailing unit moves through the interchange.

source

theorem RS.whiskerRight_mul_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] (X : D) :

Associativity of the algebra, whiskered by an object.

source

theorem RS.whiskerLeft_one_freeModShuffle {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] (V W : D) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one W))) (freeModShuffle R V W) = (CategoryTheory.MonoidalCategoryStruct.associator R V W).hom

The unit inverts the shuffle: filling the second algebra slot with the unit turns the shuffle into a reassociation.

The balance and equivariance of the shuffle #

source

The braided right action on a free module is the slide followed by multiplication: the generator is carried out of the way and the two algebra factors multiply.

source

theorem RS.freeModShuffle_condition_raw {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) :

The shuffle is balanced, in raw form: the two legs of the relative tensor product of the free modules agree after it.

source

theorem RS.freeModShuffle_act_raw {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] (V W : D) :

The shuffle is equivariant, in raw form: acting on the leading scalar and shuffling agrees with shuffling and acting.

source

theorem RS.freeModShuffle_associator_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj R V) R W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj R V) R).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V))) W) = CategoryTheory.CategoryStruct.comp (freeModShuffle R V W) (CategoryTheory.MonoidalCategoryStruct.associator R V W).inv

The shuffle absorbs the reassociation of the first leg.

source

theorem RS.freeModShuffle_unit_legM {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) :

Inserting the unit is a section of the first leg: the shuffle followed by the insertion is the insertion followed by the first leg.

source

theorem RS.freeModUnit_legN {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] (V W : D) :

Inserting the unit is a retraction of the second leg.

The isomorphism #

source

theorem RS.freeModShuffle_condition {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) :

CategoryTheory.CategoryStruct.comp (modTensorLegM R (freeMod R V) (freeMod R W)) (freeModShuffle R V W) = CategoryTheory.CategoryStruct.comp (modTensorLegN R (freeMod R V) (freeMod R W)) (freeModShuffle R V W)

The shuffle is balanced: it coequalizes the two legs of the relative tensor product of the two free modules.

source

noncomputable def RS.freeModTensorCarrier {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) :

modTensor R (freeMod R V) (freeMod R W) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj R (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)

The relative tensor of two free modules is free, at the level of underlying objects: the shuffle descends to an isomorphism, inverted by filling the second algebra slot with the unit.

Equations

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

Instances For

source

theorem RS.freeModTensorCarrier_linear {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) :

CategoryTheory.CategoryStruct.comp (modTensorAct R (freeMod R V) (freeMod R W)) (freeModTensorCarrier R V W).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (freeModTensorCarrier R V W).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)))

The descended shuffle is R-linear.

source

noncomputable def RS.freeModTensorIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) :

modTensorMod R (freeMod R V) (freeMod R W) ≅ freeMod R (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)

The relative tensor of two free modules is the free module on the tensor product.

Equations

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

Instances For

source

theorem RS.modTensorπ_freeModTensorIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) :

CategoryTheory.CategoryStruct.comp (modTensorπ R (freeMod R V) (freeMod R W)) (freeModTensorIso R V W).hom.hom = freeModShuffle R V W

The isomorphism computes the projection as the shuffle.

source

theorem RS.freeModTensorIso_gpair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) {X Y : D} (m : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (n : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) :

CategoryTheory.CategoryStruct.comp (gpair m n) (freeModTensorIso R V W).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (freeModShuffle R V W)

The isomorphism computes the pairing as the shuffle: the pairing RS.gpair of two morphisms into free modules is, after the identification with the free module on the tensor product, the tensor of the two morphisms followed by the shuffle.

Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.FreeModTensor

The relative tensor of two free modules #

Coherence for the shuffle #

The shuffle #

The balance and equivariance of the shuffle #

The isomorphism #