Monoidal change of rings for presheaves of modules

For presheaves of commutative rings R and S and a morphism α : R ⟶ S, restriction of scalars from presheaves of S-modules to presheaves of R-modules is lax symmetric monoidal. Its unit map is α itself, sectionwise, and its tensor map sends a pure tensor m ⊗ₜ[R.obj X] n of sections over X to the pure tensor m ⊗ₜ[S.obj X] n, balanced over S.obj X.

Combining it with precomposition, the pushforward of presheaves of modules along a functor and a morphism of presheaves of commutative rings is lax symmetric monoidal. Consequently its left adjoint, the pullback, carries a canonical oplax tensor comparison.

Main declarations

• PresheafOfModules.restrictScalarsLaxMonoidal: its lax monoidal structure;
• PresheafOfModules.restrictScalarsLaxBraided: compatibility with the symmetric braiding;
• PresheafOfModules.pushforwardLaxMonoidal: Mathlib's PresheafOfModulesOfCommRing.pushforward is lax monoidal;
• PresheafOfModules.pushforwardLaxBraided: it is moreover lax symmetric monoidal.

All structure maps and coherence laws are obtained sectionwise from Mathlib's lax monoidal restriction of scalars for ModuleCat.

noncomputable def TauCeti.PresheafOfModules.restrictScalarsUnit {C : Type v} [CategoryTheory.Category.{w, v} C] {R S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (α : R ⟶ S) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (PresheafOfModulesOfCommRing R) ⟶ (PresheafOfModulesOfCommRing.restrictScalars α).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (PresheafOfModulesOfCommRing S))

The unit map for restriction of scalars, given sectionwise by the coefficient morphism.

Equations

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

@[simp]

theorem TauCeti.PresheafOfModules.restrictScalarsUnit_app_apply {C : Type v} [CategoryTheory.Category.{w, v} C] {R S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (α : R ⟶ S) (X : Cᵒᵖ) (r : ↑(R.obj X)) : (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' (restrictScalarsUnit α) X)) r = (CategoryTheory.ConcreteCategory.hom (α.app X)) r

On sections over X, the unit map for restriction of scalars is α.app X.

noncomputable def TauCeti.PresheafOfModules.restrictScalarsTensor {C : Type v} [CategoryTheory.Category.{w, v} C] {R S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (α : R ⟶ S) (M N : PresheafOfModulesOfCommRing S) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((PresheafOfModulesOfCommRing.restrictScalars α).obj M) ((PresheafOfModulesOfCommRing.restrictScalars α).obj N) ⟶ (PresheafOfModulesOfCommRing.restrictScalars α).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)

The tensor map for restriction of scalars, given sectionwise by the canonical balanced map.

Equations

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

@[simp]

theorem TauCeti.PresheafOfModules.restrictScalarsTensor_app_tmul {C : Type v} [CategoryTheory.Category.{w, v} C] {R S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (α : R ⟶ S) (M N : PresheafOfModulesOfCommRing S) (X : Cᵒᵖ) (m : ↑(M.obj X)) (n : ↑(N.obj X)) : (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' (restrictScalarsTensor α M N) X)) (m ⊗ₜ[↑(R.obj X)] n) = m ⊗ₜ[↑(S.obj X)] n

On sections over X, the tensor map for restriction of scalars sends the pure tensor m ⊗ₜ n over R.obj X to the same pure tensor over S.obj X.

@[instance_reducible]

noncomputable instance TauCeti.PresheafOfModules.restrictScalarsLaxMonoidal {C : Type v} [CategoryTheory.Category.{w, v} C] {R S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (α : R ⟶ S) : (PresheafOfModulesOfCommRing.restrictScalars α).LaxMonoidal

Restriction of scalars for presheaves of modules is lax monoidal.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.PresheafOfModules.restrictScalarsLaxBraided {C : Type v} [CategoryTheory.Category.{w, v} C] {R S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (α : R ⟶ S) : (PresheafOfModulesOfCommRing.restrictScalars α).LaxBraided

Restriction of scalars preserves the symmetric braiding.

Equations

• TauCeti.PresheafOfModules.restrictScalarsLaxBraided α = { toLaxMonoidal := TauCeti.PresheafOfModules.restrictScalarsLaxMonoidal α, braided := ⋯ }

@[instance_reducible]

noncomputable instance TauCeti.PresheafOfModules.pushforwardLaxMonoidal {C : Type v} {D : Type v'} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Category.{w', v'} D] (F : CategoryTheory.Functor C D) {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (α : S ⟶ F.op.comp R) : (PresheafOfModulesOfCommRing.pushforward α).LaxMonoidal

Pushforward of presheaves of modules is lax monoidal.

Equations

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

@[simp]

theorem TauCeti.PresheafOfModules.pushforward_ε_app_apply {C : Type v} {D : Type v'} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Category.{w', v'} D] (F : CategoryTheory.Functor C D) {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (α : S ⟶ F.op.comp R) (X : Cᵒᵖ) (r : ↑(S.obj X)) : (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' (CategoryTheory.Functor.LaxMonoidal.ε (PresheafOfModulesOfCommRing.pushforward α)) X)) r = (CategoryTheory.ConcreteCategory.hom (α.app X)) r

On sections over X, the unit map for pushforward is α.app X.

@[simp]

theorem TauCeti.PresheafOfModules.pushforward_μ_app_tmul {C : Type v} {D : Type v'} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Category.{w', v'} D] (F : CategoryTheory.Functor C D) {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (α : S ⟶ F.op.comp R) (M N : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) (m : ↑(M.obj (Opposite.op (F.obj (Opposite.unop X))))) (n : ↑(N.obj (Opposite.op (F.obj (Opposite.unop X))))) : (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' (CategoryTheory.Functor.LaxMonoidal.μ (PresheafOfModulesOfCommRing.pushforward α) M N) X)) (m ⊗ₜ[↑(S.obj X)] n) = m ⊗ₜ[↑(R.obj (Opposite.op (F.obj (Opposite.unop X))))] n

On sections over X, the tensor map for pushforward sends the pure tensor m ⊗ₜ n over S.obj X to the same pure tensor over R.obj (op (F.obj X.unop)).

@[instance_reducible]

noncomputable instance TauCeti.PresheafOfModules.pushforwardLaxBraided {C : Type v} {D : Type v'} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Category.{w', v'} D] (F : CategoryTheory.Functor C D) {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (α : S ⟶ F.op.comp R) : (PresheafOfModulesOfCommRing.pushforward α).LaxBraided

Pushforward of presheaves of modules preserves the symmetric braiding.

Equations

• TauCeti.PresheafOfModules.pushforwardLaxBraided F α = { toLaxMonoidal := TauCeti.PresheafOfModules.pushforwardLaxMonoidal F α, braided := ⋯ }