The Λ coend of a pair of functors

Deligne 3.4's object Λ(α, β): the coend over X of α(X)∨ ⊗ β(X), built here as the coend of the diagram (X, Y) ↦ α(Xᘁ) ⊗ β(Y) using the source category's rigidity — for tensor functors the two agree, and this form needs no duals in the target. This file provides the diagram, the coend with its stage maps and dinaturality, the mapping property, and functoriality in both arguments.

def RS.lambdaDiagram {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) : CategoryTheory.Functor Aᵒᵖ (CategoryTheory.Functor A D)

The Λ diagram of a pair of functors: (X, Y) ↦ α(Xᘁ) ⊗ β(Y), contravariant in X through the adjoint mate.

Equations

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

@[simp]

theorem RS.lambdaDiagram_obj_obj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) (X : Aᵒᵖ) (Y : A) : ((lambdaDiagram α β).obj X).obj Y = CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj (Opposite.unop X)ᘁ) (β.obj Y)

@[simp]

theorem RS.lambdaDiagram_obj_map {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) (X : Aᵒᵖ) {X✝ Y✝ : A} (g : X✝ ⟶ Y✝) : ((lambdaDiagram α β).obj X).map g = CategoryTheory.MonoidalCategoryStruct.whiskerLeft (α.obj (Opposite.unop X)ᘁ) (β.map g)

@[simp]

theorem RS.lambdaDiagram_map_app {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) {X✝ Y✝ : Aᵒᵖ} (f : X✝ ⟶ Y✝) (Y : A) : ((lambdaDiagram α β).map f).app Y = CategoryTheory.MonoidalCategoryStruct.whiskerRight (α.map (f.unopᘁ)) (β.obj Y)

@[reducible, inline]

abbrev RS.HasLambda {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) : Prop

Existence of the Λ coend of the pair (α, β).

Equations

• RS.HasLambda α β = CategoryTheory.Limits.HasCoend (RS.lambdaDiagram α β)

noncomputable def RS.lambdaObj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) [HasLambda α β] : D

The Λ object of a pair of functors: the coend of (X, Y) ↦ α(Xᘁ) ⊗ β(Y).

Equations

• RS.lambdaObj α β = CategoryTheory.Limits.coend (RS.lambdaDiagram α β)

noncomputable def RS.lambdaStage {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) [HasLambda α β] (X : A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X) ⟶ lambdaObj α β

The stage map of the Λ coend at an object of the source.

Equations

• RS.lambdaStage α β X = CategoryTheory.Limits.coend.ι (RS.lambdaDiagram α β) X

theorem RS.lambdaStage_condition {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) [HasLambda α β] {X Y : A} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (α.map (fᘁ)) (β.obj X)) (lambdaStage α β X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (α.obj Yᘁ) (β.map f)) (lambdaStage α β Y)

Dinaturality of the stage maps.

theorem RS.lambdaStage_condition_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) [HasLambda α β] {X Y : A} (f : X ⟶ Y) {Z : D} (h : lambdaObj α β ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (α.map (fᘁ)) (β.obj X)) (CategoryTheory.CategoryStruct.comp (lambdaStage α β X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (α.obj Yᘁ) (β.map f)) (CategoryTheory.CategoryStruct.comp (lambdaStage α β Y) h)

Dinaturality of the stage maps.

theorem RS.lambdaObj_hom_ext {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) [HasLambda α β] {W : D} {f g : lambdaObj α β ⟶ W} (h : ∀ (X : A), CategoryTheory.CategoryStruct.comp (lambdaStage α β X) f = CategoryTheory.CategoryStruct.comp (lambdaStage α β X) g) : f = g

Maps out of the Λ object agree once they agree on stages.

noncomputable def RS.lambdaDesc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) [HasLambda α β] {W : D} (f : (X : A) → CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X) ⟶ W) (hf : ∀ ⦃X Y : A⦄ (g : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (α.map (gᘁ)) (β.obj X)) (f X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (α.obj Yᘁ) (β.map g)) (f Y)) : lambdaObj α β ⟶ W

Descend a dinatural family of maps to the Λ object.

Equations

• RS.lambdaDesc α β f hf = CategoryTheory.Limits.coend.desc f hf

@[simp]

theorem RS.lambdaStage_desc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) [HasLambda α β] {W : D} (f : (X : A) → CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X) ⟶ W) (hf : ∀ ⦃X Y : A⦄ (g : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (α.map (gᘁ)) (β.obj X)) (f X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (α.obj Yᘁ) (β.map g)) (f Y)) (X : A) : CategoryTheory.CategoryStruct.comp (lambdaStage α β X) (lambdaDesc α β f hf) = f X

@[simp]

