feat(algebraic_geometry): Intersection of affine open can be covered …

…by common basic opens (#11649)




Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/algebraic_geometry/AffineScheme.lean

@@ -6,6 +6,7 @@ Authors: Andrew Yang
 import algebraic_geometry.Gamma_Spec_adjunction
 import algebraic_geometry.open_immersion
 import category_theory.limits.opposites
+import ring_theory.localization.inv_submonoid
 
 /-!
 # Affine schemes
@@ -309,6 +310,115 @@ begin
     exact congr_arg subtype.val (X.map_prime_spectrum_basic_open_of_affine x).symm }
 end
 
+lemma is_affine_open.exists_basic_open_subset {X : Scheme} {U : opens X.carrier}
+  (hU : is_affine_open U) {V : opens X.carrier} (x : V) (h : ↑x ∈ U) :
+  ∃ f : X.presheaf.obj (op U), X.basic_open f ⊆ V ∧ ↑x ∈ X.basic_open f :=
+begin
+  haveI : is_affine _ := hU,
+  obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, h₁, h₂⟩ := (is_basis_basic_open (X.restrict U.open_embedding))
+    .exists_subset_of_mem_open _ ((opens.map U.inclusion).obj V).prop,
+  swap, exact ⟨x, h⟩,
+  have : U.open_embedding.is_open_map.functor.obj ((X.restrict U.open_embedding).basic_open r)
+    = X.basic_open (X.presheaf.map (eq_to_hom U.open_embedding_obj_top.symm).op r),
+  { refine (is_open_immersion.image_basic_open (X.of_restrict U.open_embedding) r).trans _,
+    erw ← Scheme.basic_open_res_eq _ _ (eq_to_hom U.open_embedding_obj_top).op,
+    rw [← comp_apply, ← category_theory.functor.map_comp, ← op_comp, eq_to_hom_trans,
+      eq_to_hom_refl, op_id, category_theory.functor.map_id],
+    erw PresheafedSpace.is_open_immersion.of_restrict_inv_app,
+    congr },
+  use X.presheaf.map (eq_to_hom U.open_embedding_obj_top.symm).op r,
+  rw ← this,
+  exact ⟨set.image_subset_iff.mpr h₂, set.mem_image_of_mem _ h₁⟩,
+  exact x.prop,
+end
+
+instance {X : Scheme} {U : opens X.carrier} (f : X.presheaf.obj (op U)) :
+  algebra (X.presheaf.obj (op U)) (X.presheaf.obj (op $ X.basic_open f)) :=
+(X.presheaf.map (hom_of_le $ RingedSpace.basic_open_subset _ f : _ ⟶ U).op).to_algebra
+
+lemma is_affine_open.opens_map_from_Spec_basic_open {X : Scheme} {U : opens X.carrier}
+  (hU : is_affine_open U) (f : X.presheaf.obj (op U)) :
+  (opens.map hU.from_Spec.val.base).obj (X.basic_open f) =
+    RingedSpace.basic_open _ (Spec_Γ_identity.inv.app (X.presheaf.obj $ op U) f) :=
+begin
+  erw LocallyRingedSpace.preimage_basic_open,
+  refine eq.trans _ (RingedSpace.basic_open_res_eq (Scheme.Spec.obj $ op $ X.presheaf.obj (op U))
+    .to_LocallyRingedSpace.to_RingedSpace (eq_to_hom hU.from_Spec_base_preimage).op _),
+  congr,
+  rw ← comp_apply,
+  congr,
+  erw ← hU.Spec_Γ_identity_hom_app_from_Spec,
+  rw iso.inv_hom_id_app_assoc,
+end
+
+/-- The canonical map `Γ(𝒪ₓ, D(f)) ⟶ Γ(Spec 𝒪ₓ(U), D(Spec_Γ_identity.inv f))`
+This is an isomorphism, as witnessed by an `is_iso` instance. -/
+def basic_open_sections_to_affine {X : Scheme} {U : opens X.carrier} (hU : is_affine_open U)
+  (f : X.presheaf.obj (op U)) : X.presheaf.obj (op $ X.basic_open f) ⟶
+    (Scheme.Spec.obj $ op $ X.presheaf.obj (op U)).presheaf.obj
+      (op $ Scheme.basic_open _ $ Spec_Γ_identity.inv.app (X.presheaf.obj (op U)) f) :=
+hU.from_Spec.1.c.app (op $ X.basic_open f) ≫ (Scheme.Spec.obj $ op $ X.presheaf.obj (op U))
+  .presheaf.map (eq_to_hom $ (hU.opens_map_from_Spec_basic_open f).symm).op
+
+instance {X : Scheme} {U : opens X.carrier} (hU : is_affine_open U)
+  (f : X.presheaf.obj (op U)) : is_iso (basic_open_sections_to_affine hU f) :=
+begin
+  delta basic_open_sections_to_affine,
+  apply_with is_iso.comp_is_iso { instances := ff },
+  { apply PresheafedSpace.is_open_immersion.is_iso_of_subset,
+    rw hU.from_Spec_range,
+    exact RingedSpace.basic_open_subset _ _ },
+  apply_instance
+end
+.
+lemma is_localization_basic_open {X : Scheme} {U : opens X.carrier} (hU : is_affine_open U)
+  (f : X.presheaf.obj (op U)) :
+  is_localization.away f (X.presheaf.obj (op $ X.basic_open f)) :=
+begin
+  apply (is_localization.is_localization_iff_of_ring_equiv (submonoid.powers f)
+    (as_iso $ basic_open_sections_to_affine hU f ≫ (Scheme.Spec.obj _).presheaf.map
+      (eq_to_hom (basic_open_eq_of_affine _).symm).op).CommRing_iso_to_ring_equiv).mpr,
+  convert structure_sheaf.is_localization.to_basic_open _ f,
+  change _ ≫ (basic_open_sections_to_affine hU f ≫ _) = _,
+  delta basic_open_sections_to_affine,
+  erw ring_hom.algebra_map_to_algebra,
+  simp only [Scheme.comp_val_c_app, category.assoc],
+  erw hU.from_Spec.val.c.naturality_assoc,
+  rw hU.from_Spec_app_eq,
+  dsimp,
+  simp only [category.assoc, ← functor.map_comp, ← op_comp],
+  apply structure_sheaf.to_open_res,
+end
+
+lemma basic_open_basic_open_is_basic_open {X : Scheme} {U : opens X.carrier}
+  (hU : is_affine_open U) (f : X.presheaf.obj (op U)) (g : X.presheaf.obj (op $ X.basic_open f)) :
+  ∃ f' : X.presheaf.obj (op U), X.basic_open f' = X.basic_open g :=
+begin
+  haveI := is_localization_basic_open hU f,
+  obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := is_localization.surj' (submonoid.powers f) g,
+  use f * x,
+  rw [algebra.smul_def, Scheme.basic_open_mul, Scheme.basic_open_mul],
+  erw Scheme.basic_open_res,
+  refine (inf_eq_left.mpr _).symm,
+  convert inf_le_left using 1,
+  apply Scheme.basic_open_of_is_unit,
+  apply submonoid.left_inv_le_is_unit _ (is_localization.to_inv_submonoid (submonoid.powers f)
+    (X.presheaf.obj (op $ X.basic_open f)) _).prop
+end
+
+lemma exists_basic_open_subset_affine_inter {X : Scheme} {U V : opens X.carrier}
+  (hU : is_affine_open U) (hV : is_affine_open V) (x : X.carrier) (hx : x ∈ U ∩ V) :
+  ∃ (f : X.presheaf.obj $ op U) (g : X.presheaf.obj $ op V),
+    X.basic_open f = X.basic_open g ∧ x ∈ X.basic_open f :=
+begin
+  obtain ⟨f, hf₁, hf₂⟩ := hU.exists_basic_open_subset ⟨x, hx.2⟩ hx.1,
+  obtain ⟨g, hg₁, hg₂⟩ := hV.exists_basic_open_subset ⟨x, hf₂⟩ hx.2,
+  obtain ⟨f', hf'⟩ := basic_open_basic_open_is_basic_open hU f
+    (X.presheaf.map (hom_of_le hf₁ : _ ⟶ V).op g),
+  replace hf' := (hf'.trans (RingedSpace.basic_open_res _ _ _)).trans (inf_eq_right.mpr hg₁),
+  exact ⟨f', g, hf', hf'.symm ▸ hg₂⟩
+end
+
 /-- The prime ideal of `𝒪ₓ(U)` corresponding to a point `x : U`. -/
 noncomputable
 def is_affine_open.prime_ideal_of {X : Scheme} {U : opens X.carrier}

