A lemma about localization

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

universe u

variable (R : Type u) [CommRing R]
  (J : Type) [Fintype J] (elem : J → R) (span : Ideal.span (Set.range elem) = ⊤)
  (loc : J → Type u) [∀ j, CommRing (loc j)] [∀ j, Algebra R (loc j)]
    [∀ j, IsLocalization.Away (elem j) (loc j)]

-- now for each `j : J`, do the same thing:
variable (K : J → Type) [∀ k, Fintype (K k)]
  (elems : ∀ j, K j → loc j) (spans : ∀ j, Ideal.span (Set.range (elems j)) = ⊤)
  (locs : ∀ j, K j → Type u) [∀ j k, CommRing (locs j k)] [∀ j k, Algebra (loc j) (locs j k)]
    [∀ j k, IsLocalization.Away (elems j k) (locs j k)]

include R J elem span loc K elems spans locs

theorem span_elems : Ideal.span (Set.range fun jk : (j : J) × K j ↦
    elem jk.fst * (IsLocalization.Away.sec (elem jk.fst) (elems jk.fst jk.snd)).1) = ⊤ :=
  sorry

instance (j : J) (k : K j) : IsLocalization.Away
    (elem j * (IsLocalization.Away.sec (elem j) (elems j k)).1)
    (RestrictScalars R (loc j) (locs j k)) :=
  sorry

[Kenny Lau]

Let $(f_1, \cdots, f_n) = R$, and then for each $R[1/f_i]$ we do the same thing, i.e. pick $f_{ij} \in R[1/f_i]$ such that $(f_{i1}, \cdots, f_{in_i}) = R[1/f_i]$.

Then pick representatives $f_{ij} = r_{ij}/f_i^{a_{ij}}$, where $r_{ij} \in R$. (that's the sec in the code)

Then I claim that firstly each new localization is a localization over $R$, i.e. $R[1/f_i][1/f_{ij}] = R[1/(f_i r_{ij})]$,

and secondly I claim that $(f_i r_{ij}) = R$.

[Kenny Lau]

Are these two lemmas (or any simpler form) in mathlib?

[Kenny Lau]

ok it seems like I can use IsLocalization.Away.mul' as a step

[Kenny Lau]

I need to first prove that $R[1/f_i][1/f_{ij}] = R[1/f_i][1/r_{ij}]$, and for that I need to show that "multiplying a unit" doesn't change the truth value of IsLocalization

[Kenny Lau]

ok I see that it is IsLocalization.Away.of_associated

[Kenny Lau]

Ok I now have a rather long proof of the two lemmas.

[Kenny Lau]

import Mathlib

universe u

variable {R : Type u} [CommRing R]
  {J : Type} [Fintype J] (elem : J → R) (span : Ideal.span (Set.range elem) = ⊤)
  (loc : J → Type u) [∀ j, CommRing (loc j)] [∀ j, Algebra R (loc j)]
    [∀ j, IsLocalization.Away (elem j) (loc j)]

-- now for each `j : J`, do the same thing:
variable {K : J → Type} [∀ k, Fintype (K k)]
  (elems : ∀ j, K j → loc j) (spans : ∀ j, Ideal.span (Set.range (elems j)) = ⊤)
  (locs : ∀ j, K j → Type u) [∀ j k, CommRing (locs j k)] [∀ j k, Algebra (loc j) (locs j k)]
    [∀ j k, IsLocalization.Away (elems j k) (locs j k)]

-- scalar tower
variable [∀ j k, Algebra R (locs j k)] [∀ j k, IsScalarTower R (loc j) (locs j k)]

variable (j : J) (k : K j)

noncomputable def bindElem : R :=
  (IsLocalization.Away.sec (elem j) (elems j k)).1

lemma associated_bindElem :
    Associated (algebraMap R (loc j) (bindElem elem loc elems j k)) (elems j k) := by
  unfold bindElem
  rw [← IsLocalization.Away.sec_spec, map_pow]
  exact associated_mul_unit_left _ _ (.pow _ <| IsLocalization.Away.algebraMap_isUnit _)

instance foo : IsLocalization.Away (algebraMap R (loc j) (bindElem elem loc elems j k)) (locs j k) :=
  IsLocalization.Away.of_associated (associated_bindElem elem loc elems j k).symm

include spans in
theorem span_map_bindElem_eq_top :
    Ideal.span (Set.range (algebraMap R (loc j) ∘ bindElem elem loc elems j)) = ⊤ := by
  rw [eq_top_iff, ← spans, Ideal.span_le, Set.range_subset_iff]
  exact fun k ↦ let ⟨u, hu⟩ := associated_bindElem elem loc elems j k
    hu ▸ Ideal.mul_mem_right _ _ (Ideal.subset_span <| Set.mem_range_self _)

include spans in
theorem exists_pow_mem_span_bindElem :
    ∃ n : ℕ, elem j ^ n ∈ Ideal.span (Set.range (bindElem elem loc elems j)) := by
  have := span_map_bindElem_eq_top elem loc elems spans j
  rw [Ideal.eq_top_iff_one, Set.range_comp, ← Ideal.map_span, ← map_one (algebraMap R (loc j)),
    IsLocalization.algebraMap_mem_map_algebraMap_iff (Submonoid.powers (elem j))] at this
  obtain ⟨_, ⟨n, rfl⟩, hn⟩ := this
  exact ⟨n, by simpa using hn⟩

include spans in
theorem exists_pow_mem_span_mul_bindElem :
    ∃ n : ℕ, elem j ^ n ∈ Ideal.span (Set.range fun k : K j ↦ elem j * bindElem elem loc elems j k) := by
  obtain ⟨n, hn⟩ := exists_pow_mem_span_bindElem elem loc elems spans j
  refine ⟨n + 1, ?_⟩
  rw [pow_succ']
  convert Ideal.mul_mem_mul (Ideal.mem_span_singleton_self _) hn
  rw [Ideal.span_mul_span', Set.singleton_mul, ← Set.range_comp]
  rfl

include span spans in
theorem span_bindElem_eq_top :
    Ideal.span (Set.range fun jk : (j : J) × K j ↦
      elem jk.fst * bindElem elem loc elems jk.fst jk.snd) = ⊤ := by
  have (j : J) := exists_pow_mem_span_mul_bindElem elem loc elems spans j
  choose n hn using this
  rw [eq_top_iff, ← Ideal.span_pow_eq_top _ span (∑ j : J, n j), Ideal.span_le,
    ← Set.range_comp, Set.range_subset_iff]
  refine fun j ↦ Ideal.mem_of_dvd _ ?_ (Ideal.span_mono ?_ (hn j))
  · exact pow_dvd_pow _ (Finset.single_le_sum (fun _ _ ↦ Nat.zero_le _) (Finset.mem_univ _))
  · exact Set.range_subset_iff.2 fun k ↦ ⟨⟨j, k⟩, rfl⟩

include span spans in
theorem span_elems : Ideal.span (Set.range fun jk : (j : J) × K j ↦
    elem jk.fst * (IsLocalization.Away.sec (elem jk.fst) (elems jk.fst jk.snd)).1) = ⊤ :=
  span_bindElem_eq_top elem span loc elems spans

instance (j : J) (k : K j) : IsLocalization.Away
    (elem j * (IsLocalization.Away.sec (elem j) (elems j k)).1)
    (locs j k) := by
  have := foo elem loc elems locs j k
  unfold bindElem at this
  exact IsLocalization.Away.mul' (loc j) _ _ _

[Kenny Lau]

Thanks to everyone who helped :duck: