English
For any s in S, there is an R-linear map divBy(s): LocalizedModule S M → LocalizedModule S M defined by p ↦ mk p.1 (p.2 · s); it is well-defined and linear.
Русский
Для любого s ∈ S существует R-линейное отображение divBy(s): LocalizedModule S M → LocalizedModule S M, заданное p ↦ mk p.1 (p.2 · s); оно корректно определено и линейно.
LaTeX
$$$\\mathrm{divBy}(s)(p) = \\mathrm{mk}(p.1, p.2\\cdot s) \\quad( p=\\mathrm{mk}(p.1,p.2) ).$$$
Lean4
/-- For any `s : S`, there is an `R`-linear map given by `a/b ↦ a/(b*s)`.
-/
@[simps]
noncomputable def divBy (s : S) : LocalizedModule S M →ₗ[R] LocalizedModule S M
where
toFun
p :=
p.liftOn (fun p => mk p.1 (p.2 * s)) fun ⟨a, b⟩ ⟨a', b'⟩ ⟨c, eq1⟩ =>
mk_eq.mpr ⟨c, by rw [mul_smul, mul_smul, smul_comm _ s, smul_comm _ s, eq1, smul_comm _ s, smul_comm _ s]⟩
map_add' x
y := by
refine x.induction_on₂ ?_ y
intro m₁ m₂ t₁ t₂
simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc, smul_comm _ s, ←
smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left s]
map_smul' r
x := by
refine x.induction_on (fun _ _ ↦ ?_)
change liftOn (mk _ _) _ _ = r • (liftOn (mk _ _) _ _)
simp_rw [liftOn_mk, mul_assoc, ← smul_def]
congr!
