English
For a morphism π, the scalar action commutes with the map: A(π)(smul_{α,φ}(r,m)) = smul_{α,φ}(R(π) r, A(π) m).
Русский
Для отображения\pi скалярное умножение сохраняется под отображением: A(π)(smul_{α,φ}(r, m)) = smul_{α,φ}(R(π) r, A(π) m).
LaTeX
$$$\forall \pi:\ X \to Y,\forall r\in R(X), m\in A(X):\\A(\pi)(smul_{\alpha,\varphi}(r, m)) = smul_{\alpha,\varphi}(R(\pi) r, A(\pi) m).$$$
Lean4
protected theorem map_smul : A.val.map π (smul α φ r m) = smul α φ (R.val.map π r) (A.val.map π m) :=
by
let S := Presheaf.imageSieve α (R.val.map π r) ⊓ Presheaf.imageSieve φ (A.val.map π m)
have hS : S ∈ J Y.unop := by
apply J.intersection_covering
all_goals apply Presheaf.imageSieve_mem
apply A.isSeparated _ _ hS
rintro Y f
⟨⟨r₀, (hr₀ : (α.app (Opposite.op Y)).hom r₀ = (R.val.map f.op).hom ((R.val.map π).hom r))⟩,
⟨m₀, (hm₀ : (φ.app _) _ = _)⟩⟩
rw [← ConcreteCategory.comp_apply, ← Functor.map_comp,
map_smul_eq α φ r m (π ≫ f.op) r₀ (by rw [hr₀, Functor.map_comp, RingCat.comp_apply]) m₀
(by rw [hm₀, Functor.map_comp, ConcreteCategory.comp_apply]),
map_smul_eq α φ (R.val.map π r) (A.val.map π m) f.op r₀ hr₀ m₀ hm₀]
