refactor(algebraic_geometry/*): Tidy up simp lemmas regarding `basic_…

…open`s. (#17014)




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

src/algebraic_geometry/AffineScheme.lean

@@ -315,7 +315,7 @@ begin
   have : hU.from_Spec.val.base '' (hU.from_Spec.val.base ⁻¹' (X.basic_open f : set X.carrier)) =
     (X.basic_open f : set X.carrier),
   { rw [set.image_preimage_eq_inter_range, set.inter_eq_left_iff_subset, hU.from_Spec_range],
-    exact Scheme.basic_open_subset _ _ },
+    exact Scheme.basic_open_le _ _ },
   rw [Scheme.hom.opens_range_coe, Scheme.comp_val_base, ← this, coe_comp, set.range_comp],
   congr' 1,
   refine (congr_arg coe $ Scheme.preimage_basic_open hU.from_Spec f).trans _,
@@ -345,7 +345,7 @@ begin
     (X.of_restrict (X.basic_open r).open_embedding) _).mp,
   delta PresheafedSpace.is_open_immersion.open_functor,
   dsimp,
-  rw [opens.functor_obj_map_obj, opens.open_embedding_obj_top, inf_comm, ← opens.inter_eq,
+  rw [opens.functor_obj_map_obj, opens.open_embedding_obj_top, inf_comm,
     ← Scheme.basic_open_res _ _ (hom_of_le le_top).op],
   exact hU.basic_open_is_affine _,
 end
@@ -385,9 +385,9 @@ 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}
+lemma is_affine_open.exists_basic_open_le {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 :=
+  ∃ 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))
@@ -409,7 +409,7 @@ 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
+(X.presheaf.map (hom_of_le $ RingedSpace.basic_open_le _ 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)) :
@@ -442,7 +442,7 @@ begin
   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 _ _ },
+    exact RingedSpace.basic_open_le _ _ },
   apply_instance
 end
 .
@@ -499,13 +499,13 @@ begin
     (X.presheaf.obj (op $ X.basic_open f)) _).prop
 end
 
-lemma exists_basic_open_subset_affine_inter {X : Scheme} {U V : opens X.carrier}
+lemma exists_basic_open_le_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₁, hf₂⟩ := hU.exists_basic_open_le ⟨x, hx.2⟩ hx.1,
+  obtain ⟨g, hg₁, hg₂⟩ := hV.exists_basic_open_le ⟨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₁),
@@ -648,7 +648,7 @@ begin
     simp only [set.Union_subset_iff, set_coe.forall, opens.supr_def, set.le_eq_subset,
       subtype.coe_mk],
     intros x hx,
-    exact X.basic_open_subset x },
+    exact X.basic_open_le x },
   { simp only [opens.supr_def, subtype.coe_mk, set.preimage_Union, subtype.val_eq_coe],
     congr' 3,
     { ext1 x,
@@ -668,7 +668,7 @@ begin
   refine ⟨λ h, le_antisymm h _, le_of_eq⟩,
   simp only [supr_le_iff, set_coe.forall],
   intros x hx,
-  exact X.basic_open_subset x
+  exact X.basic_open_le x
 end
 
 /--
@@ -698,7 +698,7 @@ begin
     have : ↑x ∈ (set.univ : set X.carrier) := trivial,
     rw ← hS at this,
     obtain ⟨W, hW⟩ := set.mem_Union.mp this,
-    obtain ⟨f, g, e, hf⟩ := exists_basic_open_subset_affine_inter V.prop W.1.prop x ⟨x.prop, hW⟩,
+    obtain ⟨f, g, e, hf⟩ := exists_basic_open_le_affine_inter V.prop W.1.prop x ⟨x.prop, hW⟩,
     refine ⟨f, hf, _⟩,
     convert hP₁ _ g (hS' W) using 1,
     ext1,

src/algebraic_geometry/Scheme.lean

@@ -212,7 +212,7 @@ RingedSpace.mem_basic_open _ f ⟨x, trivial⟩
 
 @[simp]
 lemma basic_open_res (i : op U ⟶ op V) :
-  X.basic_open (X.presheaf.map i f) = V ∩ X.basic_open f :=
+  X.basic_open (X.presheaf.map i f) = V ⊓ X.basic_open f :=
 RingedSpace.basic_open_res _ i f
 
 -- This should fire before `basic_open_res`.
@@ -221,8 +221,8 @@ lemma basic_open_res_eq (i : op U ⟶ op V) [is_iso i] :
   X.basic_open (X.presheaf.map i f) = X.basic_open f :=
 RingedSpace.basic_open_res_eq _ i f
 
-lemma basic_open_subset : X.basic_open f ⊆ U :=
-RingedSpace.basic_open_subset _ _
+lemma basic_open_le : X.basic_open f ≤ U :=
+RingedSpace.basic_open_le _ _
 
 @[simp]
 lemma preimage_basic_open {X Y : Scheme} (f : X ⟶ Y) {U : opens Y.carrier}
@@ -232,7 +232,7 @@ lemma preimage_basic_open {X Y : Scheme} (f : X ⟶ Y) {U : opens Y.carrier}
 LocallyRingedSpace.preimage_basic_open f r
 
 @[simp]
-lemma basic_open_zero (U : opens X.carrier) : X.basic_open (0 : X.presheaf.obj $ op U) = ∅ :=
+lemma basic_open_zero (U : opens X.carrier) : X.basic_open (0 : X.presheaf.obj $ op U) = ⊥ :=
 LocallyRingedSpace.basic_open_zero _ U
 
 @[simp]

src/algebraic_geometry/locally_ringed_space.lean

@@ -247,10 +247,10 @@ end
 
 -- This actually holds for all ringed spaces with nontrivial stalks.
 @[simp] lemma basic_open_zero (X : LocallyRingedSpace) (U : opens X.carrier) :
-  X.to_RingedSpace.basic_open (0 : X.presheaf.obj $ op U) = ∅ :=
+  X.to_RingedSpace.basic_open (0 : X.presheaf.obj $ op U) = ⊥ :=
 begin
   ext,
-  simp only [set.mem_empty_iff_false, topological_space.opens.empty_eq,
+  simp only [set.mem_empty_iff_false,
     topological_space.opens.mem_coe, opens.coe_bot, iff_false, RingedSpace.basic_open,
     is_unit_zero_iff, set.mem_set_of_eq, map_zero],
   rintro ⟨⟨y, _⟩, h, e⟩,

src/algebraic_geometry/locally_ringed_space/has_colimits.lean

@@ -170,7 +170,7 @@ begin
       SheafedSpace.congr_app (coequalizer.condition f.1 g.1), comp_apply],
     erw X.to_RingedSpace.basic_open_res,
     apply inf_eq_right.mpr,
-    refine (RingedSpace.basic_open_subset _ _).trans _,
+    refine (RingedSpace.basic_open_le _ _).trans _,
     rw coequalizer.condition f.1 g.1,
     exact λ _ h, h }
 end
@@ -204,7 +204,7 @@ begin
     image_basic_open_image_open f g U s,
   have VleU :
     (⟨((coequalizer.π f.val g.val).base) '' V.val, V_open⟩ : topological_space.opens _) ≤ U,
-  { exact set.image_subset_iff.mpr (Y.to_RingedSpace.basic_open_subset _) },
+  { exact set.image_subset_iff.mpr (Y.to_RingedSpace.basic_open_le _) },
   have hxV : x ∈ V := ⟨⟨_, hU⟩, ha, rfl⟩,
 
   erw ← (coequalizer f.val g.val).presheaf.germ_res_apply (hom_of_le VleU)

src/algebraic_geometry/morphisms/quasi_compact.lean

@@ -124,7 +124,7 @@ begin
   obtain ⟨s, hs, e⟩ := (is_compact_open_iff_eq_finset_affine_union _).mp ⟨hU, U.prop⟩,
   let g : s → X.affine_opens,
   { intro V,
-    use V.1 ∩ X.basic_open f,
+    use V.1 ⊓ X.basic_open f,
     have : V.1.1 ⟶ U,
     { apply hom_of_le, change _ ⊆ (U : set X.carrier), rw e,
       convert @set.subset_Union₂ _ _ _ (λ (U : X.affine_opens) (h : U ∈ s), ↑U) V V.prop using 1,
@@ -133,7 +133,7 @@ begin
     exact is_affine_open.basic_open_is_affine V.1.prop _ },
   haveI : finite s := hs.to_subtype,
   refine ⟨set.range g, set.finite_range g, _⟩,
-  refine (set.inter_eq_right_iff_subset.mpr (RingedSpace.basic_open_subset _ _)).symm.trans _,
+  refine (set.inter_eq_right_iff_subset.mpr (RingedSpace.basic_open_le _ _)).symm.trans _,
   rw [e, set.Union₂_inter],
   apply le_antisymm; apply set.Union₂_subset,
   { intros i hi,

src/algebraic_geometry/morphisms/ring_hom_properties.lean

@@ -98,8 +98,7 @@ begin
     rw [opens.open_embedding_obj_top, opens.functor_obj_map_obj],
     convert (X.basic_open_res (Scheme.Γ.map f.op r) (hom_of_le le_top).op).symm using 1,
     rw [opens.open_embedding_obj_top, opens.open_embedding_obj_top, inf_comm,
-      Scheme.Γ_map_op, ← Scheme.preimage_basic_open],
-    refl },
+      Scheme.Γ_map_op, ← Scheme.preimage_basic_open] },
   { apply is_localization.ring_hom_ext (submonoid.powers r) _,
     swap, { exact algebraic_geometry.Γ_restrict_is_localization Y r },
     rw [is_localization.away.map, is_localization.map_comp, ring_hom.algebra_map_to_algebra,
@@ -332,7 +331,7 @@ begin
     { refine X.presheaf.map
         (@hom_of_le _ _ ((is_open_map.functor _).obj _) ((is_open_map.functor _).obj _) _).op,
       rw [unop_op, unop_op, opens.open_embedding_obj_top, opens.open_embedding_obj_top],
-      exact X.basic_open_subset _ },
+      exact X.basic_open_le _ },
     { rw [op_comp, op_comp, functor.map_comp, functor.map_comp],
       refine (eq.trans _ (category.assoc _ _ _).symm : _),
       congr' 1,

src/algebraic_geometry/open_immersion.lean

@@ -1648,13 +1648,13 @@ lemma image_basic_open {X Y : Scheme} (f : X ⟶ Y) [H : is_open_immersion f]
 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,
+    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 _),
+  refine set.subset.trans (Scheme.basic_open_le _ _) (set.image_subset_range _ _),
+  refine le_trans (Scheme.basic_open_le _ _) (le_of_eq _),
   ext1,
   exact (set.preimage_image_eq _ H.base_open.inj).symm
 end
@@ -1964,7 +1964,7 @@ begin
   erw ← e,
   ext1, dsimp [opens.map, opens.inclusion],
   rw [set.image_preimage_eq_inter_range, set.inter_eq_left_iff_subset, subtype.range_coe],
-  exact Y.basic_open_subset r
+  exact Y.basic_open_le r
 end
 
 instance {X Y : Scheme} (f : X ⟶ Y) (U : opens Y.carrier) [is_open_immersion f] :

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -756,7 +756,7 @@ lemma basic_open_eq_bot_iff (f : R) :
   basic_open f = ⊥ ↔ is_nilpotent f :=
 begin
   rw [← subtype.coe_injective.eq_iff, basic_open_eq_zero_locus_compl],
-  simp only [set.eq_univ_iff_forall, topological_space.opens.empty_eq, set.singleton_subset_iff,
+  simp only [set.eq_univ_iff_forall, set.singleton_subset_iff,
     topological_space.opens.coe_bot, nilpotent_iff_mem_prime, set.compl_empty_iff, mem_zero_locus,
     set_like.mem_coe],
   exact subtype.forall,

src/algebraic_geometry/properties.lean

@@ -166,8 +166,8 @@ begin
   apply h₁,
 end
 
-lemma eq_zero_of_basic_open_empty {X : Scheme} [hX : is_reduced X] {U : opens X.carrier}
-  (s : X.presheaf.obj (op U)) (hs : X.basic_open s = ∅) :
+lemma eq_zero_of_basic_open_eq_bot {X : Scheme} [hX : is_reduced X] {U : opens X.carrier}
+  (s : X.presheaf.obj (op U)) (hs : X.basic_open s = ⊥) :
   s = 0 :=
 begin
   apply Top.presheaf.section_ext X.sheaf U,
@@ -178,7 +178,7 @@ begin
     obtain ⟨V, hx, i, H⟩ := hx x,
     unfreezingI { specialize H (X.presheaf.map i.op s) },
     erw Scheme.basic_open_res at H,
-    rw [hs, ← subtype.coe_injective.eq_iff, opens.empty_eq, opens.inter_eq, inf_bot_eq] at H,
+    rw [hs, ← subtype.coe_injective.eq_iff, inf_bot_eq] at H,
     specialize H rfl ⟨x, hx⟩,
     erw Top.presheaf.germ_res_apply at H,
     exact H },
@@ -209,7 +209,7 @@ lemma basic_open_eq_bot_iff {X : Scheme} [is_reduced X] {U : opens X.carrier}
   (s : X.presheaf.obj $ op U) :
   X.basic_open s = ⊥ ↔ s = 0 :=
 begin
-  refine ⟨eq_zero_of_basic_open_empty s, _⟩,
+  refine ⟨eq_zero_of_basic_open_eq_bot s, _⟩,
   rintro rfl,
   simp,
 end

src/algebraic_geometry/ringed_space.lean

@@ -127,12 +127,12 @@ lemma mem_top_basic_open (f : X.presheaf.obj (op ⊤)) (x : X) :
   x ∈ X.basic_open f ↔ is_unit (X.presheaf.germ ⟨x, show x ∈ (⊤ : opens X), by trivial⟩ f) :=
 mem_basic_open X f ⟨x, _⟩
 
-lemma basic_open_subset {U : opens X} (f : X.presheaf.obj (op U)) : X.basic_open f ⊆ U :=
+lemma basic_open_le {U : opens X} (f : X.presheaf.obj (op U)) : X.basic_open f ≤ U :=
 by { rintros _ ⟨x, hx, rfl⟩, exact x.2 }
 
 /-- The restriction of a section `f` to the basic open of `f` is a unit. -/
 lemma is_unit_res_basic_open {U : opens X} (f : X.presheaf.obj (op U)) :
-  is_unit (X.presheaf.map (@hom_of_le (opens X) _ _ _ (X.basic_open_subset f)).op f) :=
+  is_unit (X.presheaf.map (@hom_of_le (opens X) _ _ _ (X.basic_open_le f)).op f) :=
 begin
   apply is_unit_of_is_unit_germ,
   rintro ⟨_, ⟨x, hx, rfl⟩⟩,
@@ -142,7 +142,7 @@ begin
 end
 
 @[simp] lemma basic_open_res {U V : (opens X)ᵒᵖ} (i : U ⟶ V) (f : X.presheaf.obj U) :
-  @basic_open X (unop V) (X.presheaf.map i f) = (unop V) ∩ @basic_open X (unop U) f :=
+  @basic_open X (unop V) (X.presheaf.map i f) = (unop V) ⊓ @basic_open X (unop U) f :=
 begin
   induction U using opposite.rec,
   induction V using opposite.rec,
@@ -185,7 +185,7 @@ lemma basic_open_of_is_unit {U : opens X} {f : X.presheaf.obj (op U)} (hf : is_u
   X.basic_open f = U :=
 begin
   apply le_antisymm,
-  { exact X.basic_open_subset f },
+  { exact X.basic_open_le f },
   intros x hx,
   erw X.mem_basic_open f (⟨x, hx⟩ : U),
   exact ring_hom.is_unit_map _ hf