map_smul_eq — Mathlib

English

The key equality map_smul_eq establishes compatibility of toSheafification with the scalar action.

Русский

Утверждение map_smul_eq устанавливает совместимость действия скаляров с отображением.

LaTeX

$$$ map\_smul\_eq: (map) = (adjunction.homEquiv) \circ (map) $$$

Lean4

theorem map_smul_eq {Y : Cᵒᵖ} (f : X ⟶ Y) (r₀ : R₀.obj Y) (hr₀ : α.app Y r₀ = R.val.map f r) (m₀ : M₀.obj Y)
    (hm₀ : φ.app Y m₀ = A.val.map f m) : A.val.map f (smul α φ r m) = φ.app Y (r₀ • m₀) :=
  (smulCandidate α φ r m).h f r₀ hr₀ m₀ hm₀

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