theorem RS.lambdaStage_desc_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) [HasLambda α β] {W : D} (f : (X : A) → CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X) ⟶ W) (hf : ∀ ⦃X Y : A⦄ (g : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (α.map (gᘁ)) (β.obj X)) (f X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (α.obj Yᘁ) (β.map g)) (f Y)) (X : A) {Z : D} (h : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (lambdaStage α β X) (CategoryTheory.CategoryStruct.comp (lambdaDesc α β f hf) h) = CategoryTheory.CategoryStruct.comp (f X) h

def RS.lambdaDiagramMap {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {α α' β β' : CategoryTheory.Functor A D} (η : α ⟶ α') (τ : β ⟶ β') : lambdaDiagram α β ⟶ lambdaDiagram α' β'

Natural transformations in both arguments induce a map of Λ diagrams.

Equations

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

@[simp]

theorem RS.lambdaDiagramMap_app_app {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {α α' β β' : CategoryTheory.Functor A D} (η : α ⟶ α') (τ : β ⟶ β') (X : Aᵒᵖ) (Y : A) : ((lambdaDiagramMap η τ).app X).app Y = CategoryTheory.MonoidalCategoryStruct.tensorHom (η.app (Opposite.unop X)ᘁ) (τ.app Y)

noncomputable def RS.lambdaMap {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {α α' β β' : CategoryTheory.Functor A D} [HasLambda α β] [HasLambda α' β'] (η : α ⟶ α') (τ : β ⟶ β') : lambdaObj α β ⟶ lambdaObj α' β'

Functoriality of the Λ object in both arguments.

Equations

• RS.lambdaMap η τ = CategoryTheory.Limits.coend.map (RS.lambdaDiagramMap η τ)

@[simp]

theorem RS.lambdaStage_map {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {α α' β β' : CategoryTheory.Functor A D} [HasLambda α β] [HasLambda α' β'] (η : α ⟶ α') (τ : β ⟶ β') (X : A) : CategoryTheory.CategoryStruct.comp (lambdaStage α β X) (lambdaMap η τ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (η.app Xᘁ) (τ.app X)) (lambdaStage α' β' X)

@[simp]

theorem RS.lambdaStage_map_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {α α' β β' : CategoryTheory.Functor A D} [HasLambda α β] [HasLambda α' β'] (η : α ⟶ α') (τ : β ⟶ β') (X : A) {Z : D} (h : lambdaObj α' β' ⟶ Z) : CategoryTheory.CategoryStruct.comp (lambdaStage α β X) (CategoryTheory.CategoryStruct.comp (lambdaMap η τ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (η.app Xᘁ) (τ.app X)) (CategoryTheory.CategoryStruct.comp (lambdaStage α' β' X) h)

@[simp]

theorem RS.lambdaMap_id {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {α β : CategoryTheory.Functor A D} [HasLambda α β] : lambdaMap (CategoryTheory.CategoryStruct.id α) (CategoryTheory.CategoryStruct.id β) = CategoryTheory.CategoryStruct.id (lambdaObj α β)

theorem RS.lambdaMap_comp {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {α α' α'' β β' β'' : CategoryTheory.Functor A D} [HasLambda α β] [HasLambda α' β'] [HasLambda α'' β''] (η : α ⟶ α') (η' : α' ⟶ α'') (τ : β ⟶ β') (τ' : β' ⟶ β'') : CategoryTheory.CategoryStruct.comp (lambdaMap η τ) (lambdaMap η' τ') = lambdaMap (CategoryTheory.CategoryStruct.comp η η') (CategoryTheory.CategoryStruct.comp τ τ')

theorem RS.lambdaMap_comp_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {α α' α'' β β' β'' : CategoryTheory.Functor A D} [HasLambda α β] [HasLambda α' β'] [HasLambda α'' β''] (η : α ⟶ α') (η' : α' ⟶ α'') (τ : β ⟶ β') (τ' : β' ⟶ β'') {Z : D} (h : lambdaObj α'' β'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (lambdaMap η τ) (CategoryTheory.CategoryStruct.comp (lambdaMap η' τ') h) = CategoryTheory.CategoryStruct.comp (lambdaMap (CategoryTheory.CategoryStruct.comp η η') (CategoryTheory.CategoryStruct.comp τ τ')) h

noncomputable def RS.unitRigidDual {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] : A

The right dual of the monoidal unit supplied by the rigid structure — the instance the Λ stages use, which need not be the unit-specific instance.

Equations

• RS.unitRigidDual = (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)ᘁ

noncomputable def RS.unitRightDualIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] : unitRigidDual ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit A

The rigid right dual of the monoidal unit is the unit, through the canonical comparison of exact pairings.

Equations

• RS.unitRightDualIso = CategoryTheory.rightDualIso CategoryTheory.HasRightDual.exact CategoryTheory.exactPairingUnit

noncomputable def RS.lambdaUnit {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ lambdaObj α β

The unit of the Λ object of a pair of lax monoidal functors: the units of the functors into the stage at the monoidal unit, through the comparison of the unit with its rigid dual.

Equations

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

theorem RS.coend_hom_ext_of_preserves {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J : Type u} [CategoryTheory.Category.{v, u} J] {E : Type u'} [CategoryTheory.Category.{v', u'} E] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) [CategoryTheory.Limits.HasCoend F] (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend F).multispan G] {Z : E} {f g : G.obj (CategoryTheory.Limits.coend F) ⟶ Z} (h : ∀ (j : J), CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coend.ι F j)) f = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coend.ι F j)) g) : f = g

Maps out of the image of a coend under a colimit-preserving functor agree once they agree on the images of the stages.

theorem RS.tensorLeft_coend_hom_ext {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) [CategoryTheory.Limits.HasCoend F] (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend F).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] {Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj W (CategoryTheory.Limits.coend F) ⟶ Z} (h : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.Limits.coend.ι F j)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.Limits.coend.ι F j)) g) : f = g

Maps out of a tensor by a coend agree once they agree on whiskered stages, provided tensoring preserves the coend's colimit presentation. The workhorse for descending multiplications through Λ ⊗ Λ.

theorem RS.tensorRight_coend_hom_ext {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) [CategoryTheory.Limits.HasCoend F] (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend F).multispan (CategoryTheory.MonoidalCategory.tensorRight W)] {Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Limits.coend F) W ⟶ Z} (h : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.coend.ι F j) W) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.coend.ι F j) W) g) : f = g

