Ideal is intersection of comap_map along localisations

Stream: maths

[Geno Racklin Asher]

I'm currently attempting to formalise Prop. II.3.2 from Hartshorne's Algebraic Geometry, which states that a scheme is locally noetherian iff it has a cover by noetherian affines. I've done all the scheme-theoretic parts of the proof and have reduced it to proving the following algebraic statement (as in Hartshorne's proof):

variable {R : Type u} [CommRing R] (S : Finset R) (hS: Ideal.span (α := R) S = ⊤)

def mcm (I : Ideal R) (s : R) :=
  let f := algebraMap R (Localization.Away s)
  Ideal.comap f (Ideal.map f I)

lemma ideal_eq_sect (I : Ideal R) : I.carrier = ⋂ (s : S), mcm I s := by
  let floc s := algebraMap R (Localization.Away (M := R) s)
  apply Set.ext
  intro x
  apply Iff.intro
  . intro hx
    apply Set.mem_iInter.mpr
    intro s
    exact Ideal.le_comap_map hx
  . intro hx
    have hx: ∀ s : S, x ∈ mcm I s := by
      intro s
      apply Set.mem_iInter.mp hx s
    have : ∀ s : S, ∃ n : ℕ, (floc s x) * (floc s s ^ n) ∈ Ideal.map (floc s) I := by
      intro s
      have hx := hx s
      sorry
    sorry

But i'm now unsure how to proceed in formalising the remainder of the lemma. Hartshorne's proof is as follows:

image.png

Any advice for formalising this line of argument would be much appreciated!

[Yaël Dillies]

Hey Geno! :wave:

[Andrew Yang]

docs#IsLocalization.mem_map_algebraMap_iff is useful here.

[Andrew Yang]

And also docs#Submodule.mem_of_span_eq_top_of_smul_pow_mem

[Andrew Yang]

Those two should take you to the goal, but if you want to see my approach:

My approach

import Mathlib.RingTheory.Localization.Ideal

universe u

variable {R : Type u} [CommRing R] (S : Finset R) (hS: Ideal.span (α := R) S = ⊤)

open Localization in
lemma ideal_eq_sect (I : Ideal R) :
    I = ⨅ f ∈ S, (I.map (algebraMap R (Away f))).comap (algebraMap R (Away f)) := by
  apply le_antisymm
  · simp only [le_iInf₂_iff, ← Ideal.map_le_iff_le_comap, le_refl, implies_true]
  . intro x hx
    apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ _ hS
    rintro ⟨s, hs⟩
    simp only [Ideal.mem_iInf, Ideal.mem_comap] at hx
    obtain ⟨⟨y, ⟨_, n, rfl⟩⟩, e⟩ :=
      (IsLocalization.mem_map_algebraMap_iff (.powers s) _).mp (hx s hs)
    dsimp only at e
    rw [← map_mul, IsLocalization.eq_iff_exists (.powers s)] at e
    obtain ⟨⟨_, m, rfl⟩, e⟩ := e
    use m + n
    dsimp at e ⊢
    rw [pow_add, mul_assoc, ← mul_comm x, e]
    exact I.mul_mem_left _ y.2

[Geno Racklin Asher]

Thanks!

[Kevin Buzzard]

I hope you'll be PRing the result @Geno Racklin Asher !

[Geno Racklin Asher]

Yes, my plan is to try and formalise a couple more basic results from Stacks, namely that (locally) noetherian schemes are quasi-separated and have (locally) noetherian underlying topological spaces; but yes it would be great to get as much of that as possible PR'd into mathlib!

[Geno Racklin Asher]

Now PR'd at #13972!