src/algebraic_geometry/open_immersion.lean

@@ -205,7 +205,7 @@ begin
   simp [← functor.map_comp]
 end
 
-@[simp, reassoc] lemma inv_app_app (U : opens X) :
+@[simp, reassoc, elementwise] lemma inv_app_app (U : opens X) :
   H.inv_app U ≫ f.c.app (op (H.open_functor.obj U)) =
     X.presheaf.map (eq_to_hom (by simp [opens.map, set.preimage_image_eq _ H.base_open.inj])) :=
 by rw [inv_app, category.assoc, is_iso.inv_hom_id, category.comp_id]
@@ -255,6 +255,18 @@ instance of_restrict {X : Top} (Y : PresheafedSpace C) {f : X ⟶ Y.carrier}
       apply_instance }
   end }
 
+@[elementwise, simp]
+lemma of_restrict_inv_app {C : Type*} [category C] (X : PresheafedSpace C) {Y : Top}
+  {f : Y ⟶ Top.of X.carrier}
+  (h : open_embedding f) (U : opens (X.restrict h).carrier) :
+  (PresheafedSpace.is_open_immersion.of_restrict X h).inv_app U = 𝟙 _ :=
+begin
+  delta PresheafedSpace.is_open_immersion.inv_app,
+  rw [is_iso.comp_inv_eq, category.id_comp],
+  change X.presheaf.map _ = X.presheaf.map _,
+  congr
+end
+
 /-- An open immersion is an iso if the underlying continuous map is epi. -/
 lemma to_iso (f : X ⟶ Y) [h : is_open_immersion f] [h' : epi f.base] : is_iso f :=
 begin
@@ -604,6 +616,16 @@ by unfreezingI { cases X, delta to_LocallyRingedSpace, simp }
 
 end to_LocallyRingedSpace
 
+lemma is_iso_of_subset {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y)
+  [H : PresheafedSpace.is_open_immersion f] (U : opens Y.carrier)
+  (hU : (U : set Y.carrier) ⊆ set.range f.base) : is_iso (f.c.app $ op U) :=
+begin
+  have : U = H.base_open.is_open_map.functor.obj ((opens.map f.base).obj U),
+  { ext1,
+    exact (set.inter_eq_left_iff_subset.mpr hU).symm.trans set.image_preimage_eq_inter_range.symm },
+  convert PresheafedSpace.is_open_immersion.c_iso ((opens.map f.base).obj U),
+end
+
 end PresheafedSpace.is_open_immersion
 
 namespace SheafedSpace.is_open_immersion
@@ -1577,6 +1599,23 @@ LocallyRingedSpace.is_open_immersion.lift_uniq f g H' l hl
   hom_inv_id' := by { rw ← cancel_mono f, simp },
   inv_hom_id' := by { rw ← cancel_mono g, simp } }
 
+lemma image_basic_open {X Y : Scheme} (f : X ⟶ Y) [H : is_open_immersion f]
+  {U : opens X.carrier} (r : X.presheaf.obj (op U)) :
+  H.base_open.is_open_map.functor.obj (X.basic_open r) = Y.basic_open (H.inv_app U r) :=
+begin
+  have e := Scheme.preimage_basic_open f (H.inv_app U r),
+  rw [PresheafedSpace.is_open_immersion.inv_app_app_apply, Scheme.basic_open_res,
+    opens.inter_eq, inf_eq_right.mpr _] at e,
+  rw ← e,
+  ext1,
+  refine set.image_preimage_eq_inter_range.trans _,
+  erw set.inter_eq_left_iff_subset,
+  refine set.subset.trans (Scheme.basic_open_subset _ _) (set.image_subset_range _ _),
+  refine le_trans (Scheme.basic_open_subset _ _) (le_of_eq _),
+  ext1,
+  exact (set.preimage_image_eq _ H.base_open.inj).symm
+end
+
 end is_open_immersion
 
 /-- The functor taking open subsets of `X` to open subschemes of `X`. -/