Transport of the zigzag laws along base change

Base change is a strong monoidal functor on modules, and the zigzag laws of a duality datum are an identity between words in the monoidal structure. This file transports the identity: the base-changed insertion and contraction are the images of the insertion and contraction, conjugated by the structure map, so their composite is the image of an identity.

theorem RS.modTensorMapMod_comp {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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' M'' N N' N'' : CategoryTheory.Mod D A} (f : M ⟶ M') (f' : M' ⟶ M'') (g : N ⟶ N') (g' : N' ⟶ N'') : CategoryTheory.CategoryStruct.comp (modTensorMapMod A f g) (modTensorMapMod A f' g') = modTensorMapMod A (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g')

Functoriality of the relative tensor of morphisms.

theorem RS.projFormulaMod_unitRight {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 : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (projFormulaMod A B φ M (regularMod A)).hom (baseChangeMapMod A B φ (modTensorUnitRightMod A M).hom) = CategoryTheory.CategoryStruct.comp (modTensorMapMod B (CategoryTheory.CategoryStruct.id (baseChangeMod φ M)) (baseChangeUnitIso A B φ).hom) (modTensorUnitRightMod B (baseChangeMod φ M)).hom

The right unit coherence, as an identity of module maps.

theorem RS.projFormulaMod_unitLeft {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 φ] (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (projFormulaMod A B φ (regularMod A) N).hom (baseChangeMapMod A B φ (modTensorUnitLeftMod A N).hom) = CategoryTheory.CategoryStruct.comp (modTensorMapMod B (baseChangeUnitIso A B φ).hom (CategoryTheory.CategoryStruct.id (baseChangeMod φ N))) (modTensorUnitLeftMod B (baseChangeMod φ N)).hom

The left unit coherence, as an identity of module maps.

theorem RS.projFormulaMod_natural_left {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} (f : M ⟶ M') (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorMapMod B (baseChangeMapMod A B φ f) (CategoryTheory.CategoryStruct.id (baseChangeMod φ N))) (projFormulaMod A B φ M' N).hom = CategoryTheory.CategoryStruct.comp (projFormulaMod A B φ M N).hom (baseChangeMapMod A B φ (modTensorMapMod A f (CategoryTheory.CategoryStruct.id N)))

Naturality in the first slot, as an identity of module maps.

theorem RS.projFormulaMod_natural_right {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 : CategoryTheory.Mod D A) {N N' : CategoryTheory.Mod D A} (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (modTensorMapMod B (CategoryTheory.CategoryStruct.id (baseChangeMod φ M)) (baseChangeMapMod A B φ g)) (projFormulaMod A B φ M N').hom = CategoryTheory.CategoryStruct.comp (projFormulaMod A B φ M N).hom (baseChangeMapMod A B φ (modTensorMapMod A (CategoryTheory.CategoryStruct.id M) g))

Naturality in the second slot, as an identity of module maps.

theorem RS.projFormulaMod_assoc {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 N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorMapMod B (projFormulaMod A B φ M N).hom (CategoryTheory.CategoryStruct.id (baseChangeMod φ P))) (CategoryTheory.CategoryStruct.comp (projFormulaMod A B φ (modTensorMod A M N) P).hom (baseChangeMapMod A B φ (modTensorAssocModIso A M N P).hom)) = CategoryTheory.CategoryStruct.comp (modTensorAssocModIso B (baseChangeMod φ M) (baseChangeMod φ N) (baseChangeMod φ P)).hom (CategoryTheory.CategoryStruct.comp (modTensorMapMod B (CategoryTheory.CategoryStruct.id (baseChangeMod φ M)) (projFormulaMod A B φ N P).hom) (projFormulaMod A B φ M (modTensorMod A N P)).hom)

The associator coherence, as an identity of module maps.

theorem RS.pairMod_baseChangeDatum {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') : ModDualityDatum.pairMod B (baseChangeDatum A B φ d) = CategoryTheory.CategoryStruct.comp (projFormulaMod A B φ M' M).hom (CategoryTheory.CategoryStruct.comp (baseChangeMapMod A B φ (ModDualityDatum.pairMod A d)) (baseChangeUnitIso A B φ).hom)

The base-changed pairing, as the image of the pairing conjugated by the structure map and the unit.

theorem RS.copairMod_baseChangeDatum {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') : ModDualityDatum.copairMod B (baseChangeDatum A B φ d) = CategoryTheory.CategoryStruct.comp (baseChangeUnitIso A B φ).inv (CategoryTheory.CategoryStruct.comp (baseChangeMapMod A B φ (ModDualityDatum.copairMod A d)) (projFormulaMod A B φ M M').inv)

The base-changed copairing, as the image of the copairing conjugated by the unit and the structure map.

theorem RS.baseChangeMapMod_comp {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)] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {X Y Z : CategoryTheory.Mod D A} (f : X ⟶ Y) (g : Y ⟶ Z) : baseChangeMapMod A B φ (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (baseChangeMapMod A B φ f) (baseChangeMapMod A B φ g)

Base change on morphisms preserves composition.

theorem RS.baseChangeMapMod_id {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)] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (X : CategoryTheory.Mod D A) : baseChangeMapMod A B φ (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (baseChangeMod φ X)

Base change on morphisms preserves identities.

theorem RS.modTensorMapMod_compL {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)] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] {X Y Z W : CategoryTheory.Mod D B} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorMapMod B f (CategoryTheory.CategoryStruct.id W)) (modTensorMapMod B g (CategoryTheory.CategoryStruct.id W)) = modTensorMapMod B (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W)

