pushforward_map_app_apply' — Mathlib

English

There is an equivalence between morphisms from the pushforward and morphisms from the original presheaf after restriction

Русский

Существует эквиваленция между отображениями из pushforward и отображениями из исходной прешефы после ограничения

LaTeX

$$$\\mathrm{pushforward}.Hom\\; M\\to N\\; \\cong\\; M \\to (\\mathrm{restrictScalars}(\\varphi).obj (N))$$$

Lean4

/-- `@[simp]`-normal form of `pushforward_map_app_apply`. -/
@[simp]
theorem pushforward_map_app_apply' {M N : PresheafOfModules.{v} R} (α : M ⟶ N) (X : Cᵒᵖ)
    (m : (ModuleCat.restrictScalars (φ.app X).hom).obj (M.obj (Opposite.op (F.obj X.unop)))) :
    DFunLike.coe (F := ↑((ModuleCat.restrictScalars _).obj _) →ₗ[_] ↑((ModuleCat.restrictScalars _).obj _))
        (((pushforward φ).map α).app X).hom m =
      α.app (Opposite.op (F.obj X.unop)) m :=
  rfl

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