pushforward_obj_map_apply — Mathlib

English

The map component of pushforward at X sends m to α’s action via F.map along f.

Русский

Компонента отображения pushforward на X отправляет m под действием F.map вдоль f.

LaTeX

$$$((\\mathrm{pushforward}(\\varphi)\\!\\!\\! ).obj M).map f \\;\\mathrm{hom} \\; m = M.map (F.map f.unop).op m$$$

Lean4

theorem pushforward_obj_map_apply (M : PresheafOfModules.{v} R) {X Y : Cᵒᵖ} (f : X ⟶ Y)
    (m : (ModuleCat.restrictScalars (φ.app X).hom).obj (M.obj (Opposite.op (F.obj X.unop)))) :
    (((pushforward φ).obj M).map f).hom m = M.map (F.map f.unop).op m :=
  rfl

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