moduleCatRestrictScalarsPseudofunctor

Mathlib.Algebra.Category.ModuleCat.Pseudofunctor

URI: https://scilib.ai/kg/mathlib#RingCat.moduleCatRestrictScalarsPseudofunctor

Lean4

/-- 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. -/
@[simps! obj map mapId mapComp]
noncomputable def moduleCatRestrictScalarsPseudofunctor : Pseudofunctor (LocallyDiscrete RingCat.{u}ᵒᵖ) Cat :=
  LocallyDiscrete.mkPseudofunctor (fun R ↦ Cat.of (ModuleCat.{v} R.unop)) (fun f ↦ restrictScalars f.unop.hom)
    (fun R ↦ restrictScalarsId R.unop) (fun f g ↦ restrictScalarsComp g.unop.hom f.unop.hom)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru