English
The canonical congruence r on M × S yields the localization of M at S as the quotient; i.e., Localization is given by (M × S)/r(S).
Русский
Каноническое тождество r на M × S задаёт локализацию M в S как фактор-облако; то есть Localization ≅ (M × S)/r(S).
LaTeX
$$$ \text{Localization}(M,S) \cong (M \times S)/r(S) $$$
Lean4
/-- The congruence relation on `M × S`, `M` a `CommMonoid` and `S` a submonoid of `M`, whose
quotient is the localization of `M` at `S`, defined as the unique congruence relation on
`M × S` such that for any other congruence relation `s` on `M × S` where for all `y ∈ S`,
`(1, 1) ∼ (y, y)` under `s`, we have that `(x₁, y₁) ∼ (x₂, y₂)` by `r` implies
`(x₁, y₁) ∼ (x₂, y₂)` by `s`. -/
@[to_additive /-- The congruence relation on `M × S`, `M` an `AddCommMonoid` and `S` an `AddSubmonoid` of `M`,
whose quotient is the localization of `M` at `S`, defined as the unique congruence relation on
`M × S` such that for any other congruence relation `s` on `M × S` where for all `y ∈ S`,
`(0, 0) ∼ (y, y)` under `s`, we have that `(x₁, y₁) ∼ (x₂, y₂)` by `r` implies
`(x₁, y₁) ∼ (x₂, y₂)` by `s`. -/
]
def r (S : Submonoid M) : Con (M × S) :=
sInf {c | ∀ y : S, c 1 (y, y)}