Composing two relative tensors of morphisms with identity second slots.

theorem RS.modTensorMapMod_compR {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)] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] {W X Y Z : CategoryTheory.Mod D B} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorMapMod B (CategoryTheory.CategoryStruct.id W) f) (modTensorMapMod B (CategoryTheory.CategoryStruct.id W) g) = modTensorMapMod B (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.comp f g)

Composing two relative tensors of morphisms with identity first slots.

theorem RS.modTensorMapMod_id {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)] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (X W : CategoryTheory.Mod D B) : modTensorMapMod B (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id W) = CategoryTheory.CategoryStruct.id (modTensorMod B X W)

The relative tensor with two identities is the identity.

theorem RS.baseChange_sandwichIns {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 (sandwichIns B (baseChangeDatum A B φ d)) (CategoryTheory.CategoryStruct.comp (modTensorMapMod B (projFormulaMod A B φ M M').hom (CategoryTheory.CategoryStruct.id (baseChangeMod φ M))) (projFormulaMod A B φ (modTensorMod A M M') M).hom) = baseChangeMapMod A B φ (sandwichIns A d)

The insertion transports: the base-changed sandwich insertion, conjugated by the structure map, is the image of the insertion.

theorem RS.baseChange_sandwichCon {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.CategoryStruct.comp (modTensorMapMod B (projFormulaMod A B φ M M').hom (CategoryTheory.CategoryStruct.id (baseChangeMod φ M))) (projFormulaMod A B φ (modTensorMod A M M') M).hom) (baseChangeMapMod A B φ (sandwichCon A d)) = sandwichCon B (baseChangeDatum A B φ d)

The contraction transports: the conjugated image of the sandwich contraction is the base-changed contraction.

theorem RS.baseChange_sandwich_zig {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} (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) : CategoryTheory.CategoryStruct.comp (sandwichIns B (baseChangeDatum A B φ d)) (sandwichCon B (baseChangeDatum A B φ d)) = CategoryTheory.CategoryStruct.id (baseChangeMod φ M)

The zig triangle transports: the base-changed datum satisfies the sandwich retract identity.

theorem RS.baseChange_carrier_zig {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} (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (baseChangeMod φ M).X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (baseChangeDatum A B φ d).copair) (baseChangeMod φ M).X) (zigContract B (baseChangeDatum A B φ d).pair ⋯)) = CategoryTheory.CategoryStruct.id (baseChangeMod φ M).X

The carrier zig law of the base-changed datum.

theorem RS.baseChange_sandwichInsR {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 (sandwichInsR B (baseChangeDatum A B φ d)) (CategoryTheory.CategoryStruct.comp (modTensorMapMod B (CategoryTheory.CategoryStruct.id (baseChangeMod φ M')) (projFormulaMod A B φ M M').hom) (projFormulaMod A B φ M' (modTensorMod A M M')).hom) = baseChangeMapMod A B φ (sandwichInsR A d)

The dual insertion transports.

theorem RS.baseChange_sandwichConR {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.CategoryStruct.comp (modTensorMapMod B (CategoryTheory.CategoryStruct.id (baseChangeMod φ M')) (projFormulaMod A B φ M M').hom) (projFormulaMod A B φ M' (modTensorMod A M M')).hom) (baseChangeMapMod A B φ (sandwichConR A d)) = sandwichConR B (baseChangeDatum A B φ d)

The dual contraction transports.

theorem RS.baseChange_sandwich_zag {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} (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) : CategoryTheory.CategoryStruct.comp (sandwichInsR B (baseChangeDatum A B φ d)) (sandwichConR B (baseChangeDatum A B φ d)) = CategoryTheory.CategoryStruct.id (baseChangeMod φ M')

The zag triangle transports.

theorem RS.baseChange_carrier_zag {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} (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) : 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 (baseChangeDatum A B φ d).copair)) (zagContract B (baseChangeDatum A B φ d).pair ⋯)) = CategoryTheory.CategoryStruct.id (baseChangeMod φ M').X

The carrier zag law of the base-changed datum.

theorem RS.baseChange_modZigzagDatum {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} (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) : ModZigzagDatum B (baseChangeDatum A B φ d)

Base change preserves the zigzag laws.

theorem RS.baseChangeZigzag (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)] : BaseChangeZigzagStatement

Base change preserves the zigzag laws: the statement of record, discharged.