English
There exists a localization of R away from r, provided that algebraMap_R^S(r) is a unit, together with surjectivity data and a compatibility condition: if algebraMap_R^S(a) = algebraMap_R^S(b) then there is n with r^n a = r^n b.
Русский
Существует локализация R away от r, если алгебраическая карта алгебраического отображения R в S отображается в единицу, вместе с данными сюръекции и совместимостью: если алгебраMap_R^S(a) = алгебраMap_R^S(b), то существует n такое, что r^n a = r^n b.
LaTeX
$$$\\text{If } r \\in R,\\; \\mathsf{IsUnit}(\\operatorname{algebraMap}_{R,S}(r))\\text{, surj: } \\forall s, \\exists n,a:\\; s\\cdot \\operatorname{algebraMap}_{R,S}(r)^n = \\operatorname{algebraMap}_{R,S}(a) \\text{ and } exists_of_eq:\\; ∀ a,b,\\; \\operatorname{algebraMap}_{R,S}(a)=\\operatorname{algebraMap}_{R,S}(b) \\Rightarrow \\exists n:\\; r^n a = r^n b$ implies IsLocalization.Away r S exists.$$
Lean4
/-- Specialized constructor for `IsLocalization.Away`. -/
theorem mk (r : R) (map_unit : IsUnit (algebraMap R S r))
(surj : ∀ s, ∃ (n : ℕ) (a : R), s * algebraMap R S r ^ n = algebraMap R S a)
(exists_of_eq : ∀ a b, algebraMap R S a = algebraMap R S b → ∃ (n : ℕ), r ^ n * a = r ^ n * b) :
IsLocalization.Away r S
where
map_units := by
rintro ⟨-, n, rfl⟩
simp only [map_pow]
exact IsUnit.pow _ map_unit
surj
z := by
obtain ⟨n, a, hn⟩ := surj z
use ⟨a, ⟨r ^ n, n, rfl⟩⟩
simpa using hn
exists_of_eq {x y}
h := by
obtain ⟨n, hn⟩ := exists_of_eq x y h
use ⟨r ^ n, n, rfl⟩
