V(I) /\ V(J) = V(I+J)

Stream: Is there code for X?

[Alexandra Foster]

There's a classic proposition in algebraic geometry, that the vanishing set V(I + J) of the ideal I + J for ideals I, J is equal to V(I) intersect V(J). Is this anywhere in mathlib? I've been slowly tinkering at it myself and the way I wrote it was like:

import data.mv_polynomial.basic
import data.set.basic
import data.fintype.basic
import algebra.ring.basic
import algebra.field
import algebra.module.submodule
import ring_theory.ideal.basic
import ring_theory.nullstellensatz

noncomputable theory

variables (σ : Type) [fintype σ]
variables (k : Type) [field k]

lemma ideal_addition_variety_intersection
  (I : ideal (mv_polynomial σ k))
  (J : ideal (mv_polynomial σ k)):
  mv_polynomial.zero_locus (I + J)
  = (mv_polynomial.zero_locus I)
    ∩ (mv_polynomial.zero_locus J)

(I used mv_polynomial.zero_locus from ring_theory.nullstellensatz, which, if this result isn't already in mathlib, might make sense as a place to put it..?)

[Johan Commelin]

See https://github.com/leanprover-community/mathlib/blob/master/src/algebraic_geometry/prime_spectrum.lean#L269L271

[Johan Commelin]

The rest of that file also contains a bunch of similar lemmas

[Johan Commelin]

This is in the context of the prime spectrum of a ring, not in the sense of "classical" algebraic geometry in $K^n$.

[Alexandra Foster]

That's great regardless, thanks!

[Kevin Buzzard]

Here's a documented proof, modulo ideal.mem_add, which I couldn't find! Is it there? Edit: it's mem_sup plus definitional abuse. Eew.

import ring_theory.nullstellensatz

noncomputable theory

variables (σ : Type) [fintype σ]
variables (k : Type) [field k]

lemma ideal.mem_add {R : Type*} [semiring R] {I J : ideal R} {f : R} :
  f ∈ I + J ↔ ∃ (g ∈ I) (h ∈ J), g + h = f :=
submodule.mem_sup

lemma ideal_addition_variety_intersection (I : ideal (mv_polynomial σ k))
  (J : ideal (mv_polynomial σ k)) :
  mv_polynomial.zero_locus (I + J) = (mv_polynomial.zero_locus I) ∩ (mv_polynomial.zero_locus J) :=
begin
  -- extensionality: two sets are equal iff they have the same elements
  ext P,
  -- ↔ can be broken down into → and ←
  split,
  { -- one way: assume P ∈ V(I+J)
    intro hP,
    -- need to prove P ∈ V(I) ∧ P ∈ V(J)
    split,
    { -- want P ∈ V(I+J) → P ∈ V(I). But we know V sends ⊆ to ⊇
      refine mv_polynomial.zero_locus_anti_mono _ hP,
      -- so now it suffices to prove I ≤ I + J
      exact le_sup_left },
    { -- essentially same proof the other way
      refine mv_polynomial.zero_locus_anti_mono _ hP,
      exact le_sup_right } },
  { -- Other way: assume P ∈ V(I) and P ∈ V(J)
    rintro ⟨hPI, hPJ⟩,
    -- assume f ∈ I + J
    intros f hf,
    -- write f as g + h with g ∈ I and h ∈ J
    rw ideal.mem_add at hf,
    rcases hf with ⟨g, hg, h, hh, rfl⟩,
    -- evaluation is additive
    rw ring_hom.map_add,
    -- but eval P g = 0 and eval P h = 0
    rw [hPI g hg, hPJ h hh],
    -- and now it's easy
    simp }
end

[Kevin Buzzard]

Re: mem_add -- it's mem_sup! I've edited.

[Kevin Buzzard]

Bonus: commenting out [fintype σ] we see the proof still works :D

[Alexandra Foster]

wow..! I was working away at it myself but I appreciate this solution. linear_algebra.basic is a great discovery, and I am impressed but not surprised that the proof of mem_sup in there is so long. I've been thinking, it's a very interesting choice to have sup be a more basic notion than sum

[Adam Topaz]

@Alexandra Foster the reason we use sup is because ideals in a commutative ring form a lattice, in the sense of docs#lattice and the sum of ideals corresponds to the sup in this lattice.

[Adam Topaz]

You will find other instances in mathlib as well. For example, the sup of two subgroups A and B of a given group G is the subgroup generated by A and B, and again the collection of all subgroups form a lattice.

[Heather Macbeth]

Incidentally, this lemma should join mathlib, right? (Maybe in the ring_theory.nullstellensatz file under the name mv_polynomial.zero_locus_sup.)

[Adam Topaz]

Yes it probably should be in mathlib, in one form or another... It might be worth it to give a full definition of the Zariski topology on an algebraic set

[Adam Topaz]

(and compare with the Zariski topology of the prime spectrum that we already have)