English
Let X be an object. For r, r' ∈ R(X) and m ∈ A(X), the scalar action is additive in the coefficient: (r + r') · m = r · m + r' · m.
Русский
Пусть X — объект. Пусть r, r' ∈ R(X) и m ∈ A(X). Тогде (r + r') · m = r · m + r' · m.
LaTeX
$$$\forall X\,\forall r,r'\in R(X)\,\forall m\in A(X):\\smul_{\alpha,\varphi}(r + r', m) = smul_{\alpha,\varphi}(r, m) + smul_{\alpha,\varphi}(r', m).$$$
Lean4
protected theorem add_smul : smul α φ (r + r') m = smul α φ r m + smul α φ r' m :=
by
let S := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
have hS : S ∈ J X.unop := by
refine J.intersection_covering (J.intersection_covering ?_ ?_) ?_
all_goals apply Presheaf.imageSieve_mem
apply A.isSeparated _ _ hS
rintro Y f
⟨⟨⟨r₀ : R₀.obj _, (hr₀ : (α.app (Opposite.op Y)) r₀ = (R.val.map f.op) r)⟩,
⟨r₀' : R₀.obj _, (hr₀' : (α.app (Opposite.op Y)) r₀' = (R.val.map f.op) r')⟩⟩,
⟨m₀, hm₀⟩⟩
rw [(A.val.map f.op).hom.map_add, map_smul_eq α φ r m f.op r₀ hr₀ m₀ hm₀, map_smul_eq α φ r' m f.op r₀' hr₀' m₀ hm₀,
map_smul_eq α φ (r + r') m f.op (r₀ + r₀') (by rw [_root_.map_add, _root_.map_add, hr₀, hr₀']) m₀ hm₀, add_smul,
_root_.map_add]
