Intermediate rings of a localization

Let S be a localization of A at a submonoid M, and let B be an intermediate A-algebra whose map to S is injective, for instance an A-subalgebra of S. Then S is also the localization of B at the image of M: inverting M in B changes nothing beyond S. In particular, for the localization away from an element a, the induced map A_a → B_a is bijective.

This applies to the affine charts A[I/a] ⊆ A_a of a blowup, which become A_a again after inverting a.

Main results

• IsLocalization.isLocalization_algebraMapSubmonoid_of_injective: S is the localization of B at the image of M.
• IsLocalization.Away.bijective_awayMap_of_injective: for S a localization away from a, the map Localization.awayMap (algebraMap A B) a : A_a → B_a is bijective.

theorem IsLocalization.isLocalization_algebraMapSubmonoid_of_injective {A : Type u_1} {B : Type u_2} {S : Type u_3} [CommSemiring A] [CommSemiring B] [CommSemiring S] [Algebra A B] [Algebra B S] [Algebra A S] [IsScalarTower A B S] (M : Submonoid A) [IsLocalization M S] (h : Function.Injective ⇑(algebraMap B S)) : IsLocalization (Algebra.algebraMapSubmonoid B M) S

An intermediate ring of a localization. If S is a localization of A at M and the map B → S from an intermediate A-algebra B is injective, then S is the localization of B at the image of M.

theorem IsLocalization.Away.bijective_awayMap_of_injective {A : Type u_1} {B : Type u_2} {S : Type u_3} [CommSemiring A] [CommSemiring B] [CommSemiring S] [Algebra A B] [Algebra B S] [Algebra A S] [IsScalarTower A B S] (a : A) [Away a S] (h : Function.Injective ⇑(algebraMap B S)) : Function.Bijective ⇑(Localization.awayMap (algebraMap A B) a)

Inverting a in an intermediate ring of A_a. If S is a localization of A away from a and the map B → S from an intermediate A-algebra B is injective, then the induced map A_a → B_a of localizations away from a is bijective.