The pseudofunctors which send a commutative ring to its category of modules #

In this file, we construct the pseudofunctors CommRingCat.moduleCatRestrictScalarsPseudofunctor and RingCat.moduleCatRestrictScalarsPseudofunctor which sends a (commutative) ring to its category of modules: the contravariant functoriality is given by the restriction of scalars functors.

We also define a pseudofunctor CommRingCat.moduleCatExtendScalarsPseudofunctor: the covariant functoriality is given by the extension of scalars functors.

source

noncomputable def CommRingCat.moduleCatRestrictScalarsPseudofunctor :

CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete CommRingCat ᵒᵖ) CategoryTheory.Cat

The pseudofunctor from LocallyDiscrete CommRingCatᵒᵖ to Cat which sends a commutative ring R to its category of modules. The functoriality is given by the restriction of scalars.

Equations

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

Instances For

source

@[simp]

theorem CommRingCat.moduleCatRestrictScalarsPseudofunctor_map {X✝ Y✝ : CategoryTheory.LocallyDiscrete CommRingCat ᵒᵖ} (f : X✝ ⟶ Y✝) :

moduleCatRestrictScalarsPseudofunctor.map f = ModuleCat.restrictScalars (Hom.hom f.as.unop)

source

@[simp]

theorem CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj (b : CategoryTheory.LocallyDiscrete CommRingCat ᵒᵖ) :

moduleCatRestrictScalarsPseudofunctor.obj b = CategoryTheory.Cat.of (ModuleCat ↑(Opposite.unop b.as))

source

@[simp]

theorem CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete CommRingCat ᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) :

moduleCatRestrictScalarsPseudofunctor.mapComp x✝ x✝¹ = ModuleCat.restrictScalarsComp (Hom.hom x✝¹.as.unop) (Hom.hom x✝.as.unop)

source

@[simp]

theorem CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId (x✝ : CategoryTheory.LocallyDiscrete CommRingCat ᵒᵖ) :

moduleCatRestrictScalarsPseudofunctor.mapId x✝ = ModuleCat.restrictScalarsId ↑(Opposite.unop x✝.as)

source

noncomputable def RingCat.moduleCatRestrictScalarsPseudofunctor :

CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete RingCat ᵒᵖ) CategoryTheory.Cat

The pseudofunctor from LocallyDiscrete RingCatᵒᵖ to Cat which sends a ring R to its category of modules. The functoriality is given by the restriction of scalars.

Equations

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

Instances For

source

@[simp]

theorem RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete RingCat ᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) :

moduleCatRestrictScalarsPseudofunctor.mapComp x✝ x✝¹ = ModuleCat.restrictScalarsComp (Hom.hom x✝¹.as.unop) (Hom.hom x✝.as.unop)

source

@[simp]

theorem RingCat.moduleCatRestrictScalarsPseudofunctor_map {X✝ Y✝ : CategoryTheory.LocallyDiscrete RingCat ᵒᵖ} (f : X✝ ⟶ Y✝) :

moduleCatRestrictScalarsPseudofunctor.map f = ModuleCat.restrictScalars (Hom.hom f.as.unop)

source

@[simp]

theorem RingCat.moduleCatRestrictScalarsPseudofunctor_mapId (x✝ : CategoryTheory.LocallyDiscrete RingCat ᵒᵖ) :

moduleCatRestrictScalarsPseudofunctor.mapId x✝ = ModuleCat.restrictScalarsId ↑(Opposite.unop x✝.as)

source

@[simp]

theorem RingCat.moduleCatRestrictScalarsPseudofunctor_obj (b : CategoryTheory.LocallyDiscrete RingCat ᵒᵖ) :

moduleCatRestrictScalarsPseudofunctor.obj b = CategoryTheory.Cat.of (ModuleCat ↑(Opposite.unop b.as))

source

noncomputable def CommRingCat.moduleCatExtendScalarsPseudofunctor :

CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete CommRingCat) CategoryTheory.Cat

The pseudofunctor from LocallyDiscrete CommRingCat to Cat which sends a commutative ring R to its category of modules. The functoriality is given by the extension of scalars.

Equations