English
Let M be a submonoid of a finite family of commutative rings {R_i}. Denote by M_i the projection of M to the i-th factor. Then the canonical map from the localization of the product ∏_i R_i at M to the product of the localizations of each R_i at M_i is a bijection; in particular, there exists a ring isomorphism Loc_M(∏_i R_i) ≅ ∏_i Loc_{M_i}(R_i).
Русский
Пусть M — подмоном в конечном произведении коммутативных колец {R_i}. Обозначим M_i проекцию M на i-ую координату. Тогда каноническое отображение локализации произведения ∏_i R_i по M в произведение локализаций каждого R_i по M_i является биекцией; существует изоморфизм Loc_M(∏_i R_i) ≅ ∏_i Loc_{M_i}(R_i).
LaTeX
$$$\\operatorname{Loc}_{M}\\left(\\prod_{i=1}^n R_i\\right) \\cong \\prod_{i=1}^n \\operatorname{Loc}_{\\pi_i(M)}(R_i)$$$
Lean4
/-- Let `M` be a submonoid of a direct product of commutative rings `R i`, and let `M' i` denote
the projection of `M` onto each factor. Then the canonical map from the localization of the direct
product `Π i, R i` at `M` to the direct product of the localizations of each `R i` at `M' i`
is bijective. -/
theorem bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom [IsLocalization M S'] [Finite ι] :
Function.Bijective (lift (S := S') (isUnit_piRingHom_algebraMap_comp_piEvalRingHom R S M)) :=
have := (iff_map_piEvalRingHom R (Π i, S i) M).mpr inferInstance
(ringEquivOfRingEquiv (M := M) (T := M) _ _ (.refl _) <| Submonoid.map_equiv_eq_comap_symm _ _).bijective
