pushforward₀_obj — Mathlib

Lean4

/-- Implementation of `pushforward₀`. -/
@[simps]
def pushforward₀_obj (R : Dᵒᵖ ⥤ RingCat.{u}) (M : PresheafOfModules R) : PresheafOfModules (F.op ⋙ R) :=
  { obj X := ModuleCat.of _ (M.obj (F.op.obj X))
    map {X Y} f := M.map (F.op.map f)
    map_id
      X := by
      refine ModuleCat.hom_ext (@LinearMap.ext _ _ _ _ _ _ _ _ (_) (_) _ _ _ (fun x => ?_))
      exact (M.congr_map_apply (F.op.map_id X) x).trans (by simp)
    map_comp := fun f g ↦
      by
      refine ModuleCat.hom_ext (@LinearMap.ext _ _ _ _ _ _ _ _ (_) (_) _ _ _ (fun x => ?_))
      exact (M.congr_map_apply (F.op.map_comp f g) x).trans (by simp) }

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