Right-hand mirror of RS.tensorLeft_coend_hom_ext.

def RS.tensorLeftCoendCocone {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) (W : D) {Z : D} (k : (j : J) → CategoryTheory.MonoidalCategoryStruct.tensorObj W ((F.obj (Opposite.op j)).obj j) ⟶ Z) (hk : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((F.map g.op).app i)) (k i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((F.obj (Opposite.op j)).map g)) (k j)) : CategoryTheory.Limits.Cocone ((CategoryTheory.Limits.multispanIndexCoend F).multispan.comp (CategoryTheory.MonoidalCategory.tensorLeft W))

The cocone under the whiskered multispan carried by a dinatural family.

Equations

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

@[simp]

theorem RS.tensorLeftCoendCocone_pt {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) (W : D) {Z : D} (k : (j : J) → CategoryTheory.MonoidalCategoryStruct.tensorObj W ((F.obj (Opposite.op j)).obj j) ⟶ Z) (hk : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((F.map g.op).app i)) (k i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((F.obj (Opposite.op j)).map g)) (k j)) : (tensorLeftCoendCocone F W k hk).pt = Z

@[simp]

theorem RS.tensorLeftCoendCocone_ι_app {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) (W : D) {Z : D} (k : (j : J) → CategoryTheory.MonoidalCategoryStruct.tensorObj W ((F.obj (Opposite.op j)).obj j) ⟶ Z) (hk : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((F.map g.op).app i)) (k i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((F.obj (Opposite.op j)).map g)) (k j)) (x : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.multispanShapeCoend J)) : (tensorLeftCoendCocone F W k hk).ι.app x = match x with | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.CategoryStruct.comp (((CategoryTheory.Limits.multispanIndexCoend F).multispan.comp (CategoryTheory.MonoidalCategory.tensorLeft W)).map (CategoryTheory.Limits.WalkingMultispan.Hom.fst a)) (k ((CategoryTheory.Limits.multispanShapeCoend J).fst a)) | CategoryTheory.Limits.WalkingMultispan.right j => k j

noncomputable def RS.tensorLeftCoendDesc {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) [CategoryTheory.Limits.HasCoend F] (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend F).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] {Z : D} (k : (j : J) → CategoryTheory.MonoidalCategoryStruct.tensorObj W ((F.obj (Opposite.op j)).obj j) ⟶ Z) (hk : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((F.map g.op).app i)) (k i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((F.obj (Opposite.op j)).map g)) (k j)) : CategoryTheory.MonoidalCategoryStruct.tensorObj W (CategoryTheory.Limits.coend F) ⟶ Z

Descend a whiskered dinatural family through a tensor by a coend.

Equations

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

@[simp]

theorem RS.whiskerLeft_ι_tensorLeftCoendDesc {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) [CategoryTheory.Limits.HasCoend F] (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend F).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] {Z : D} (k : (j : J) → CategoryTheory.MonoidalCategoryStruct.tensorObj W ((F.obj (Opposite.op j)).obj j) ⟶ Z) (hk : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((F.map g.op).app i)) (k i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((F.obj (Opposite.op j)).map g)) (k j)) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.Limits.coend.ι F j)) (tensorLeftCoendDesc F W k hk) = k j

@[simp]

