English
If M ≤ N are submonoids and there is a condition that every element of N is some multiple of an element of M (in a suitable sense), then N determines the same localization as M; i.e., IsLocalization N S holds if IsLocalization M S and the specified condition holds.
Русский
Если N состоит из умножений элементов M в нужном смысле, локализация N равна локализации M.
LaTeX
$$IsLocalization N S$$
Lean4
/-- If `M ≤ N` are submonoids of `R` such that `∀ x : N, ∃ m : R, m * x ∈ M`, then the
localization at `N` is equal to the localization of `M`. -/
theorem isLocalization_of_is_exists_mul_mem (M N : Submonoid R) [IsLocalization M S] (h : M ≤ N)
(h' : ∀ x : N, ∃ m : R, m * x ∈ M) : IsLocalization N S
where
map_units
y := by
obtain ⟨m, hm⟩ := h' y
have := IsLocalization.map_units S ⟨_, hm⟩
rw [map_mul] at this
exact (IsUnit.mul_iff.mp this).2
surj
z := by
obtain ⟨⟨y, s⟩, e⟩ := IsLocalization.surj M z
exact ⟨⟨y, _, h s.prop⟩, e⟩
exists_of_eq
{_ _} := by
rw [IsLocalization.eq_iff_exists M]
exact fun ⟨x, hx⟩ => ⟨⟨_, h x.prop⟩, hx⟩
