Localization of localization

Stream: Is there code for X?

[Andrew Yang]

Do we have results about the localization of a localization? Something like

import ring_theory.localization

variables (R : Type*) [comm_ring R] (M : submonoid R) (S : Type*) [comm_ring S] [algebra R S]
variables [is_localization M S] (N : submonoid S) (T : Type*) [comm_ring T] [algebra S T]
variables [is_localization N T] [algebra R T] [is_scalar_tower R S T]

example : is_localization ((N ⊔ M.map (algebra_map R S)).comap (algebra_map R S).to_monoid_hom) T := sorry

[Anne Baanen]

I don't think so, at least I'm sure that we didn't a couple months ago and I haven't seen anything similar in the commit log.

[Johan Commelin]

That submonoid doesn't look like fun to work with.

[Johan Commelin]

It might be best to abstract it away as soon as possible

[Andrew Yang]

#10456
Though I'm not that well-versed in the localization library to give a concise proof.
Any golfing opportunities?

import ring_theory.localization

variables {R : Type*} [comm_ring R] (M : submonoid R) {S : Type*} [comm_ring S] [algebra R S]
variables [is_localization M S] (N : submonoid S) (T : Type*) [comm_ring T] [algebra S T]
variables [algebra R T] [is_scalar_tower R S T]

lemma localization_localization_is_localization [is_localization N T] :
  is_localization ((N ⊔ M.map (algebra_map R S)).comap (algebra_map R S).to_monoid_hom) T :=
{ map_units := begin
    rintros ⟨y, h⟩,
    erw submonoid.mem_sup at h,
    rcases h with ⟨y, hy, z, hz, eq⟩,
    rw [is_scalar_tower.algebra_map_eq R S T, ring_hom.comp_apply],
    erw ← eq,
    simp only [set_like.coe_mk, is_unit.mul_iff, ring_hom.map_mul],
    split,
    exact is_localization.map_units T ⟨y, hy⟩,
    refine is_unit.map (algebra_map S T).to_monoid_hom _,
    rcases hz with ⟨z, hz, rfl⟩,
    apply is_localization.map_units _ ⟨z, hz⟩,
    apply_instance
  end,
  surj := λ x, begin
    rcases is_localization.surj N x with ⟨⟨y, s⟩, eq₁⟩, -- x = y / s
    rcases is_localization.surj M y with ⟨⟨z, t⟩, eq₂⟩, -- y = z / t
    rcases is_localization.surj M s.1 with ⟨⟨z', t'⟩, eq₃⟩, -- s = z' / t'
    dsimp only at eq₁ eq₂ eq₃,
    use z * t', use z' * t, -- x = y / s = (z * t') / (z' * t)
    { erw submonoid.mem_sup,
      refine ⟨s.1, s.2, _, ⟨_, submonoid.mul_mem _ t.2 t'.2, rfl⟩, _⟩,
      erw [mul_comm t.val, ring_hom.map_mul, ring_hom.map_mul, ← eq₃, mul_assoc],
      refl },
    { simp only [set_like.coe_mk, mul_assoc, function.comp_app, ← eq₂, ← eq₁, ring_hom.coe_comp,
        ring_hom.map_mul, subtype.val_eq_coe, ← eq₃, is_scalar_tower.algebra_map_eq R S T],
      congr' 2,
      exact mul_comm _ _ },
  end,
  eq_iff_exists := λ x y, begin
    rw [is_scalar_tower.algebra_map_apply R S T, is_scalar_tower.algebra_map_apply R S T],
    rw is_localization.eq_iff_exists N T,
    split,
    { rintros ⟨z, eq₁⟩,
      rcases is_localization.surj M z.1 with ⟨⟨z', s⟩, eq₂⟩,
      replace eq₁ := congr_arg (λ x, x * algebra_map R S s) eq₁,
      dsimp only [subtype.val_eq_coe] at eq₁ eq₂,
      rw [mul_assoc, mul_assoc, eq₂, ← ring_hom.map_mul, ← ring_hom.map_mul,
        is_localization.eq_iff_exists M S] at eq₁,
      rcases eq₁ with ⟨c, eq₃⟩,
      use z' * c,
      { erw [submonoid.mem_sup, ring_hom.map_mul, ← eq₂],
        refine ⟨z.1, z.2, _, ⟨_, submonoid.mul_mem _ s.2 c.2, rfl⟩, _⟩,
        rw [monoid_hom.map_mul, mul_assoc],
        refl },
      { simpa [mul_assoc] using eq₃ } },
    { rintro ⟨⟨c, hc⟩, eq₁⟩,
      erw submonoid.mem_sup at hc,
      rcases hc with ⟨z₁, hz₁, z₂, hz₂, eq₂⟩,
      use ⟨z₁, hz₁⟩,
      replace eq₁ := congr_arg (λ x, algebra_map R S x * ring.inverse z₂) eq₁,
      dsimp only at eq₁,
      rw [ring_hom.map_mul, ring_hom.map_mul] at eq₁,
      erw ← eq₂ at eq₁,
      have : is_unit (z₂ : S),
      { rcases hz₂ with ⟨z, hz, rfl⟩,
        exact is_localization.map_units S ⟨z, hz⟩ },
      simpa [mul_assoc, ring.mul_inverse_cancel _ this] using eq₁ }
  end }