English
There is a scalar action of T on LocalizedModule S M, defined by x · mk m s = mk ((IsLocalization.sec S x).1 · m) ((IsLocalization.sec S x).2 · s).
Русский
Действие скаляра T на LocalizedModule S M задано формулой x · mk m s = mk ((IsLocalization.sec S x).1 · m) ((IsLocalization.sec S x).2 · s).
LaTeX
$$$x \\cdot \\mathrm{mk}(m,s) = \\mathrm{mk}((\\text{IsLocalization.sec } S x).1 \\cdot m, (\\text{IsLocalization.sec } S x).2 \\cdot s)$$$
Lean4
noncomputable instance : SMul T (LocalizedModule S M) where
smul x
p :=
let a := IsLocalization.sec S x
liftOn p (fun p ↦ mk (a.1 • p.1) (a.2 * p.2))
(by
rintro p p' ⟨s, h⟩
refine mk_eq.mpr ⟨s, ?_⟩
calc
_ = a.2 • a.1 • s • p'.2 • p.1 := by simp_rw [Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul]; ring_nf
_ = a.2 • a.1 • s • p.2 • p'.1 := by rw [h]
_ = s • (a.2 * p.2) • a.1 • p'.1 := by simp_rw [Submonoid.smul_def, ← mul_smul, Submonoid.coe_mul]; ring_nf)