theorem RS.whiskerLeft_ι_tensorLeftCoendDesc_assoc {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) [CategoryTheory.Limits.HasCoend F] (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend F).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] {Z : D} (k : (j : J) → CategoryTheory.MonoidalCategoryStruct.tensorObj W ((F.obj (Opposite.op j)).obj j) ⟶ Z) (hk : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((F.map g.op).app i)) (k i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((F.obj (Opposite.op j)).map g)) (k j)) (j : J) {Z✝ : D} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.Limits.coend.ι F j)) (CategoryTheory.CategoryStruct.comp (tensorLeftCoendDesc F W k hk) h) = CategoryTheory.CategoryStruct.comp (k j) h

def RS.tensorRightCoendCocone {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) (W : D) {Z : D} (k : (j : J) → CategoryTheory.MonoidalCategoryStruct.tensorObj ((F.obj (Opposite.op j)).obj j) W ⟶ Z) (hk : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((F.map g.op).app i) W) (k i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((F.obj (Opposite.op j)).map g) W) (k j)) : CategoryTheory.Limits.Cocone ((CategoryTheory.Limits.multispanIndexCoend F).multispan.comp (CategoryTheory.MonoidalCategory.tensorRight W))

The cocone under the right-whiskered multispan carried by a dinatural family.

Equations

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

@[simp]

theorem RS.tensorRightCoendCocone_ι_app {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) (W : D) {Z : D} (k : (j : J) → CategoryTheory.MonoidalCategoryStruct.tensorObj ((F.obj (Opposite.op j)).obj j) W ⟶ Z) (hk : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((F.map g.op).app i) W) (k i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((F.obj (Opposite.op j)).map g) W) (k j)) (x : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.multispanShapeCoend J)) : (tensorRightCoendCocone F W k hk).ι.app x = match x with | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.CategoryStruct.comp (((CategoryTheory.Limits.multispanIndexCoend F).multispan.comp (CategoryTheory.MonoidalCategory.tensorRight W)).map (CategoryTheory.Limits.WalkingMultispan.Hom.fst a)) (k ((CategoryTheory.Limits.multispanShapeCoend J).fst a)) | CategoryTheory.Limits.WalkingMultispan.right j => k j

@[simp]

theorem RS.tensorRightCoendCocone_pt {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) (W : D) {Z : D} (k : (j : J) → CategoryTheory.MonoidalCategoryStruct.tensorObj ((F.obj (Opposite.op j)).obj j) W ⟶ Z) (hk : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((F.map g.op).app i) W) (k i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((F.obj (Opposite.op j)).map g) W) (k j)) : (tensorRightCoendCocone F W k hk).pt = Z

noncomputable def RS.tensorRightCoendDesc {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) [CategoryTheory.Limits.HasCoend F] (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend F).multispan (CategoryTheory.MonoidalCategory.tensorRight W)] {Z : D} (k : (j : J) → CategoryTheory.MonoidalCategoryStruct.tensorObj ((F.obj (Opposite.op j)).obj j) W ⟶ Z) (hk : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((F.map g.op).app i) W) (k i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((F.obj (Opposite.op j)).map g) W) (k j)) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Limits.coend F) W ⟶ Z

Descend a right-whiskered dinatural family through a tensor by a coend.

Equations

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

@[simp]

theorem RS.ι_whiskerRight_tensorRightCoendDesc {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) [CategoryTheory.Limits.HasCoend F] (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend F).multispan (CategoryTheory.MonoidalCategory.tensorRight W)] {Z : D} (k : (j : J) → CategoryTheory.MonoidalCategoryStruct.tensorObj ((F.obj (Opposite.op j)).obj j) W ⟶ Z) (hk : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((F.map g.op).app i) W) (k i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((F.obj (Opposite.op j)).map g) W) (k j)) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.coend.ι F j) W) (tensorRightCoendDesc F W k hk) = k j

@[simp]

theorem RS.ι_whiskerRight_tensorRightCoendDesc_assoc {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J D)) [CategoryTheory.Limits.HasCoend F] (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend F).multispan (CategoryTheory.MonoidalCategory.tensorRight W)] {Z : D} (k : (j : J) → CategoryTheory.MonoidalCategoryStruct.tensorObj ((F.obj (Opposite.op j)).obj j) W ⟶ Z) (hk : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((F.map g.op).app i) W) (k i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((F.obj (Opposite.op j)).map g) W) (k j)) (j : J) {Z✝ : D} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.coend.ι F j) W) (CategoryTheory.CategoryStruct.comp (tensorRightCoendDesc F W k hk) h) = CategoryTheory.CategoryStruct.comp (k j) h

theorem RS.braid_shuffle {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {P Q R : A} [CategoryTheory.BraidedCategory A] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ P Q).hom R) (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj Q P) R).hom (CategoryTheory.MonoidalCategoryStruct.associator R Q P).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P Q R).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (β_ Q R).hom) (β_ P (CategoryTheory.MonoidalCategoryStruct.tensorObj R Q)).hom)

