forgetToPresheafModuleCatMap — Mathlib

Lean4
/-- Implementation of the functor `PresheafOfModules R ⥤ Cᵒᵖ ⥤ ModuleCat (R.obj X)`
when `X` is initial.

The functor is implemented as, on object level `M ↦ (c ↦ M(c))` where the `R(X)`-module structure
on `M(c)` is given by restriction of scalars along the unique morphism `R(c) ⟶ R(X)`; and on
morphism level `(f : M ⟶ N) ↦ (c ↦ f(c))`.
-/
noncomputable def forgetToPresheafModuleCatMap (X : Cᵒᵖ) (hX : Limits.IsInitial X) {M N : PresheafOfModules.{v} R}
    (f : M ⟶ N) : forgetToPresheafModuleCatObj X hX M ⟶ forgetToPresheafModuleCatObj X hX N
    where
  app
    Y :=
    ModuleCat.ofHom (X := (forgetToPresheafModuleCatObj X hX M).obj Y) (Y :=
      (forgetToPresheafModuleCatObj X hX N).obj Y)
      { toFun := f.app Y
        map_add' := by simp
        map_smul' := fun r ↦ (f.app Y).hom.map_smul (R.map (hX.to Y) _) }
  naturality Y Z
    g := by
    ext x
    exact naturality_apply f g x
Похожие утверждения