The monoidal adjunction between the extension and the restriction of scalars

Let f : R →+* S be a morphism of commutative rings. We show that the functor extendsScalars f : ModuleCat R ⥤ ModuleCat S is monoidal, and deduce that restrictScalars f : ModuleCat S ⥤ ModuleCat R is lax monoidal.

@[simp]

theorem ModuleCat.extendsScalars_map_leftUnitor_inv_one_tmul {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (M : ModuleCat R) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom ((extendScalars f).map (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv)) (1 ⊗ₜ[R] m) = 1 ⊗ₜ[R] (1 ⊗ₜ[R] m)

@[simp]

theorem ModuleCat.extendsScalars_map_rightUnitor_inv_one_tmul {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (M : ModuleCat R) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom ((extendScalars f).map (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv)) (1 ⊗ₜ[R] m) = 1 ⊗ₜ[R] (m ⊗ₜ[R] 1)

@[implicit_reducible]

noncomputable instance ModuleCat.instMonoidalExtendScalars {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : (extendScalars f).Monoidal

Equations

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

theorem ModuleCat.extendScalars_ε {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : CategoryTheory.Functor.LaxMonoidal.ε (extendScalars f) = ofHom ↑(TensorProduct.AlgebraTensorModule.rid R S S).symm

theorem ModuleCat.extendScalars_η {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : CategoryTheory.Functor.OplaxMonoidal.η (extendScalars f) = ofHom ↑(TensorProduct.AlgebraTensorModule.rid R S S)

theorem ModuleCat.extendScalars_μ {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (M₁ M₂ : ModuleCat R) : CategoryTheory.Functor.LaxMonoidal.μ (extendScalars f) M₁ M₂ = ofHom ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R S ↑M₁ ↑M₂).symm

theorem ModuleCat.extendScalars_δ {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (M₁ M₂ : ModuleCat R) : CategoryTheory.Functor.OplaxMonoidal.δ (extendScalars f) M₁ M₂ = ofHom ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R S ↑M₁ ↑M₂)

@[simp]

theorem ModuleCat.extendScalars_δ_tmul {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (M₁ M₂ : ModuleCat R) (m₁ : ↑M₁) (m₂ : ↑M₂) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.OplaxMonoidal.δ (extendScalars f) M₁ M₂)) (1 ⊗ₜ[R] (m₁ ⊗ₜ[R] m₂)) = 1 ⊗ₜ[R] m₁ ⊗ₜ[S] (1 ⊗ₜ[R] m₂)

@[implicit_reducible]

noncomputable instance ModuleCat.instLaxMonoidalRestrictScalars {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : (restrictScalars f).LaxMonoidal

Equations

• ModuleCat.instLaxMonoidalRestrictScalars f = (ModuleCat.extendRestrictScalarsAdj f).rightAdjointLaxMonoidal

@[simp]

theorem ModuleCat.restrictScalars_η {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (r : R) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.ε (restrictScalars f))) r = f r

@[simp]

theorem ModuleCat.restrictScalars_μ_tmul {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (M₁ M₂ : ModuleCat S) (m₁ : ↑M₁) (m₂ : ↑M₂) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ (restrictScalars f) M₁ M₂)) (m₁ ⊗ₜ[R] m₂) = m₁ ⊗ₜ[S] m₂