English
The localized module LocalizedModule S M carries an additive commutative group structure extending the addition in M; in particular, addition is well-defined and satisfies the group axioms after localization.
Русский
Локализованный модуль LocalizedModule S M имеет структуру аддитивной коммутативной группы, расширяющую сложение в M; операция сложения корректно определена после локализации и удовлетворяет аксиомам группы.
LaTeX
$$$\\big(\\mathrm{LocalizedModule}(S,M), +, 0\\big) \\text{ is an abelian group}$$$
Lean4
instance {M : Type*} [AddCommGroup M] [Module R M] : AddCommGroup (LocalizedModule S M) :=
{
show AddCommMonoid (LocalizedModule S M) by
infer_instance with
neg_add_cancel := by
rintro ⟨m, s⟩
change
(liftOn (mk m s) (fun x => mk (-x.1) x.2) fun ⟨m1, s1⟩ ⟨m2, s2⟩ ⟨u, hu⟩ =>
by
rw [mk_eq]
exact ⟨u, by simpa⟩) +
mk m s =
0
rw [liftOn_mk, mk_add_mk]
simp
-- TODO: fix the diamond
zsmul := zsmulRec }
