forgetToPresheafModuleCatObjMap — Mathlib

Lean4

/-- Auxiliary definition for `forgetToPresheafModuleCatObj`. -/
noncomputable def forgetToPresheafModuleCatObjMap {Y Z : Cᵒᵖ} (f : Y ⟶ Z) :
    forgetToPresheafModuleCatObjObj X hX M Y ⟶ forgetToPresheafModuleCatObjObj X hX M Z :=
  ModuleCat.ofHom (X := forgetToPresheafModuleCatObjObj X hX M Y) (Y := forgetToPresheafModuleCatObjObj X hX M Z)
    { toFun := fun x => M.map f x
      map_add' := by simp
      map_smul' := fun r x =>
        by
        simp only [ModuleCat.restrictScalars.smul_def, RingHom.id_apply, M.map_smul]
        rw [← RingCat.comp_apply, ← R.map_comp]
        congr
        apply hX.hom_ext }

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