pushforward_obj_map_apply' — Mathlib

English

The same identity as above but in simplified, explicit form for the forgetful target.

Русский

Та же идентичность, упрощенная на целевом забывчивом объекте.

LaTeX

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

Lean4

/-- `@[simp]`-normal form of `pushforward_obj_map_apply`. -/
@[simp]
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)))) :
    DFunLike.coe (F :=
        ↑((ModuleCat.restrictScalars _).obj _) →ₗ[_]
          ↑((ModuleCat.restrictScalars (S.map f).hom).obj ((ModuleCat.restrictScalars _).obj _)))
        (((pushforward φ).obj M).map f).hom m =
      M.map (F.map f.unop).op m :=
  rfl

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