Base change and the tensor product of modules

The change-of-rings collapse: over a base morphism, the relative tensor of a module over the new base with an induced module collapses to the relative tensor over the old base of the restricted module. Together with the associativity of the relative tensor this yields the projection formula: base change commutes with the tensor product of modules.

noncomputable def RS.restrictMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) : CategoryTheory.Mod D A

Scalar restriction of a module along the base morphism.

Equations

• RS.restrictMod A B φ P = (CategoryTheory.Mod.comap φ).obj P

@[simp]

theorem RS.restrictMod_X {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) : (restrictMod A B φ P).X = P.X

theorem RS.actRight_restrictMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) : actRight A (restrictMod A B φ P).X = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X φ) (actRight B P.X)

The restricted right action acts through the base morphism.

noncomputable def RS.restrictπ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj P.X N.X ⟶ modTensor A (restrictMod A B φ P) N

The projection of the restricted-module tensor, retyped at the carrier of the unrestricted module. All statements of this development use this spelling, so that goals remain type-correct at the instances transparency level.

Equations

• RS.restrictπ A B φ P N = RS.modTensorπ A (RS.restrictMod A B φ P) N

theorem RS.restrictπ_cond {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X φ) (actRight B P.X)) N.X) (restrictπ A B φ P N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X A N.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (actLeft A N.X)) (restrictπ A B φ P N))

The balance of the restricted-module tensor, in the retyped spelling: sliding the base through the base morphism on the module side is acting on the second factor.

noncomputable def RS.collapseCover {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj P.X (CategoryTheory.MonoidalCategoryStruct.tensorObj B N.X) ⟶ modTensor A (restrictMod A B φ P) N

The cover of the collapse: act the middle base into the module and project.

Equations

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

theorem RS.collapseCover_cond {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (modTensorLegM A (restrictRegular φ) N)) (collapseCover A B φ P N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (modTensorLegN A (restrictRegular φ) N)) (collapseCover A B φ P N)

The cover of the collapse coequalizes the whiskered balance of the induced module: the base slides onto the module through the associativity of the right action and the balance of the target.

noncomputable def RS.collapseMid {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj P.X (baseChange φ N) ⟶ modTensor A (restrictMod A B φ P) N

The half-descended collapse, on the induced module.

Equations

• RS.collapseMid A B φ P N = RS.modTensorWhiskerDesc A (RS.restrictRegular φ) N P.X (RS.collapseCover A B φ P N) ⋯

@[simp]

theorem RS.whiskerLeft_collapseMid {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (modTensorπ A (restrictRegular φ) N)) (collapseMid A B φ P N) = collapseCover A B φ P N

Defining equation of the half-descended collapse.

theorem RS.whiskerLeft_collapseMid_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)] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) {Z : D} (h : modTensor A (restrictMod A B φ P) N ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (modTensorπ A (restrictRegular φ) N)) (collapseMid A B φ P N)) h = CategoryTheory.CategoryStruct.comp (collapseCover A B φ P N) h

Defining equation of the half-descended collapse.

theorem RS.collapseMid_cond {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorLegM B P (baseChangeMod φ N)) (collapseMid A B φ P N) = CategoryTheory.CategoryStruct.comp (modTensorLegN B P (baseChangeMod φ N)) (collapseMid A B φ P N)

The half-descended collapse coequalizes the outer balance: sliding the base between the module and the induced factor is absorbed by the associativity of the right action.

noncomputable def RS.collapseHom {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : modTensor B P (baseChangeMod φ N) ⟶ modTensor A (restrictMod A B φ P) N

The collapse: the relative tensor over the new base with an induced module collapses onto the relative tensor over the old base of the restricted module.

Equations

• RS.collapseHom A B φ P N = RS.modTensorDesc B P (RS.baseChangeMod φ N) (RS.collapseMid A B φ P N) ⋯

@[simp]

theorem RS.modTensorπ_collapseHom {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorπ B P (baseChangeMod φ N)) (collapseHom A B φ P N) = collapseMid A B φ P N

Defining equation of the collapse.

@[simp]

theorem RS.modTensorπ_collapseHom_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)] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) {Z : D} (h : modTensor A (restrictMod A B φ P) N ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ B P (baseChangeMod φ N)) (CategoryTheory.CategoryStruct.comp (collapseHom A B φ P N) h) = CategoryTheory.CategoryStruct.comp (collapseMid A B φ P N) h

Defining equation of the collapse.

