English
If A is a Semiring with an R-algebra structure, the localized module LocalizedModule S A forms aMonoid under multiplication, with multiplication defined by multiplying numerators and denominators.
Русский
Если A — полукольцо с структурой алгебры над R, локализованный модуль LocalizedModule S A образует моноид под умножением, где числители и знаменатели перемножаются.
LaTeX
$$$\\mathrm{mk}(a_1,s_1) \\cdot \\mathrm{mk}(a_2,s_2) = \\mathrm{mk}(a_1 a_2, s_1 s_2)$$$
Lean4
instance {A : Type*} [Semiring A] [Algebra R A] {S : Submonoid R} : Monoid (LocalizedModule S A) :=
{ mul := fun m₁ m₂ =>
liftOn₂ m₁ m₂ (fun x₁ x₂ => LocalizedModule.mk (x₁.1 * x₂.1) (x₁.2 * x₂.2))
(by
rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨b₁, t₁⟩ ⟨b₂, t₂⟩ ⟨u₁, e₁⟩ ⟨u₂, e₂⟩
rw [mk_eq]
use u₁ * u₂
dsimp only at e₁ e₂ ⊢
rw [eq_comm]
trans (u₁ • t₁ • a₁) • u₂ • t₂ • a₂
on_goal 1 => rw [e₁, e₂]
on_goal 2 => rw [eq_comm]
all_goals
rw [smul_smul, mul_mul_mul_comm, ← smul_eq_mul, ← smul_eq_mul (α := A), smul_smul_smul_comm, mul_smul,
mul_smul])
one := mk 1 (1 : S)
one_mul := by
rintro ⟨a, s⟩
exact mk_eq.mpr ⟨1, by simp only [one_mul, one_smul]⟩
mul_one := by
rintro ⟨a, s⟩
exact mk_eq.mpr ⟨1, by simp only [mul_one, one_smul]⟩
mul_assoc := by
rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨a₃, s₃⟩
apply mk_eq.mpr _
use 1
simp only [one_mul, smul_smul, ← mul_assoc] }
