Localizing a product of commutative rings

Main Result

• bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom: the canonical map from a localization of a finite product of rings R i at a monoid M to the direct product of localizations R i at the projection of M onto each corresponding factor is bijective.

Implementation notes

See Mathlib/RingTheory/Localization/Defs.lean for a design overview.

Tags

localization, commutative ring

instance IsLocalization.instForallPiUniv {ι : Type u_1} (R : ι → Type u_2) (S : ι → Type u_3) [(i : ι) → CommSemiring (R i)] [(i : ι) → CommSemiring (S i)] [(i : ι) → Algebra (R i) (S i)] (M : (i : ι) → Submonoid (R i)) [∀ (i : ι), IsLocalization (M i) (S i)] : IsLocalization (Submonoid.pi Set.univ M) ((i : ι) → S i)

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.

theorem IsLocalization.iff_map_piEvalRingHom {ι : Type u_1} (R : ι → Type u_2) [(i : ι) → CommSemiring (R i)] (S' : Type u_4) [CommSemiring S'] [Algebra ((i : ι) → R i) S'] (M : Submonoid ((i : ι) → R i)) [Finite ι] : IsLocalization M S' ↔ IsLocalization (Submonoid.pi Set.univ fun (i : ι) => Submonoid.map (Pi.evalRingHom R i) M) S'

theorem IsLocalization.isUnit_piRingHom_algebraMap_comp_piEvalRingHom {ι : Type u_1} (R : ι → Type u_2) (S : ι → Type u_3) [(i : ι) → CommSemiring (R i)] [(i : ι) → CommSemiring (S i)] [(i : ι) → Algebra (R i) (S i)] (M : Submonoid ((i : ι) → R i)) [∀ (i : ι), IsLocalization (Submonoid.map (Pi.evalRingHom R i) M) (S i)] (y : ↥M) : IsUnit ((Pi.ringHom fun (i : ι) => (algebraMap (R i) (S i)).comp (Pi.evalRingHom R i)) ↑y)

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 corresponding factor. Given a ring homomorphism from the direct product Π i, R i to the product of the localizations of each R i at M' i, every y : M maps to a unit under this homomorphism.

theorem IsLocalization.bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom {ι : Type u_1} (R : ι → Type u_2) (S : ι → Type u_3) [(i : ι) → CommSemiring (R i)] [(i : ι) → CommSemiring (S i)] [(i : ι) → Algebra (R i) (S i)] (S' : Type u_4) [CommSemiring S'] [Algebra ((i : ι) → R i) S'] (M : Submonoid ((i : ι) → R i)) [∀ (i : ι), IsLocalization (Submonoid.map (Pi.evalRingHom R i) M) (S i)] [IsLocalization M S'] [Finite ι] : Function.Bijective ⇑(lift ⋯)

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 IsLocalization.surjective_piRingHom_algebraMap_comp_piEvalRingHom {ι : Type u_1} {R : ι → Type u_2} (S : ι → Type u_3) [(i : ι) → CommSemiring (R i)] [(i : ι) → CommSemiring (S i)] [(i : ι) → Algebra (R i) (S i)] (M : Submonoid ((i : ι) → R i)) [∀ (i : ι), IsLocalization (Submonoid.map (Pi.evalRingHom R i) M) (S i)] [∀ (i : ι), Ring.KrullDimLE 0 (R i)] [∀ (i : ι), IsLocalRing (R i)] : Function.Surjective ⇑(Pi.ringHom fun (i : ι) => (algebraMap (R i) (S i)).comp (Pi.evalRingHom R i))

theorem IsLocalization.algebraMap_pi_surjective_of_isLocalization {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → CommSemiring (R i)] (S' : Type u_4) [CommSemiring S'] [Algebra ((i : ι) → R i) S'] (M : Submonoid ((i : ι) → R i)) [∀ (i : ι), Ring.KrullDimLE 0 (R i)] [∀ (i : ι), IsLocalRing (R i)] [IsLocalization M S'] [Finite ι] : Function.Surjective ⇑(algebraMap ((i : ι) → R i) S')

Let M be a submonoid of a direct product of commutative rings R i. If each R i has maximal nilradical then the direct product ∏ R i surjects onto the localization of ∏ R i at M.