noncomputable def RS.unitSlot {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (N : CategoryTheory.Mod D A) : N.X ⟶ baseChange φ N

The unit insertion into the induced module.

Equations

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

theorem RS.actLeft_unitSlot {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (actLeft A N.X) (unitSlot A B φ N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ N.X) (modTensorπ A (restrictRegular φ) N)

Acting before the unit insertion is acting through the base morphism after it: the balance of the induced module at the unit.

theorem RS.whiskerLeft_unitSlot_baseChangeAct {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 φ] (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (unitSlot A B φ N)) (baseChangeAct φ N) = modTensorπ A (restrictRegular φ) N

Acting on the unit insertion is the projection: the inserted unit is absorbed by the action.

noncomputable def RS.bcπ {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj P.X (baseChange φ N) ⟶ modTensor B P (baseChangeMod φ N)

The projection of the new-base tensor, retyped at the induced-module carrier.

Equations

• RS.bcπ A B φ P N = RS.modTensorπ B P (RS.baseChangeMod φ N)

theorem RS.bcπ_cond {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actRight B P.X) (baseChange φ N)) (bcπ A B φ P N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X B (baseChange φ N)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (baseChangeAct φ N)) (bcπ A B φ P N))

The balance of the new-base tensor, in the retyped spelling.

noncomputable def RS.collapseInvCover {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj P.X N.X ⟶ modTensor B P (baseChangeMod φ N)

The cover of the inverse collapse: insert the unit of the new base and project.

Equations

• RS.collapseInvCover A B φ P N = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (RS.unitSlot A B φ N)) (RS.bcπ A B φ P N)

theorem RS.collapseInvCover_cond {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorLegM A (restrictMod A B φ P) N) (collapseInvCover A B φ P N) = CategoryTheory.CategoryStruct.comp (modTensorLegN A (restrictMod A B φ P) N) (collapseInvCover A B φ P N)

The cover of the inverse collapse coequalizes the balance of the restricted-module tensor: the old base enters the induced factor through the unit insertion.

noncomputable def RS.collapseInv {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : modTensor A (restrictMod A B φ P) N ⟶ modTensor B P (baseChangeMod φ N)

The inverse collapse: descend the unit insertion.

Equations

• RS.collapseInv A B φ P N = RS.modTensorDesc A (RS.restrictMod A B φ P) N (RS.collapseInvCover A B φ P N) ⋯

@[simp]

theorem RS.restrictπ_collapseInv {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (restrictπ A B φ P N) (collapseInv A B φ P N) = collapseInvCover A B φ P N

Defining equation of the inverse collapse.

@[simp]

theorem RS.restrictπ_collapseInv_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)] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) {Z : D} (h : modTensor B P (baseChangeMod φ N) ⟶ Z) : CategoryTheory.CategoryStruct.comp (restrictπ A B φ P N) (CategoryTheory.CategoryStruct.comp (collapseInv A B φ P N) h) = CategoryTheory.CategoryStruct.comp (collapseInvCover A B φ P N) h

Defining equation of the inverse collapse.

theorem RS.whiskerLeft_unitSlot_collapseMid {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (unitSlot A B φ N)) (collapseMid A B φ P N) = restrictπ A B φ P N

The inserted unit is absorbed by the half-descended collapse.

@[simp]

theorem RS.collapseInv_collapseHom {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (collapseInv A B φ P N) (collapseHom A B φ P N) = CategoryTheory.CategoryStruct.id (modTensor A (restrictMod A B φ P) N)

The collapse retracts the inverse collapse.

@[simp]

theorem RS.collapseInv_collapseHom_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)] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) {Z : D} (h : modTensor A (restrictMod A B φ P) N ⟶ Z) : CategoryTheory.CategoryStruct.comp (collapseInv A B φ P N) (CategoryTheory.CategoryStruct.comp (collapseHom A B φ P N) h) = h

The collapse retracts the inverse collapse.

@[simp]

theorem RS.collapseHom_collapseInv {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (collapseHom A B φ P N) (collapseInv A B φ P N) = CategoryTheory.CategoryStruct.id (modTensor B P (baseChangeMod φ N))

The inverse collapse retracts the collapse.

@[simp]

theorem RS.collapseHom_collapseInv_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)] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) {Z : D} (h : modTensor B P (baseChangeMod φ N) ⟶ Z) : CategoryTheory.CategoryStruct.comp (collapseHom A B φ P N) (CategoryTheory.CategoryStruct.comp (collapseInv A B φ P N) h) = h

The inverse collapse retracts the collapse.

noncomputable def RS.collapseIso {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 φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : modTensor B P (baseChangeMod φ N) ≅ modTensor A (restrictMod A B φ P) N

The change-of-rings collapse, packaged.

Equations

• RS.collapseIso A B φ P N = { hom := RS.collapseHom A B φ P N, inv := RS.collapseInv A B φ P N, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem RS.actLeft_restrict_baseChange {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 φ] (M : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ (baseChange φ M)) (baseChangeAct φ M) = modTensorAct A (restrictRegular φ) M

The restricted action of a base change is the descended module action on the relative tensor.

theorem RS.restrictMod_baseChange_eq {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 φ] (M : CategoryTheory.Mod D A) : restrictMod A B φ (baseChangeMod φ M) = modTensorMod A (restrictRegular φ) M

The restricted base change is the module tensor with the restricted regular module.

noncomputable def RS.projFormula {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) : modTensor B (baseChangeMod φ M) (baseChangeMod φ N) ≅ baseChange φ (modTensorMod A M N)

The projection formula: the relative tensor over the new base of two base changes is the base change of the relative tensor.

Equations

• RS.projFormula A B φ M N = RS.collapseIso A B φ (RS.baseChangeMod φ M) N ≪≫ CategoryTheory.eqToIso ⋯ ≪≫ RS.modTensorAssocIso A (RS.restrictRegular φ) M N

noncomputable def RS.baseChangePair {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') : modTensor B (baseChangeMod φ M') (baseChangeMod φ M) ⟶ B

The base change of the pairing: collapse, apply the pairing under the base, and collapse the regular module.

Equations

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

noncomputable def RS.baseChangeCopair {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') : B ⟶ modTensor B (baseChangeMod φ M) (baseChangeMod φ M')

The base change of the copairing.

Equations

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