The braid shuffle: the two ways of carrying the reversed pair across a third object agree — the Yang–Baxter consequence behind the associativity of the Λ multiplication.

theorem RS.eq_of_whiskerRight_comp_evaluation {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {P Q Z : A} [CategoryTheory.ExactPairing P Q] {h₁ h₂ : Z ⟶ Q} (H : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight h₁ P) (ε_ P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight h₂ P) (ε_ P Q)) : h₁ = h₂

Maps into a right dual agree once their evaluation composites agree.

theorem RS.rightDualTensorIso_inv_comp_evaluation {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] (X Y : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.rightDualTensorIso X Y).inv (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) (ε_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)ᘁ) = ε_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj Yᘁ Xᘁ)

The comparison of the dual of a product with the product of the duals reduces the rigid evaluation to the tensor-pairing evaluation.

theorem RS.whiskerLeft_mate_square {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] (X : A) {Y Y' : A} (g : Y ⟶ Y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (gᘁ) Xᘁ) (CategoryTheory.rightDualTensorIso X Y).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDualTensorIso X Y').inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X gᘁ)

The mate of a left whiskering, through the comparison of the dual of a tensor product with the tensor of the duals: the dinaturality input of the Λ multiplication.

theorem RS.whiskerRight_mate_square {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {X X' : A} (f : X ⟶ X') (Y : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ (fᘁ)) (CategoryTheory.rightDualTensorIso X Y).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDualTensorIso X' Y).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Yᘁ)

The mate of a right whiskering: the left-slot mirror of RS.whiskerLeft_mate_square.

theorem RS.associator_mate_square {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] (X Y Z : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Zᘁ Yᘁ Xᘁ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Zᘁ (CategoryTheory.rightDualTensorIso X Y).inv) (CategoryTheory.rightDualTensorIso (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.rightDualTensorIso Y Z).inv Xᘁ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDualTensorIso X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv ((CategoryTheory.MonoidalCategoryStruct.associator X Y Z).homᘁ))

The mate of the associator, through the comparisons of duals of tensor products: the source-side kernel of the Λ associativity.

theorem RS.cAssoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] [CategoryTheory.BraidedCategory A] (X Y Z : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (β_ Xᘁ Yᘁ).hom (CategoryTheory.rightDualTensorIso X Y).inv) Zᘁ) (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)ᘁ Zᘁ).hom (CategoryTheory.rightDualTensorIso (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Xᘁ Yᘁ Zᘁ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Xᘁ (CategoryTheory.CategoryStruct.comp (β_ Yᘁ Zᘁ).hom (CategoryTheory.rightDualTensorIso Y Z).inv)) (CategoryTheory.CategoryStruct.comp (β_ Xᘁ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)ᘁ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDualTensorIso X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv ((CategoryTheory.MonoidalCategoryStruct.associator X Y Z).homᘁ))))

Associativity of the composite dual comparisons: the full source-side input of the Λ associativity, assembled from the braid shuffle and the mate of the associator.

theorem RS.braiding_mate_square {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] [CategoryTheory.SymmetricCategory A] (X Y : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDualTensorIso Y X).inv ((β_ X Y).homᘁ) = CategoryTheory.CategoryStruct.comp (β_ Xᘁ Yᘁ).hom (CategoryTheory.rightDualTensorIso X Y).inv

The mate of the braiding through the dual-tensor comparisons: the source-side kernel of the Λ commutativity.

noncomputable def RS.unitTensorDualIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] (Y : A) : (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) Y)ᘁ ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Yᘁ unitRigidDual

The tensor dual comparison at the monoidal unit, pinned to the rigid blanket instances that the Λ stages use.

Equations

• RS.unitTensorDualIso Y = CategoryTheory.rightDualTensorIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) Y

noncomputable def RS.unitRigidEvaluation {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] : CategoryTheory.MonoidalCategoryStruct.tensorObj unitRigidDual (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit A

The rigid evaluation of the monoidal unit, at the blanket instance.

Equations

• RS.unitRigidEvaluation = ε_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) RS.unitRigidDual

theorem RS.unitRightDualIso_inv_comp_evaluation {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight unitRightDualIso.inv (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)) unitRigidEvaluation = ε_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)

The unit comparison reduces the blanket evaluation of the unit to the unit pairing.

theorem RS.unitTensorDualIso_inv_comp_evaluation {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] (Y : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (unitTensorDualIso Y).inv (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) Y)) (ε_ (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) Y)ᘁ) = CategoryTheory.monoidalComp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Yᘁ unitRigidDual) (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) Y))) (CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ (CategoryTheory.MonoidalCategoryStruct.whiskerRight unitRigidEvaluation Y)) (ε_ Y Yᘁ))

The pinned tensor dual comparison at the unit reduces the rigid evaluation to the expanded tensor evaluation.

noncomputable def RS.tensorUnitDualIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] (Y : A) : (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit A))ᘁ ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj unitRigidDual Yᘁ

