English
For any morphism π: X ⟶ Y, the action commutes with the structure maps: A(π)(smul_{α,φ}(r,m)) = smul_{α,φ}(R(π) r, A(π) m).
Русский
Для любого отображения\pi: X → Y действие совместимо с отображениями: A(π)(smul_{α,φ}(r, m)) = smul_{α,φ}(R(π) r, A(π) m).
LaTeX
$$$\forall X,Y,\forall \pi:\n 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 mul_smul : smul α φ (r * r') m = smul α φ r (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₀ : M₀.obj _, hm₀⟩⟩
rw [map_smul_eq α φ (r * r') m f.op (r₀ * r₀') (by rw [map_mul, map_mul, hr₀, hr₀']) m₀ hm₀, mul_smul,
map_smul_eq α φ r (smul α φ r' m) f.op r₀ hr₀ (r₀' • m₀) (map_smul_eq α φ r' m f.op r₀' hr₀' m₀ hm₀).symm]
