pushforward_map_app_apply — Mathlib

English

A variant of the pushforward map at X with a morphism α

Русский

Вариант отображения pushforward в точке X с гомоморфизмом α

LaTeX

$$$\\bigl(\\mathrm{pushforward}(\\varphi).map \\alpha\\bigr).app X \\;\\mathrm{hom} = \\alpha.app (F.obj X.unop)\\;$$

Lean4

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)))) :
    (((pushforward φ).map α).app X).hom m = α.app (Opposite.op (F.obj X.unop)) m :=
  rfl

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