The base change of a duality datum

The pairing and copairing of a duality datum base-change to a duality datum over the new base: the projection formula, the functorial maps and the unit collapses are all linear, so the composites defining the base-changed pairing and copairing are linear too.

theorem RS.baseChangePair_linear {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 (modTensorAct B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangePair A B φ d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (baseChangePair A B φ d)) CategoryTheory.MonObj.mul

The base-changed pairing is linear.

theorem RS.baseChangeCopair_linear {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.MonObj.mul (baseChangeCopair A B φ d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (baseChangeCopair A B φ d)) (modTensorAct B (baseChangeMod φ M) (baseChangeMod φ M'))

The base-changed copairing is linear.

noncomputable def RS.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 B (baseChangeMod φ M) (baseChangeMod φ M')

The base change of a duality datum.

Equations

• RS.baseChangeDatum A B φ d = { pair := RS.baseChangePair A B φ d, copair := RS.baseChangeCopair A B φ d, pair_linear := ⋯, copair_linear := ⋯ }

noncomputable def RS.baseChangeUnitIso {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] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] : baseChangeMod φ (regularMod A) ≅ regularMod B

The unit of the base-change structure: the base change of the regular module is the regular module over the new base.

Equations

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