feat(algebraic_geometry): Qcqs lemma (#15996)

Co-authored-by: Andrew Yang <[email protected]>
Co-authored-by: Joël Riou <[email protected]>

Author: erdOne

docs/references.bib

@@ -1783,6 +1783,12 @@ @Book{            riehl2017
   url           = {http://www.math.jhu.edu/~eriehl/context.pdf}
 }
 
+@Misc{            RisingSea,
+  author        = "Vakil, Ravi",
+  title         = "{The Rising Sea: Foundations Of Algebraic Geometry Notes}",
+  url           = "https://math.stanford.edu/~vakil/216blog/"
+}
+
 @Book{            rudin2006real,
   title         = {Real and Complex Analysis},
   author        = {Rudin, Walter},

src/algebraic_geometry/AffineScheme.lean

@@ -679,7 +679,7 @@ Let `P` be a predicate on the affine open sets of `X` satisfying
 
 Then `P` holds for every affine open of `X`.
 
-This is also known as the **Affine communication lemma** in Vakil's "The rising sea". -/
+This is also known as the **Affine communication lemma** in [*The rising sea*][RisingSea]. -/
 @[elab_as_eliminator]
 lemma of_affine_open_cover {X : Scheme} (V : X.affine_opens) (S : set X.affine_opens)
   {P : X.affine_opens → Prop}

src/algebraic_geometry/morphisms/quasi_compact.lean

@@ -24,6 +24,8 @@ open category_theory category_theory.limits opposite topological_space
 
 universe u
 
+open_locale algebraic_geometry
+
 namespace algebraic_geometry
 
 variables {X Y : Scheme.{u}} (f : X ⟶ Y)
@@ -285,4 +287,54 @@ begin
     exact supr_insert }
 end
 
+lemma exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_affine_open (X : Scheme)
+  {U : opens X.carrier} (hU : is_affine_open U) (x f : X.presheaf.obj (op U))
+  (H : x |_ X.basic_open f = 0) :
+  ∃ n : ℕ, f ^ n * x = 0 :=
+begin
+  rw ← map_zero (X.presheaf.map (hom_of_le $ X.basic_open_le f : X.basic_open f ⟶ U).op) at H,
+  have := (is_localization_basic_open hU f).3,
+  obtain ⟨⟨_, n, rfl⟩, e⟩ := this.mp H,
+  exact ⟨n, by simpa [mul_comm x] using e⟩,
+end
+
+/-- If `x : Γ(X, U)` is zero on `D(f)` for some `f : Γ(X, U)`, and `U` is quasi-compact, then
+`f ^ n * x = 0` for some `n`. -/
+lemma exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_compact (X : Scheme)
+  {U : opens X.carrier} (hU : is_compact U.1) (x f : X.presheaf.obj (op U))
+  (H : x |_ X.basic_open f = 0) :
+  ∃ n : ℕ, f ^ n * x = 0 :=
+begin
+  obtain ⟨s, hs, e⟩ := (is_compact_open_iff_eq_finset_affine_union U.1).mp ⟨hU, U.2⟩,
+  replace e : U = supr (λ i : s, (i : opens X.carrier)),
+  { ext1, simpa using e },
+  have h₁ : ∀ i : s, i.1.1 ≤ U,
+  { intro i, change (i : opens X.carrier) ≤ U, rw e, exact le_supr _ _ },
+  have H' := λ (i : s), exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_affine_open X i.1.2
+    (X.presheaf.map (hom_of_le (h₁ i)).op x) (X.presheaf.map (hom_of_le (h₁ i)).op f) _,
+  swap,
+  { delta Top.presheaf.restrict_open Top.presheaf.restrict at H ⊢,
+    convert congr_arg (X.presheaf.map (hom_of_le _).op) H,
+    { simp only [← comp_apply, ← functor.map_comp], congr },
+    { rw map_zero },
+    { rw X.basic_open_res, exact set.inter_subset_right _ _ } },
+  choose n hn using H',
+  haveI := hs.to_subtype,
+  casesI nonempty_fintype s,
+  use finset.univ.sup n,
+  suffices : ∀ (i : s), X.presheaf.map (hom_of_le (h₁ i)).op (f ^ (finset.univ.sup n) * x) = 0,
+  { subst e,
+    apply X.sheaf.eq_of_locally_eq (λ (i : s), (i : opens X.carrier)),
+    intro i,
+    rw map_zero,
+    apply this },
+  intro i,
+  replace hn := congr_arg
+    (λ x, X.presheaf.map (hom_of_le (h₁ i)).op (f ^ (finset.univ.sup n - n i)) * x) (hn i),
+  dsimp at hn,
+  simp only [← map_mul, ← map_pow] at hn,
+  rwa [mul_zero, ← mul_assoc, ← pow_add, tsub_add_cancel_of_le] at hn,
+  apply finset.le_sup (finset.mem_univ i)
+end
+
 end algebraic_geometry

src/algebraic_geometry/morphisms/quasi_separated.lean

@@ -20,6 +20,10 @@ We show that a morphism is quasi-separated if the preimage of every affine open
 We also show that this property is local at the target,
 and is stable under compositions and base-changes.
 
+## Main result
+- `is_localization_basic_open_of_qcqs` (**Qcqs lemma**):
+  If `U` is qcqs, then `Γ(X, D(f)) ≃ Γ(X, U)_f` for every `f : Γ(X, U)`.
+
 -/
 
 noncomputable theory
@@ -28,6 +32,8 @@ open category_theory category_theory.limits opposite topological_space
 
 universe u
 
+open_locale algebraic_geometry
+
 namespace algebraic_geometry
 
 variables {X Y : Scheme.{u}} (f : X ⟶ Y)
@@ -274,4 +280,204 @@ begin
   { apply algebraic_geometry.quasi_separated_of_mono }
 end
 
+lemma exists_eq_pow_mul_of_is_affine_open (X : Scheme) (U : opens X.carrier) (hU : is_affine_open U)
+  (f : X.presheaf.obj (op U)) (x : X.presheaf.obj (op $ X.basic_open f)) :
+  ∃ (n : ℕ) (y : X.presheaf.obj (op U)),
+    y |_ X.basic_open f = (f |_ X.basic_open f) ^ n * x :=
+begin
+  have := (is_localization_basic_open hU f).2,
+  obtain ⟨⟨y, _, n, rfl⟩, d⟩ := this x,
+  use [n, y],
+  delta Top.presheaf.restrict_open Top.presheaf.restrict,
+  simpa [mul_comm x] using d.symm,
+end
+
+lemma exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux (X : Scheme)
+  (S : X.affine_opens) (U₁ U₂ : opens X.carrier)
+  {n₁ n₂ : ℕ} {y₁ : X.presheaf.obj (op U₁)}
+  {y₂ : X.presheaf.obj (op U₂)} {f : X.presheaf.obj (op $ U₁ ⊔ U₂)}
+  {x : X.presheaf.obj (op $ X.basic_open f)}
+  (h₁ : S.1 ≤ U₁) (h₂ : S.1 ≤ U₂)
+  (e₁ : X.presheaf.map (hom_of_le $ X.basic_open_le
+    (X.presheaf.map (hom_of_le le_sup_left).op f) : _ ⟶ U₁).op y₁ =
+      X.presheaf.map (hom_of_le (by { erw X.basic_open_res, exact inf_le_left })).op
+        (X.presheaf.map (hom_of_le le_sup_left).op f) ^ n₁ *
+      (X.presheaf.map (hom_of_le (by { erw X.basic_open_res, exact inf_le_right })).op) x)
+  (e₂ : X.presheaf.map (hom_of_le $ X.basic_open_le
+    (X.presheaf.map (hom_of_le le_sup_right).op f) : _ ⟶ U₂).op y₂ =
+      X.presheaf.map (hom_of_le (by { rw X.basic_open_res, exact inf_le_left })).op
+        (X.presheaf.map (hom_of_le le_sup_right).op f) ^ n₂ *
+      (X.presheaf.map (hom_of_le (by { rw X.basic_open_res, exact inf_le_right })).op) x) :
+  ∃ n : ℕ, X.presheaf.map (hom_of_le $ h₁).op
+    ((X.presheaf.map (hom_of_le le_sup_left).op f) ^ (n + n₂) * y₁) =
+    X.presheaf.map (hom_of_le $ h₂).op
+      ((X.presheaf.map (hom_of_le le_sup_right).op f) ^ (n + n₁) * y₂) :=
+begin
+  have := (is_localization_basic_open S.2
+    (X.presheaf.map (hom_of_le $ le_trans h₁ le_sup_left).op f)),
+  obtain ⟨⟨_, n, rfl⟩, e⟩ :=
+    (@is_localization.eq_iff_exists _ _ _ _ _ _ this (X.presheaf.map (hom_of_le $ h₁).op
+      ((X.presheaf.map (hom_of_le le_sup_left).op f) ^ n₂ * y₁))
+    (X.presheaf.map (hom_of_le $ h₂).op
+      ((X.presheaf.map (hom_of_le le_sup_right).op f) ^ n₁ * y₂))).mp _,
+  swap,
+  { simp only [map_pow, ring_hom.algebra_map_to_algebra, map_mul, ← comp_apply,
+      ← functor.map_comp, ← op_comp, hom_of_le_comp],
+    have h₃ : X.basic_open ((X.presheaf.map (hom_of_le (h₁.trans le_sup_left)).op) f) ≤ S.val,
+    { simpa only [X.basic_open_res] using inf_le_left, },
+    transitivity
+      X.presheaf.map (hom_of_le $ h₃.trans $ h₁.trans le_sup_left).op f ^ (n₂ + n₁) *
+      X.presheaf.map (hom_of_le $ (X.basic_open_res f _).trans_le inf_le_right).op x,
+    { rw [pow_add, mul_assoc], congr' 1,
+      convert congr_arg (X.presheaf.map (hom_of_le _).op) e₁,
+      { simp only [map_pow, map_mul, ← comp_apply, ← functor.map_comp, ← op_comp], congr },
+      { simp only [map_pow, map_mul, ← comp_apply, ← functor.map_comp, ← op_comp], congr },
+      { rw [X.basic_open_res, X.basic_open_res], rintros x ⟨H₁, H₂⟩, exact ⟨h₁ H₁, H₂⟩ } },
+    { rw [add_comm, pow_add, mul_assoc], congr' 1,
+      convert congr_arg (X.presheaf.map (hom_of_le _).op) e₂.symm,
+      { simp only [map_pow, map_mul, ← comp_apply, ← functor.map_comp, ← op_comp], congr },
+      { simp only [map_pow, map_mul, ← comp_apply, ← functor.map_comp, ← op_comp], congr },
+      { simp only [X.basic_open_res],
+        rintros x ⟨H₁, H₂⟩, exact ⟨h₂ H₁, H₂⟩ } } },
+  use n,
+  conv_lhs at e { rw mul_comm },
+  conv_rhs at e { rw mul_comm },
+  simp only [pow_add, map_pow, map_mul, ← comp_apply, ← mul_assoc,
+    ← functor.map_comp, subtype.coe_mk] at e ⊢,
+  convert e
+end
+
+lemma exists_eq_pow_mul_of_is_compact_of_is_quasi_separated (X : Scheme)
+  (U : opens X.carrier) (hU : is_compact U.1) (hU' : is_quasi_separated U.1)
+  (f : X.presheaf.obj (op U)) (x : X.presheaf.obj (op $ X.basic_open f)) :
+  ∃ (n : ℕ) (y : X.presheaf.obj (op U)), y |_ X.basic_open f = (f |_ X.basic_open f) ^ n * x :=
+begin
+  delta Top.presheaf.restrict_open Top.presheaf.restrict,
+  revert hU' f x,
+  apply compact_open_induction_on U hU,
+  { intros hU' f x,
+    use [0, f],
+    refine @@subsingleton.elim (CommRing.subsingleton_of_is_terminal
+      (X.sheaf.is_terminal_of_eq_empty _)) _ _,
+    erw eq_bot_iff,
+    exact X.basic_open_le f },
+  { -- Given `f : 𝒪(S ∪ U), x : 𝒪(X_f)`, we need to show that `f ^ n * x` is the restriction of
+    -- some `y : 𝒪(S ∪ U)` for some `n : ℕ`.
+    intros S hS U hU hSU f x,
+    -- We know that such `y₁, n₁` exists on `S` by the induction hypothesis.
+    obtain ⟨n₁, y₁, hy₁⟩ := hU (hSU.of_subset $ set.subset_union_left _ _)
+      (X.presheaf.map (hom_of_le le_sup_left).op f) (X.presheaf.map (hom_of_le _).op x),
+    swap, { rw X.basic_open_res, exact inf_le_right },
+    -- We know that such `y₂, n₂` exists on `U` since `U` is affine.
+    obtain ⟨n₂, y₂, hy₂⟩ := exists_eq_pow_mul_of_is_affine_open X _ U.2
+      (X.presheaf.map (hom_of_le le_sup_right).op f) (X.presheaf.map (hom_of_le _).op x),
+    delta Top.presheaf.restrict_open Top.presheaf.restrict at hy₂,
+    swap, { rw X.basic_open_res, exact inf_le_right },
+    -- Since `S ∪ U` is quasi-separated, `S ∩ U` can be covered by finite affine opens.
+    obtain ⟨s, hs', hs⟩ := (is_compact_open_iff_eq_finset_affine_union _).mp
+      ⟨hSU _ _ (set.subset_union_left _ _) S.2 hS
+        (set.subset_union_right _ _) U.1.2 U.2.is_compact, (S ⊓ U.1).2⟩,
+    haveI := hs'.to_subtype,
+    casesI nonempty_fintype s,
+    replace hs : S ⊓ U.1 = supr (λ i : s, (i : opens X.carrier)) := by { ext1, simpa using hs },
+    have hs₁ : ∀ i : s, i.1.1 ≤ S,
+    { intro i, change (i : opens X.carrier) ≤ S,
+      refine le_trans _ inf_le_left, use U.1, erw hs, exact le_supr _ _ },
+    have hs₂ : ∀ i : s, i.1.1 ≤ U.1,
+    { intro i, change (i : opens X.carrier) ≤ U,
+      refine le_trans _ inf_le_right, use S, erw hs, exact le_supr _ _ },
+    -- On each affine open in the intersection, we have `f ^ (n + n₂) * y₁ = f ^ (n + n₁) * y₂`
+    -- for some `n` since `f ^ n₂ * y₁ = f ^ (n₁ + n₂) * x = f ^ n₁ * y₂` on `X_f`.
+    have : ∀ i : s, ∃ n : ℕ,
+      X.presheaf.map (hom_of_le $ hs₁ i).op
+        ((X.presheaf.map (hom_of_le le_sup_left).op f) ^ (n + n₂) * y₁) =
+      X.presheaf.map (hom_of_le $ hs₂ i).op
+        ((X.presheaf.map (hom_of_le le_sup_right).op f) ^ (n + n₁) * y₂),
+    { intro i,
+      exact exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux X i.1 S U (hs₁ i) (hs₂ i)
+        hy₁ hy₂ },
+    choose n hn using this,
+    -- We can thus choose a big enough `n` such that `f ^ (n + n₂) * y₁ = f ^ (n + n₁) * y₂`
+    -- on `S ∩ U`.
+    have : X.presheaf.map (hom_of_le $ inf_le_left).op
+      ((X.presheaf.map (hom_of_le le_sup_left).op f) ^ (finset.univ.sup n + n₂) * y₁) =
+        X.presheaf.map (hom_of_le $ inf_le_right).op
+          ((X.presheaf.map (hom_of_le le_sup_right).op f) ^ (finset.univ.sup n + n₁) * y₂),
+    { fapply X.sheaf.eq_of_locally_eq' (λ i : s, i.1.1),
+      { refine λ i, hom_of_le _, erw hs, exact le_supr _ _ },
+      { exact le_of_eq hs },
+      { intro i,
+        replace hn := congr_arg (λ x, X.presheaf.map (hom_of_le
+          (le_trans (hs₁ i) le_sup_left)).op f ^ (finset.univ.sup n - n i) * x) (hn i),
+        dsimp only at hn,
+        delta Scheme.sheaf SheafedSpace.sheaf,
+        simp only [← map_pow, map_mul, ← comp_apply, ← functor.map_comp, ← op_comp, ← mul_assoc]
+          at hn ⊢,
+        erw [← map_mul, ← map_mul] at hn,
+        rw [← pow_add, ← pow_add, ← add_assoc, ← add_assoc, tsub_add_cancel_of_le] at hn,
+        convert hn,
+        exact finset.le_sup (finset.mem_univ _) } },
+    use finset.univ.sup n + n₁ + n₂,
+    -- By the sheaf condition, since `f ^ (n + n₂) * y₁ = f ^ (n + n₁) * y₂`, it can be glued into
+    -- the desired section on `S ∪ U`.
+    use (X.sheaf.obj_sup_iso_prod_eq_locus S U.1).inv ⟨⟨_ * _, _ * _⟩, this⟩,
+    refine X.sheaf.eq_of_locally_eq₂
+      (hom_of_le (_ : X.basic_open (X.presheaf.map (hom_of_le le_sup_left).op f) ≤ _))
+      (hom_of_le (_ : X.basic_open (X.presheaf.map (hom_of_le le_sup_right).op f) ≤ _)) _ _ _ _ _,
+    { rw X.basic_open_res, exact inf_le_right },
+    { rw X.basic_open_res, exact inf_le_right },
+    { rw [X.basic_open_res, X.basic_open_res],
+      erw ← inf_sup_right,
+      refine le_inf_iff.mpr ⟨X.basic_open_le f, le_of_eq rfl⟩ },
+    { convert congr_arg (X.presheaf.map (hom_of_le _).op)
+        (X.sheaf.obj_sup_iso_prod_eq_locus_inv_fst S U.1 ⟨⟨_ * _, _ * _⟩, this⟩) using 1,
+      { delta Scheme.sheaf SheafedSpace.sheaf,
+        simp only [← comp_apply (X.presheaf.map _) (X.presheaf.map _),
+          ← functor.map_comp, ← op_comp],
+        congr },
+      { delta Scheme.sheaf SheafedSpace.sheaf,
+        simp only [map_pow, map_mul, ← comp_apply, ← functor.map_comp, ← op_comp, mul_assoc,
+          pow_add], erw hy₁, congr' 1, rw [← mul_assoc, ← mul_assoc], congr' 1,
+        rw [mul_comm, ← comp_apply, ← functor.map_comp], congr } },
+    { convert congr_arg (X.presheaf.map (hom_of_le _).op)
+        (X.sheaf.obj_sup_iso_prod_eq_locus_inv_snd S U.1 ⟨⟨_ * _, _ * _⟩, this⟩) using 1,
+      { delta Scheme.sheaf SheafedSpace.sheaf,
+        simp only [← comp_apply (X.presheaf.map _) (X.presheaf.map _),
+          ← functor.map_comp, ← op_comp],
+        congr },
+      { delta Scheme.sheaf SheafedSpace.sheaf,
+        simp only [map_pow, map_mul, ← comp_apply, ← functor.map_comp, ← op_comp, mul_assoc,
+          pow_add], erw hy₂, rw [← comp_apply, ← functor.map_comp], congr } } }
+end
+
+/-- If `U` is qcqs, then `Γ(X, D(f)) ≃ Γ(X, U)_f` for every `f : Γ(X, U)`.
+This is known as the **Qcqs lemma** in [R. Vakil, *The rising sea*][RisingSea]. -/
+lemma is_localization_basic_open_of_qcqs {X : Scheme} {U : opens X.carrier}
+  (hU : is_compact U.1) (hU' : is_quasi_separated U.1)
+  (f : X.presheaf.obj (op U)) :
+  is_localization.away f (X.presheaf.obj (op $ X.basic_open f)) :=
+begin
+  constructor,
+  { rintro ⟨_, n, rfl⟩,
+    simp only [map_pow, subtype.coe_mk, ring_hom.algebra_map_to_algebra],
+    exact is_unit.pow _ (RingedSpace.is_unit_res_basic_open _ f), },
+  { intro z,
+    obtain ⟨n, y, e⟩ := exists_eq_pow_mul_of_is_compact_of_is_quasi_separated X U hU hU' f z,
+    refine ⟨⟨y, _, n, rfl⟩, _⟩,
+    simpa only [map_pow, subtype.coe_mk, ring_hom.algebra_map_to_algebra, mul_comm z]
+      using e.symm },
+  { intros x y,
+    rw [← sub_eq_zero, ← map_sub, ring_hom.algebra_map_to_algebra],
+    simp_rw [← @sub_eq_zero _ _ (x * _) (y * _), ← sub_mul],
+    generalize : x - y = z,
+    split,
+    { intro H,
+      obtain ⟨n, e⟩ := exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_compact X hU _ _ H,
+      refine ⟨⟨_, n, rfl⟩, _⟩,
+      simpa [mul_comm z] using e },
+    { rintro ⟨⟨_, n, rfl⟩, e : z * f ^ n = 0⟩,
+      rw [← ((RingedSpace.is_unit_res_basic_open _ f).pow n).mul_left_inj, zero_mul, ← map_pow,
+        ← map_mul, e, map_zero] } }
+end
+
 end algebraic_geometry