English
Assuming α acts compatibly on R and A via IsScalarTower, there is a natural SMul action of α on the homogeneous localization HomogeneousLocalization 𝒜 x, defined by m · [a/s] = [m·a / s].
Русский
При условии совместимости действия α на R и A через IsScalarTower существует естественное скалярное действие α на однородную локализацию HomogeneousLocalization 𝒜 x, заданное формулой m · [a/s] = [m·a / s].
LaTeX
$$$\text{There is a scalar action } \alpha \times \mathrm{HomogeneousLocalization}_{\mathcal{A}}(x) \to \mathrm{HomogeneousLocalization}_{\mathcal{A}}(x),\ (m,y) \mapsto m\cdot y$$$
Lean4
instance : SMul α (HomogeneousLocalization 𝒜 x) where
smul
m :=
Quotient.map' (m • ·) fun c1 c2 (h : Localization.mk _ _ = Localization.mk _ _) =>
by
change Localization.mk _ _ = Localization.mk _ _
simp only [num_smul, den_smul]
convert congr_arg (fun z : at x => m • z) h <;> rw [Localization.smul_mk]