The tensor dual comparison with the unit on the right, pinned to the rigid blanket instances.

Equations

• RS.tensorUnitDualIso Y = CategoryTheory.rightDualTensorIso Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)

theorem RS.tensorUnitDualIso_inv_comp_evaluation {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] (Y : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (tensorUnitDualIso Y).inv (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit A))) (ε_ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit A))ᘁ) = CategoryTheory.monoidalComp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj unitRigidDual Yᘁ) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)))) (CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft unitRigidDual (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ Y Yᘁ) (CategoryTheory.MonoidalCategoryStruct.tensorUnit A))) unitRigidEvaluation)

The pinned tensor dual comparison with the unit on the right reduces the rigid evaluation to the expanded tensor evaluation.

theorem RS.rightUnitor_mate {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] [CategoryTheory.BraidedCategory A] (Y : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Yᘁ).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ unitRightDualIso.inv) (CategoryTheory.CategoryStruct.comp (β_ Yᘁ unitRigidDual).hom (tensorUnitDualIso Y).inv)) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).homᘁ

The mate of the right unitor: the mirror of RS.leftUnitor_mate.

theorem RS.leftUnitor_mate {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] [CategoryTheory.BraidedCategory A] (Y : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Yᘁ).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight unitRightDualIso.inv Yᘁ) (CategoryTheory.CategoryStruct.comp (β_ unitRigidDual Yᘁ).hom (unitTensorDualIso Y).inv)) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).homᘁ

The mate of the left unitor, expressed through the unit and tensor dual comparisons: the source-side input of the Λ unit law.

noncomputable def RS.lambdaMulStage {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] (X Y : A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X)) (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Yᘁ) (β.obj Y)) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)ᘁ) (β.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))

The stage-level multiplication of the Λ object: middle-four exchange, the tensorators of the two functors, and the comparison of the dual of a product with the product of the duals.

Equations

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

theorem RS.lambdaMulStage_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] (X Y Z : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (lambdaMulStage α β X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Zᘁ) (β.obj Z))) (CategoryTheory.CategoryStruct.comp (lambdaMulStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) (lambdaStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X)) (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Yᘁ) (β.obj Y)) (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Zᘁ) (β.obj Z))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X)) (lambdaMulStage α β Y Z)) (CategoryTheory.CategoryStruct.comp (lambdaMulStage α β X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) (lambdaStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))))

The stage-level associativity of the Λ multiplication.

theorem RS.lambdaMulStage_dinat_right {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] (X : A) {Y Y' : A} (g : Y ⟶ Y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X)) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (α.map (gᘁ)) (β.obj Y))) (CategoryTheory.CategoryStruct.comp (lambdaMulStage α β X Y) (lambdaStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (α.obj Y'ᘁ) (β.map g))) (CategoryTheory.CategoryStruct.comp (lambdaMulStage α β X Y') (lambdaStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y')))

Dinaturality of the stage-level multiplication in the right variable: the input of the inner coend descent of the Λ multiplication.

theorem RS.lambdaMulStage_unit_left {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] (Y : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Yᘁ) (β.obj Y))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε α) (α.map unitRightDualIso.inv)) (CategoryTheory.Functor.LaxMonoidal.ε β)) (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Yᘁ) (β.obj Y))) (CategoryTheory.CategoryStruct.comp (lambdaMulStage α β (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) Y) (lambdaStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) Y)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Yᘁ) (β.obj Y))).hom (lambdaStage α β Y)

The stage-level left unit computation: the Λ unit composed into the multiplication at a stage collapses to the left unitor.

theorem RS.lambdaMulStage_dinat_left {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] {X X' : A} (f : X ⟶ X') (Y : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (α.map (fᘁ)) (β.obj X)) (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Yᘁ) (β.obj Y))) (CategoryTheory.CategoryStruct.comp (lambdaMulStage α β X Y) (lambdaStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (α.obj X'ᘁ) (β.map f)) (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Yᘁ) (β.obj Y))) (CategoryTheory.CategoryStruct.comp (lambdaMulStage α β X' Y) (lambdaStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj X' Y)))

Dinaturality of the stage-level multiplication in the left variable: the input of the outer coend descent of the Λ multiplication.

noncomputable def RS.lambdaMulLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] (X : A) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X)))] : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X)) (lambdaObj α β) ⟶ lambdaObj α β

The inner descent of the Λ multiplication: for a fixed left stage, the stage-level multiplication descends through the right coend.

Equations

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

theorem RS.whiskerLeft_stage_lambdaMulLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] (X : A) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X)))] (Y : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X)) (lambdaStage α β Y)) (lambdaMulLeft α β X) = CategoryTheory.CategoryStruct.comp (lambdaMulStage α β X Y) (lambdaStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))

