English
An explicit form r'(S) of the congruence on M × S defining the localization; it is equivalent to r(S).
Русский
Явно заданная форма r'(S) конгруэнции на M × S, задающая локализацию; она эквивалентна r(S).
LaTeX
$$$ r'(S) \;\text{is the explicit congruence on } M \times S \text{ defining the localization} $$$
Lean4
/-- An alternate form of the congruence relation on `M × S`, `M` a `CommMonoid` and `S` a
submonoid of `M`, whose quotient is the localization of `M` at `S`. -/
@[to_additive /-- An alternate form of the congruence relation on `M × S`, `M` a `CommMonoid` and `S` a
submonoid of `M`, whose quotient is the localization of `M` at `S`. -/
]
def r' : Con (M × S) := by
-- note we multiply by `c` on the left so that we can later generalize to `•`
refine
{ r := fun a b : M × S ↦ ∃ c : S, ↑c * (↑b.2 * a.1) = c * (a.2 * b.1)
iseqv := ⟨fun a ↦ ⟨1, rfl⟩, fun ⟨c, hc⟩ ↦ ⟨c, hc.symm⟩, ?_⟩
mul' := ?_ }
· rintro a b c ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩
use t₂ * t₁ * b.2
simp only [Submonoid.coe_mul]
calc
(t₂ * t₁ * b.2 : M) * (c.2 * a.1) = t₂ * c.2 * (t₁ * (b.2 * a.1)) := by ac_rfl
_ = t₁ * a.2 * (t₂ * (c.2 * b.1)) := by rw [ht₁]; ac_rfl
_ = t₂ * t₁ * b.2 * (a.2 * c.1) := by rw [ht₂]; ac_rfl
· rintro a b c d ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩
use t₂ * t₁
calc
(t₂ * t₁ : M) * (b.2 * d.2 * (a.1 * c.1)) = t₂ * (d.2 * c.1) * (t₁ * (b.2 * a.1)) := by ac_rfl
_ = (t₂ * t₁ : M) * (a.2 * c.2 * (b.1 * d.1)) := by rw [ht₁, ht₂]; ac_rfl
