zsmul_app — Mathlib

English

Integer scalar multiplication on morphisms in PresheafOfModules is computed componentwise: (n • f).app X = n • f.app X.

Русский

Целочисленное умножение на морфизмы в PresheafOfModules вычисляется покомпонентно: (n • f).app X = n • f.app X.

LaTeX

$$$ (n \cdot f).\mathrm{app} \\ X = n \\cdot f.\\mathrm{app} \\ X $$$

Lean4

theorem zsmul_app (n : ℤ) (f : M₁ ⟶ M₂) (X : Cᵒᵖ) : (n • f).app X = n • f.app X :=
  by
  ext x
  change (toPresheaf R ⋙ (evaluation _ _).obj X).map (n • f) x = _
  rw [Functor.map_zsmul]
  rfl

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