theorem RS.whiskerLeft_stage_lambdaMulLeft_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] (X : A) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X)))] (Y : A) {Z : D} (h : lambdaObj α β ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X)) (lambdaStage α β Y)) (CategoryTheory.CategoryStruct.comp (lambdaMulLeft α β X) h) = CategoryTheory.CategoryStruct.comp (lambdaMulStage α β X Y) (CategoryTheory.CategoryStruct.comp (lambdaStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) h)

theorem RS.lambdaMulLeft_dinat {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] [∀ (W : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] {X X' : A} (f : X ⟶ X') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (α.map (fᘁ)) (β.obj X)) (lambdaObj α β)) (lambdaMulLeft α β X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (α.obj X'ᘁ) (β.map f)) (lambdaObj α β)) (lambdaMulLeft α β X')

Dinaturality of the inner descent in the left variable.

noncomputable def RS.lambdaMul {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] [∀ (W : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))] : CategoryTheory.MonoidalCategoryStruct.tensorObj (lambdaObj α β) (lambdaObj α β) ⟶ lambdaObj α β

The Λ multiplication (Deligne 3.7's product): the stage-level multiplication descended through both coend variables.

Equations

• RS.lambdaMul α β = RS.tensorRightCoendDesc (RS.lambdaDiagram α β) (RS.lambdaObj α β) (fun (X : A) => RS.lambdaMulLeft α β X) ⋯

@[simp]

theorem RS.stage_whiskerRight_lambdaMul {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] [∀ (W : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))] (X : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (lambdaStage α β X) (lambdaObj α β)) (lambdaMul α β) = lambdaMulLeft α β X

@[simp]

theorem RS.stage_whiskerRight_lambdaMul_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] [∀ (W : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))] (X : A) {Z : D} (h : lambdaObj α β ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (lambdaStage α β X) (lambdaObj α β)) (CategoryTheory.CategoryStruct.comp (lambdaMul α β) h) = CategoryTheory.CategoryStruct.comp (lambdaMulLeft α β X) h

theorem RS.stage_tensorHom_lambdaMul {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] [∀ (W : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))] (X Y : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (lambdaStage α β X) (lambdaStage α β Y)) (lambdaMul α β) = CategoryTheory.CategoryStruct.comp (lambdaMulStage α β X Y) (lambdaStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))

The two-stage computation of the Λ multiplication.

theorem RS.lambdaMul_unit_left {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] [∀ (W : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (lambdaUnit α β) (lambdaObj α β)) (lambdaMul α β) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (lambdaObj α β)).hom

The left unit law of the Λ algebra: the Λ unit composed into the Λ multiplication is the left unitor.

theorem RS.lambdaMulStage_unit_right {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] (Y : A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Yᘁ) (β.obj Y)) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Yᘁ) (β.obj Y)) (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε α) (α.map unitRightDualIso.inv)) (CategoryTheory.Functor.LaxMonoidal.ε β))) (CategoryTheory.CategoryStruct.comp (lambdaMulStage α β Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)) (lambdaStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit A))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Yᘁ) (β.obj Y))).hom (lambdaStage α β Y)

The stage-level right unit computation: the mirror of RS.lambdaMulStage_unit_left.

theorem RS.lambdaMul_unit_right {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] [∀ (W : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (lambdaObj α β) (lambdaUnit α β)) (lambdaMul α β) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (lambdaObj α β)).hom

The right unit law of the Λ algebra.

theorem RS.lambda_triple_hom_ext {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [HasLambda α β] [∀ (W : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] [∀ (W : D), CategoryTheory.Limits.PreservesColimit ((CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan.comp (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))) (CategoryTheory.MonoidalCategory.tensorRight W)] [∀ (W W' : D), CategoryTheory.Limits.PreservesColimit ((CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan.comp (CategoryTheory.MonoidalCategory.tensorLeft W)) (CategoryTheory.MonoidalCategory.tensorRight W')] {Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (lambdaObj α β) (lambdaObj α β)) (lambdaObj α β) ⟶ Z} (h : ∀ (X Y W' : A), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (lambdaStage α β X) (lambdaStage α β Y)) (lambdaStage α β W')) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (lambdaStage α β X) (lambdaStage α β Y)) (lambdaStage α β W')) g) : f = g

Maps out of the triple tensor of the Λ object agree once they agree on triples of stages.

theorem RS.lambdaMul_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] [∀ (W : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))] [∀ (W : D), CategoryTheory.Limits.PreservesColimit ((CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan.comp (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))) (CategoryTheory.MonoidalCategory.tensorRight W)] [∀ (W W' : D), CategoryTheory.Limits.PreservesColimit ((CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan.comp (CategoryTheory.MonoidalCategory.tensorLeft W)) (CategoryTheory.MonoidalCategory.tensorRight W')] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (lambdaMul α β) (lambdaObj α β)) (lambdaMul α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (lambdaObj α β) (lambdaObj α β) (lambdaObj α β)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (lambdaObj α β) (lambdaMul α β)) (lambdaMul α β))

