Away localizations of quotients

Let B → A be a surjective ring map whose kernel is annihilated by some b ∈ B. Inverting b kills the kernel, so a localization of A away from the image of b is already a localization of B away from b.

In the other direction, localization away from an element commutes with quotients: if S is a localization of R away from f, then S ⧸ I S is a localization of R ⧸ I away from the image of f.

Main results

• IsLocalization.Away.of_surjective_of_mul_eq_zero: a localization of A away from the image of b is a localization of B away from b.
• IsLocalization.Away.quotient: S ⧸ I S is a localization of R ⧸ I away from the image of f whenever S is a localization of R away from f.

theorem IsLocalization.Away.of_surjective_of_mul_eq_zero {B : Type u_1} {A : Type u_2} {T : Type u_3} [CommRing B] [CommRing A] [CommRing T] [Algebra B A] [Algebra A T] [Algebra B T] [IsScalarTower B A T] (hBA : Function.Surjective ⇑(algebraMap B A)) {b : B} (hb : ∀ x ∈ RingHom.ker (algebraMap B A), b * x = 0) [Away ((algebraMap B A) b) T] : Away b T

Let B → A be surjective, with kernel annihilated by b ∈ B. Then a localization of A away from the image of b is a localization of B away from b.

instance IsLocalization.Away.quotient {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (f : R) [Away f S] (I : Ideal R) : Away ((Ideal.Quotient.mk I) f) (S ⧸ Ideal.map (algebraMap R S) I)

Localization away from an element commutes with quotients: if S is a localization of R away from f, then S ⧸ I S is a localization of R ⧸ I away from the image of f.