moduleCatExtendScalarsPseudofunctor

Lean4

/-- 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. -/
@[simps! obj map mapId mapComp]
noncomputable def moduleCatExtendScalarsPseudofunctor : Pseudofunctor (LocallyDiscrete CommRingCat.{u}) Cat :=
  LocallyDiscrete.mkPseudofunctor (fun R ↦ Cat.of (ModuleCat.{u} R)) (fun f ↦ extendScalars f.hom)
    (fun R ↦ extendScalarsId R) (fun f g ↦ extendScalarsComp f.hom g.hom) (fun _ _ _ ↦ extendScalars_assoc' _ _ _)
    (fun _ ↦ extendScalars_id_comp _) (fun _ ↦ extendScalars_comp_id _)

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