The base-changed pairing on its cover

The pairing of a base-changed duality datum, evaluated on the double cover of the relative tensor over the new base: it multiplies the two base factors and applies the pairing through the base morphism. This is the working form for the adjointness of the split idempotents.

theorem RS.baseChangePair_cover {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A (restrictRegular φ) M') (CategoryTheory.MonoidalCategoryStruct.tensorObj B M.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (baseChangeMod φ M').X (modTensorπ A (restrictRegular φ) M)) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ B M'.X B M.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj M'.X M.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) (CategoryTheory.CategoryStruct.comp d.pair φ))) CategoryTheory.MonObj.mul))

The base-changed pairing on the cover: it multiplies the two base factors and applies the pairing through the base morphism.

theorem RS.tensorμ_braid {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X Y Z W : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X Y Z W) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z (CategoryTheory.MonoidalCategoryStruct.tensorObj Y W)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Z (CategoryTheory.MonoidalCategoryStruct.tensorObj Y W)).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (β_ Z W).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) W Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator X Y W).hom Z) (CategoryTheory.MonoidalCategoryStruct.associator X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y W) Z).hom))

The interchange followed by braiding the base factor to the right is a reassociation of the braiding.

theorem RS.mulSwap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] {U V : D} (f : U ⟶ B) (g : V ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (β_ U V).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f) CategoryTheory.MonObj.mul)

Multiplying two scalars is symmetric.

theorem RS.mulLeftAssoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : D) [CategoryTheory.MonObj B] {U V : D} (f : U ⟶ B) (g : V ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B f) CategoryTheory.MonObj.mul) g) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B U V).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) CategoryTheory.MonObj.mul)) CategoryTheory.MonObj.mul)

Reassociating a product with a base factor on the left.

theorem RS.tensorμ_shuffle {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (W X Y : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj W Y) (β_ X Y).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ W Y Y X) (CategoryTheory.MonoidalCategoryStruct.associator W Y (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X)).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator W Y (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Y).inv (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X) Y).hom))

The interchange, followed by reassociation, is the braiding of the outer block.

theorem RS.mulSlide {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] {U V : D} (f : U ⟶ B) (g : V ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f B) CategoryTheory.MonObj.mul) g) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U B V).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (β_ B V).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g B) CategoryTheory.MonObj.mul)) CategoryTheory.MonObj.mul))

Sliding a base factor across a product of two scalars.

theorem RS.actRight_ins {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) {M : CategoryTheory.Mod D A} (v : M.X ⟶ B) (hv : CategoryTheory.CategoryStruct.comp (actLeft A M.X) v = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A v) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ B) CategoryTheory.MonObj.mul)) : CategoryTheory.CategoryStruct.comp (actRight A M.X) v = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight v A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul)

A base-linear insertion intertwines the braided right action with multiplication through the base morphism.

theorem RS.splitCoevalCoreDual_cover {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {M M' : CategoryTheory.Mod D A} (v : M.X ⟶ B) (d : ModDualityDatum A M M') (hv : CategoryTheory.CategoryStruct.comp (actLeft A M.X) v = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A v) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ B) CategoryTheory.MonObj.mul)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (splitCoevalCoreDual A B φ v hv) (CategoryTheory.MonoidalCategoryStruct.tensorObj B M.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (baseChangeMod φ M').X (modTensorπ A (restrictRegular φ) M)) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modTensor A M M') (β_ B M.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (modTensor A M M') M.X B).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (zigContract A d.pair ⋯) v) B) CategoryTheory.MonObj.mul))

The dual coevaluation core against the base-changed pairing: the pairing sees the inserted primal factor through the zig contraction.

theorem RS.splitCoevalDual_point_pair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {M M' : CategoryTheory.Mod D A} (v : M.X ⟶ B) (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) (hv : CategoryTheory.CategoryStruct.comp (actLeft A M.X) v = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A v) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ B) CategoryTheory.MonObj.mul)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (baseChangeMod φ M).X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp d.copair (splitCoevalCoreDual A B φ v hv))) (baseChangeMod φ M).X) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair)) = splitEval A B φ v hv

The dual coevaluation point against the base-changed pairing: pairing the inserted point with a vector evaluates the insertion on it.

theorem RS.baseChangePair_linear_outer {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (baseChangeAct φ M') (baseChangeMod φ M).X) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B (baseChangeMod φ M').X (baseChangeMod φ M).X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair)) CategoryTheory.MonObj.mul)

The base-changed pairing is linear over the new base in its outer variable.

theorem RS.splitCoevalDual_pair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {M M' : CategoryTheory.Mod D A} (v : M.X ⟶ B) (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) (hv : CategoryTheory.CategoryStruct.comp (actLeft A M.X) v = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A v) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ B) CategoryTheory.MonObj.mul)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (splitCoevalDual A B φ v d hv) (baseChangeMod φ M).X) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitEval A B φ v hv)) CategoryTheory.MonObj.mul

The dual coevaluation against the base-changed pairing: pairing the dual coevaluation with a vector evaluates the insertion on it.

theorem RS.mulShuffle {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (X Y : D) (w : Y ⟶ B) (p : CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj B Y) (CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight w X))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ B Y B X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B p) CategoryTheory.MonObj.mul))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B Y (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom p w) CategoryTheory.MonObj.mul))) CategoryTheory.MonObj.mul)

The shuffle identity behind the primal cover.

theorem RS.splitCoevalCore_cover {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {M M' : CategoryTheory.Mod D A} (w : M'.X ⟶ B) (d : ModDualityDatum A M M') (hw : CategoryTheory.CategoryStruct.comp (actLeft A M'.X) w = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ B) CategoryTheory.MonObj.mul)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj B M'.X) (splitCoevalCore A B φ w hw)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A (restrictRegular φ) M') (baseChangeMod φ M).X) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B M'.X (modTensor A M M')).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (zagContract A d.pair ⋯) w)) CategoryTheory.MonObj.mul)

The coevaluation core against the base-changed pairing: the pairing sees the inserted dual factor through the zag contraction.

theorem RS.splitCoeval_point_pair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {M M' : CategoryTheory.Mod D A} (w : M'.X ⟶ B) (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) (hw : CategoryTheory.CategoryStruct.comp (actLeft A M'.X) w = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ B) CategoryTheory.MonObj.mul)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (baseChangeMod φ M').X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (baseChangeMod φ M').X (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp d.copair (splitCoevalCore A B φ w hw)))) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair)) = splitEval A B φ w hw

The coevaluation point against the base-changed pairing.

theorem RS.baseChangePair_linear_inner {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (baseChangeMod φ M').X (baseChangeAct φ M)) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (baseChangeMod φ M').X B (baseChangeMod φ M).X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ (baseChangeMod φ M').X B).hom (baseChangeMod φ M).X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B (baseChangeMod φ M').X (baseChangeMod φ M).X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair)) CategoryTheory.MonObj.mul)))

The base-changed pairing is linear over the new base in its inner variable.

theorem RS.splitCoeval_pair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {M M' : CategoryTheory.Mod D A} (w : M'.X ⟶ B) (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) (hw : CategoryTheory.CategoryStruct.comp (actLeft A M'.X) w = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ B) CategoryTheory.MonObj.mul)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (baseChangeMod φ M').X (splitCoeval A B φ w d hw)) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (splitEval A B φ w hw) B) CategoryTheory.MonObj.mul

The coevaluation against the base-changed pairing.