English
Let M be a submonoid of a direct product of rings; a unit result holds for the pi-localized map into the product of localizations.
Русский
Пусть M — подмоноид прямого произведения колец; получаем единичность элемента после отображения через локализацию в произведение локализаций.
LaTeX
$$$\\text{IsLocalization}(M) \\,\\Rightarrow \\, \\text{IsUnit}(\\Pi \\text{ringHom}(...)(y))$$$
Lean4
/-- If `S i` is a localization of `R i` at the submonoid `M i` for each `i`,
then `Π i, S i` is a localization of `Π i, R i` at the product submonoid. -/
instance (M : Π i, Submonoid (R i)) [∀ i, IsLocalization (M i) (S i)] : IsLocalization (.pi .univ M) (Π i, S i)
where
map_units m := Pi.isUnit_iff.mpr fun i ↦ map_units _ ⟨m.1 i, m.2 i ⟨⟩⟩
surj
z := by
choose rm h using fun i ↦ surj (M := M i) (z i)
exact ⟨(fun i ↦ (rm i).1, ⟨_, fun i _ ↦ (rm i).2.2⟩), funext h⟩
exists_of_eq {x y}
eq := by
choose c hc using fun i ↦ exists_of_eq (M := M i) (congr_fun eq i)
exact ⟨⟨_, fun i _ ↦ (c i).2⟩, funext hc⟩
