Base change as a monoidal functor

Base change along a morphism of commutative algebras carries modules to modules, morphisms to morphisms, and the relative tensor to the relative tensor: the projection formula is the structure map, the collapse of the regular module is the unit. This file bundles the structure map as an isomorphism of modules over the new base and proves it natural in both slots.

noncomputable def RS.projFormulaMod {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 : CategoryTheory.Mod D A) : modTensorMod B (baseChangeMod φ M) (baseChangeMod φ N) ≅ baseChangeMod φ (modTensorMod A M N)

The structure map of base change, as an isomorphism of modules over the new base.

Equations

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

theorem RS.projFormula_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 (modTensorMap B (CategoryTheory.CategoryStruct.id (baseChangeMod φ M)) (baseChangeMapMod A B φ g)) (projFormula A B φ M N').hom = CategoryTheory.CategoryStruct.comp (projFormula A B φ M N).hom (modTensorMap A (CategoryTheory.CategoryStruct.id (restrictRegular φ)) (modTensorMapMod A (CategoryTheory.CategoryStruct.id M) g))

The structure map is natural in the second slot.

theorem RS.projFormula_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 (modTensorMap B (baseChangeMapMod A B φ f) (CategoryTheory.CategoryStruct.id (baseChangeMod φ N))) (projFormula A B φ M' N).hom = CategoryTheory.CategoryStruct.comp (projFormula A B φ M N).hom (modTensorMap A (CategoryTheory.CategoryStruct.id (restrictRegular φ)) (modTensorMapMod A f (CategoryTheory.CategoryStruct.id N)))

The structure map is natural in the first slot.

theorem RS.projFormula_assoc_leftCover {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 (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A (restrictRegular φ) M) (CategoryTheory.MonoidalCategoryStruct.tensorObj B N.X)) (CategoryTheory.MonoidalCategoryStruct.tensorObj B P.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (baseChangeMod φ M).X (modTensorπ A (restrictRegular φ) N)) (CategoryTheory.MonoidalCategoryStruct.tensorObj B P.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ B (baseChangeMod φ M) (baseChangeMod φ N)) (CategoryTheory.MonoidalCategoryStruct.tensorObj B P.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modTensor B (baseChangeMod φ M) (baseChangeMod φ N)) (modTensorπ A (restrictRegular φ) P)) (CategoryTheory.CategoryStruct.comp (modTensorπ B (modTensorMod B (baseChangeMod φ M) (baseChangeMod φ N)) (baseChangeMod φ P)) (CategoryTheory.CategoryStruct.comp (modTensorMap B (projFormulaMod A B φ M N).hom (CategoryTheory.CategoryStruct.id (baseChangeMod φ P))) (CategoryTheory.CategoryStruct.comp (projFormula A B φ (modTensorMod A M N) P).hom (modTensorMap A (CategoryTheory.CategoryStruct.id (restrictRegular φ)) (modTensorAssocModIso A M N P).hom))))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ B M.X B N.X) (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (modTensorπ A M N))) (CategoryTheory.MonoidalCategoryStruct.tensorObj B P.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ B (modTensor A M N) B P.X) (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj (modTensor A M N) P.X))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (modTensorAssocMid A M N P)) (modTensorπ A (restrictRegular φ) (modTensorMod A M (modTensorMod A N P)))))

The left-nested side of the associator square, evaluated on the triple cover.

theorem RS.projFormula_assoc_rightCover {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 (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A (restrictRegular φ) M) (CategoryTheory.MonoidalCategoryStruct.tensorObj B N.X)) (CategoryTheory.MonoidalCategoryStruct.tensorObj B P.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (baseChangeMod φ M).X (modTensorπ A (restrictRegular φ) N)) (CategoryTheory.MonoidalCategoryStruct.tensorObj B P.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ B (baseChangeMod φ M) (baseChangeMod φ N)) (CategoryTheory.MonoidalCategoryStruct.tensorObj B P.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modTensor B (baseChangeMod φ M) (baseChangeMod φ N)) (modTensorπ A (restrictRegular φ) P)) (CategoryTheory.CategoryStruct.comp (modTensorπ B (modTensorMod B (baseChangeMod φ M) (baseChangeMod φ N)) (baseChangeMod φ P)) (CategoryTheory.CategoryStruct.comp (modTensorAssocHom B (baseChangeMod φ M) (baseChangeMod φ N) (baseChangeMod φ P)) (CategoryTheory.CategoryStruct.comp (modTensorMap B (CategoryTheory.CategoryStruct.id (baseChangeMod φ M)) (projFormulaMod A B φ N P).hom) (projFormula A B φ M (modTensorMod A N P)).hom)))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj B M.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj B N.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj B P.X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj B M.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ B N.X B P.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj N.X P.X)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (modTensorπ A N P))))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ B M.X B (modTensor A N P)) (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X (modTensor A N P)))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (modTensorπ A M (modTensorMod A N P))) (modTensorπ A (restrictRegular φ) (modTensorMod A M (modTensorMod A N P))))))

The right-nested side of the associator square, evaluated on the triple cover.

theorem RS.projFormula_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 (modTensorMap B (projFormulaMod A B φ M N).hom (CategoryTheory.CategoryStruct.id (baseChangeMod φ P))) (CategoryTheory.CategoryStruct.comp (projFormula A B φ (modTensorMod A M N) P).hom (modTensorMap A (CategoryTheory.CategoryStruct.id (restrictRegular φ)) (modTensorAssocModIso A M N P).hom)) = CategoryTheory.CategoryStruct.comp (modTensorAssocHom B (baseChangeMod φ M) (baseChangeMod φ N) (baseChangeMod φ P)) (CategoryTheory.CategoryStruct.comp (modTensorMap B (CategoryTheory.CategoryStruct.id (baseChangeMod φ M)) (projFormulaMod A B φ N P).hom) (projFormula A B φ M (modTensorMod A N P)).hom)

The associator coherence of the projection formula: base change carries the module associator to the module associator through the structure map.