Associativity of the Λ multiplication (Deligne 3.8).

theorem RS.lambda_pair_hom_ext {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (α β : CategoryTheory.Functor A D) [HasLambda α β] [∀ (W : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))] {Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (lambdaObj α β) (lambdaObj α β) ⟶ Z} (h : ∀ (X Y : A), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (lambdaStage α β X) (lambdaStage α β Y)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (lambdaStage α β X) (lambdaStage α β Y)) g) : f = g

Maps out of the square of the Λ object agree once they agree on pairs of stages.

@[implicit_reducible]

noncomputable def RS.lambdaMonObj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] [HasLambda α β] [∀ (W : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))] [∀ (W : D), CategoryTheory.Limits.PreservesColimit ((CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan.comp (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))) (CategoryTheory.MonoidalCategory.tensorRight W)] [∀ (W W' : D), CategoryTheory.Limits.PreservesColimit ((CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan.comp (CategoryTheory.MonoidalCategory.tensorLeft W)) (CategoryTheory.MonoidalCategory.tensorRight W')] : CategoryTheory.MonObj (lambdaObj α β)

The Λ algebra (Deligne 3.7): the coend of a pair of lax monoidal functors from a braided rigid source is a monoid object, with the stage at the unit as unit and the descended stage-level multiplication as product.

Equations

• RS.lambdaMonObj α β = { one := RS.lambdaUnit α β, mul := RS.lambdaMul α β, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

theorem RS.lambdaMulStage_map {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory A] [CategoryTheory.BraidedCategory D] (α β : CategoryTheory.Functor A D) [α.LaxMonoidal] [β.LaxMonoidal] {α' β' : CategoryTheory.Functor A D} [α'.LaxMonoidal] [β'.LaxMonoidal] (η : α ⟶ α') (τ : β ⟶ β') [CategoryTheory.NatTrans.IsMonoidal η] [CategoryTheory.NatTrans.IsMonoidal τ] (X Y : A) : CategoryTheory.CategoryStruct.comp (lambdaMulStage α β X Y) (CategoryTheory.MonoidalCategoryStruct.tensorHom (η.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)ᘁ) (τ.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (η.app Xᘁ) (τ.app X)) (CategoryTheory.MonoidalCategoryStruct.tensorHom (η.app Yᘁ) (τ.app Y))) (lambdaMulStage α' β' X Y)

The stage-level multiplication is natural in the pair of monoidal transformations.

theorem RS.lambdaMulStage_comm {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory A] [CategoryTheory.SymmetricCategory D] (α β : CategoryTheory.Functor A D) [α.LaxBraided] [β.LaxBraided] [HasLambda α β] (X Y : A) : CategoryTheory.CategoryStruct.comp (lambdaMulStage α β X Y) (lambdaStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) = CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Xᘁ) (β.obj X)) (CategoryTheory.MonoidalCategoryStruct.tensorObj (α.obj Yᘁ) (β.obj Y))).hom (CategoryTheory.CategoryStruct.comp (lambdaMulStage α β Y X) (lambdaStage α β (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X)))

The stage-level commutativity of the Λ multiplication over a symmetric source and target with braided functors.

theorem RS.lambdaMul_comm {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory A] [CategoryTheory.SymmetricCategory D] (α β : CategoryTheory.Functor A D) [α.LaxBraided] [β.LaxBraided] [HasLambda α β] [∀ (W : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))] : CategoryTheory.CategoryStruct.comp (β_ (lambdaObj α β) (lambdaObj α β)).hom (lambdaMul α β) = lambdaMul α β

Commutativity of the Λ multiplication (Deligne 3.8).

theorem RS.lambdaIsCommMonObj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RightRigidCategory A] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory A] [CategoryTheory.SymmetricCategory D] (α β : CategoryTheory.Functor A D) [α.LaxBraided] [β.LaxBraided] [HasLambda α β] [∀ (W : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorLeft W)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan (CategoryTheory.MonoidalCategory.tensorRight (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))] [∀ (W : D), CategoryTheory.Limits.PreservesColimit ((CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan.comp (CategoryTheory.MonoidalCategory.tensorRight (lambdaObj α β))) (CategoryTheory.MonoidalCategory.tensorRight W)] [∀ (W W' : D), CategoryTheory.Limits.PreservesColimit ((CategoryTheory.Limits.multispanIndexCoend (lambdaDiagram α β)).multispan.comp (CategoryTheory.MonoidalCategory.tensorLeft W)) (CategoryTheory.MonoidalCategory.tensorRight W')] : CategoryTheory.IsCommMonObj (lambdaObj α β)

The Λ algebra is commutative over symmetric data with braided functors (Deligne 3.7–3.8 in full).