bump to nightly-2023-05-21-18

mathlib commit leanprover-community/mathlib@33c67ae

Mathbin/AlgebraicGeometry/AffineScheme.lean

@@ -162,20 +162,20 @@ def Scheme.affineOpens (X : Scheme) : Set (Opens X.carrier) :=
   { U : Opens X.carrier | IsAffineOpen U }
 #align algebraic_geometry.Scheme.affine_opens AlgebraicGeometry.Scheme.affineOpens
 
-theorem range_isAffineOpen_of_open_immersion {X Y : Scheme} [IsAffine X] (f : X ⟶ Y)
+theorem rangeIsAffineOpenOfOpenImmersion {X Y : Scheme} [IsAffine X] (f : X ⟶ Y)
     [H : IsOpenImmersion f] : IsAffineOpen f.opensRange :=
   by
   refine' is_affine_of_iso (is_open_immersion.iso_of_range_eq f (Y.of_restrict _) _).inv
   exact subtype.range_coe.symm
   infer_instance
-#align algebraic_geometry.range_is_affine_open_of_open_immersion AlgebraicGeometry.range_isAffineOpen_of_open_immersion
+#align algebraic_geometry.range_is_affine_open_of_open_immersion AlgebraicGeometry.rangeIsAffineOpenOfOpenImmersion
 
-theorem top_isAffineOpen (X : Scheme) [IsAffine X] : IsAffineOpen (⊤ : Opens X.carrier) :=
+theorem topIsAffineOpen (X : Scheme) [IsAffine X] : IsAffineOpen (⊤ : Opens X.carrier) :=
   by
   convert range_is_affine_open_of_open_immersion (𝟙 X)
   ext1
   exact set.range_id.symm
-#align algebraic_geometry.top_is_affine_open AlgebraicGeometry.top_isAffineOpen
+#align algebraic_geometry.top_is_affine_open AlgebraicGeometry.topIsAffineOpen
 
 instance Scheme.affineCover_isAffine (X : Scheme) (i : X.affineCover.J) :
     IsAffine (X.affineCover.obj i) :=
@@ -245,20 +245,19 @@ theorem IsAffineOpen.isCompact {X : Scheme} {U : Opens X.carrier} (hU : IsAffine
   exact Set.image_univ
 #align algebraic_geometry.is_affine_open.is_compact AlgebraicGeometry.IsAffineOpen.isCompact
 
-theorem IsAffineOpen.image_isOpenImmersion {X Y : Scheme} {U : Opens X.carrier}
-    (hU : IsAffineOpen U) (f : X ⟶ Y) [H : IsOpenImmersion f] :
-    IsAffineOpen (f.opensFunctor.obj U) :=
+theorem IsAffineOpen.imageIsOpenImmersion {X Y : Scheme} {U : Opens X.carrier} (hU : IsAffineOpen U)
+    (f : X ⟶ Y) [H : IsOpenImmersion f] : IsAffineOpen (f.opensFunctor.obj U) :=
   by
   haveI : is_affine _ := hU
   convert range_is_affine_open_of_open_immersion (X.of_restrict U.open_embedding ≫ f)
   ext1
   exact Set.image_eq_range _ _
-#align algebraic_geometry.is_affine_open.image_is_open_immersion AlgebraicGeometry.IsAffineOpen.image_isOpenImmersion
+#align algebraic_geometry.is_affine_open.image_is_open_immersion AlgebraicGeometry.IsAffineOpen.imageIsOpenImmersion
 
 theorem isAffineOpen_iff_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f]
     (U : Opens X.carrier) : IsAffineOpen (H.openFunctor.obj U) ↔ IsAffineOpen U :=
   by
-  refine' ⟨fun hU => @is_affine_of_iso _ _ hU, fun hU => hU.image_isOpenImmersion f⟩
+  refine' ⟨fun hU => @is_affine_of_iso _ _ hU, fun hU => hU.imageIsOpenImmersion f⟩
   refine' (is_open_immersion.iso_of_range_eq (X.of_restrict _ ≫ f) (Y.of_restrict _) _).Hom
   · rw [Scheme.comp_val_base, coe_comp, Set.range_comp]
     dsimp [opens.inclusion]
@@ -268,7 +267,7 @@ theorem isAffineOpen_iff_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : Is
 #align algebraic_geometry.is_affine_open_iff_of_is_open_immersion AlgebraicGeometry.isAffineOpen_iff_of_isOpenImmersion
 
 instance Scheme.quasi_compact_of_affine (X : Scheme) [IsAffine X] : CompactSpace X.carrier :=
-  ⟨(top_isAffineOpen X).IsCompact⟩
+  ⟨(topIsAffineOpen X).IsCompact⟩
 #align algebraic_geometry.Scheme.quasi_compact_of_affine AlgebraicGeometry.Scheme.quasi_compact_of_affine
 
 theorem IsAffineOpen.fromSpec_base_preimage {X : Scheme} {U : Opens X.carrier}
@@ -336,7 +335,7 @@ theorem IsAffineOpen.fromSpec_app_eq {X : Scheme} {U : Opens X.carrier} (hU : Is
   by rw [← hU.Spec_Γ_identity_hom_app_from_Spec, iso.inv_hom_id_app_assoc]
 #align algebraic_geometry.is_affine_open.from_Spec_app_eq AlgebraicGeometry.IsAffineOpen.fromSpec_app_eq
 
-theorem IsAffineOpen.basicOpen_is_affine {X : Scheme} {U : Opens X.carrier} (hU : IsAffineOpen U)
+theorem IsAffineOpen.basicOpenIsAffine {X : Scheme} {U : Opens X.carrier} (hU : IsAffineOpen U)
     (f : X.Presheaf.obj (op U)) : IsAffineOpen (X.basicOpen f) :=
   by
   convert range_is_affine_open_of_open_immersion
@@ -371,9 +370,9 @@ theorem IsAffineOpen.basicOpen_is_affine {X : Scheme} {U : Opens X.carrier} (hU
   congr 2
   rw [iso.eq_inv_comp]
   erw [hU.Spec_Γ_identity_hom_app_from_Spec]
-#align algebraic_geometry.is_affine_open.basic_open_is_affine AlgebraicGeometry.IsAffineOpen.basicOpen_is_affine
+#align algebraic_geometry.is_affine_open.basic_open_is_affine AlgebraicGeometry.IsAffineOpen.basicOpenIsAffine
 
-theorem IsAffineOpen.map_restrict_basicOpen {X : Scheme} (r : X.Presheaf.obj (op ⊤))
+theorem IsAffineOpen.mapRestrictBasicOpen {X : Scheme} (r : X.Presheaf.obj (op ⊤))
     {U : Opens X.carrier} (hU : IsAffineOpen U) :
     IsAffineOpen ((Opens.map (X.of_restrict (X.basicOpen r).OpenEmbedding).1.base).obj U) :=
   by
@@ -384,7 +383,7 @@ theorem IsAffineOpen.map_restrict_basicOpen {X : Scheme} (r : X.Presheaf.obj (op
   erw [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 _
-#align algebraic_geometry.is_affine_open.map_restrict_basic_open AlgebraicGeometry.IsAffineOpen.map_restrict_basicOpen
+#align algebraic_geometry.is_affine_open.map_restrict_basic_open AlgebraicGeometry.IsAffineOpen.mapRestrictBasicOpen
 
 theorem Scheme.map_prime_spectrum_basicOpen_of_affine (X : Scheme) [IsAffine X]
     (f : Scheme.Γ.obj (op X)) :
@@ -519,7 +518,7 @@ theorem is_localization_basicOpen {X : Scheme} {U : Opens X.carrier} (hU : IsAff
 
 instance {X : Scheme} [IsAffine X] (r : X.Presheaf.obj (op ⊤)) :
     IsLocalization.Away r (X.Presheaf.obj (op <| X.basicOpen r)) :=
-  is_localization_basicOpen (top_isAffineOpen X) r
+  is_localization_basicOpen (topIsAffineOpen X) r
 
 theorem is_localization_of_eq_basicOpen {X : Scheme} {U V : Opens X.carrier} (i : V ⟶ U)
     (hU : IsAffineOpen U) (r : X.Presheaf.obj (op U)) (e : V = X.basicOpen r) :
@@ -536,7 +535,7 @@ instance ΓRestrictAlgebra {X : Scheme} {Y : TopCat} {f : Y ⟶ X.carrier} (hf :
 
 instance Γ_restrict_is_localization (X : Scheme.{u}) [IsAffine X] (r : Scheme.Γ.obj (op X)) :
     IsLocalization.Away r (Scheme.Γ.obj (op <| X.restrict (X.basicOpen r).OpenEmbedding)) :=
-  is_localization_of_eq_basicOpen _ (top_isAffineOpen X) r (Opens.openEmbedding_obj_top _)
+  is_localization_of_eq_basicOpen _ (topIsAffineOpen X) r (Opens.openEmbedding_obj_top _)
 #align algebraic_geometry.Γ_restrict_is_localization AlgebraicGeometry.Γ_restrict_is_localization
 
 theorem basicOpen_basicOpen_is_basicOpen {X : Scheme} {U : Opens X.carrier} (hU : IsAffineOpen U)
@@ -673,7 +672,7 @@ theorem IsAffineOpen.is_localization_stalk {X : Scheme} {U : Opens X.carrier} (h
 @[simps]
 def Scheme.affineBasicOpen (X : Scheme) {U : X.affineOpens} (f : X.Presheaf.obj <| op U) :
     X.affineOpens :=
-  ⟨X.basicOpen f, U.Prop.basicOpen_is_affine f⟩
+  ⟨X.basicOpen f, U.Prop.basicOpenIsAffine f⟩
 #align algebraic_geometry.Scheme.affine_basic_open AlgebraicGeometry.Scheme.affineBasicOpen
 
 @[simp]

Mathbin/AlgebraicGeometry/Gluing.lean

@@ -438,7 +438,7 @@ instance : Epi 𝒰.fromGlued.val.base :=
   exact h
 
 instance fromGlued_open_immersion : IsOpenImmersion 𝒰.fromGlued :=
-  SheafedSpace.IsOpenImmersion.of_stalk_iso _ 𝒰.fromGlued_openEmbedding
+  SheafedSpace.IsOpenImmersion.ofStalkIso _ 𝒰.fromGlued_openEmbedding
 #align algebraic_geometry.Scheme.open_cover.from_glued_open_immersion AlgebraicGeometry.Scheme.OpenCover.fromGlued_open_immersion
 
 instance : IsIso 𝒰.fromGlued :=

Mathbin/AlgebraicGeometry/Limits.lean

@@ -139,12 +139,12 @@ instance initial_isEmpty : IsEmpty (⊥_ Scheme).carrier :=
   ⟨fun x => ((initial.to Scheme.empty : _).1.base x).elim⟩
 #align algebraic_geometry.initial_is_empty AlgebraicGeometry.initial_isEmpty
 
-theorem bot_isAffineOpen (X : Scheme) : IsAffineOpen (⊥ : Opens X.carrier) :=
+theorem botIsAffineOpen (X : Scheme) : IsAffineOpen (⊥ : Opens X.carrier) :=
   by
   convert range_is_affine_open_of_open_immersion (initial.to X)
   ext
   exact (false_iff_iff _).mpr fun x => isEmptyElim (show (⊥_ Scheme).carrier from x.some)
-#align algebraic_geometry.bot_is_affine_open AlgebraicGeometry.bot_isAffineOpen
+#align algebraic_geometry.bot_is_affine_open AlgebraicGeometry.botIsAffineOpen
 
 instance : HasStrictInitialObjects Scheme :=
   hasStrictInitialObjects_of_initial_is_strict fun A f => by infer_instance

Mathbin/AlgebraicGeometry/Morphisms/Basic.lean

@@ -129,11 +129,11 @@ def targetAffineLocally (P : AffineTargetMorphismProperty) : MorphismProperty Sc
   fun {X Y : Scheme} (f : X ⟶ Y) => ∀ U : Y.affineOpens, @P (f ∣_ U) U.Prop
 #align algebraic_geometry.target_affine_locally AlgebraicGeometry.targetAffineLocally
 
-theorem IsAffineOpen.map_isIso {X Y : Scheme} {U : Opens Y.carrier} (hU : IsAffineOpen U)
-    (f : X ⟶ Y) [IsIso f] : IsAffineOpen ((Opens.map f.1.base).obj U) :=
+theorem IsAffineOpen.mapIsIso {X Y : Scheme} {U : Opens Y.carrier} (hU : IsAffineOpen U) (f : X ⟶ Y)
+    [IsIso f] : IsAffineOpen ((Opens.map f.1.base).obj U) :=
   haveI : is_affine _ := hU
   is_affine_of_iso (f ∣_ U)
-#align algebraic_geometry.is_affine_open.map_is_iso AlgebraicGeometry.IsAffineOpen.map_isIso
+#align algebraic_geometry.is_affine_open.map_is_iso AlgebraicGeometry.IsAffineOpen.mapIsIso
 
 theorem targetAffineLocally_respectsIso {P : AffineTargetMorphismProperty}
     (hP : P.toProperty.RespectsIso) : (targetAffineLocally P).RespectsIso :=
@@ -162,11 +162,11 @@ structure AffineTargetMorphismProperty.IsLocal (P : AffineTargetMorphismProperty
   RespectsIso : P.toProperty.RespectsIso
   toBasicOpen :
     ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (r : Y.Presheaf.obj <| op ⊤),
-      P f → @P (f ∣_ Y.basic_open r) ((top_is_affine_open Y).basicOpen_is_affine _)
+      P f → @P (f ∣_ Y.basic_open r) ((top_is_affine_open Y).basicOpenIsAffine _)
   ofBasicOpenCover :
     ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (s : Finset (Y.Presheaf.obj <| op ⊤))
       (hs : Ideal.span (s : Set (Y.Presheaf.obj <| op ⊤)) = ⊤),
-      (∀ r : s, @P (f ∣_ Y.basic_open r.1) ((top_is_affine_open Y).basicOpen_is_affine _)) → P f
+      (∀ r : s, @P (f ∣_ Y.basic_open r.1) ((top_is_affine_open Y).basicOpenIsAffine _)) → P f
 #align algebraic_geometry.affine_target_morphism_property.is_local AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal
 
 theorem targetAffineLocallyOfOpenCover {P : AffineTargetMorphismProperty} (hP : P.IsLocal)
@@ -277,7 +277,7 @@ theorem AffineTargetMorphismProperty.isLocalOfOpenCoverImply (P : AffineTargetMo
   refine' ⟨hP, _, _⟩
   · introv h
     skip
-    haveI : is_affine _ := (top_is_affine_open Y).basicOpen_is_affine r
+    haveI : is_affine _ := (top_is_affine_open Y).basicOpenIsAffine r
     delta morphism_restrict
     rw [affine_cancel_left_is_iso hP]
     refine' @H f ⟨Scheme.open_cover_of_is_iso (𝟙 Y), _, _⟩ (Y.of_restrict _) _inst _
@@ -294,10 +294,10 @@ theorem AffineTargetMorphismProperty.isLocalOfOpenCoverImply (P : AffineTargetMo
     rwa [← category.comp_id pullback.snd, ← pullback.condition, affine_cancel_left_is_iso hP] at
       this
     · intro i
-      exact (top_is_affine_open Y).basicOpen_is_affine _
+      exact (top_is_affine_open Y).basicOpenIsAffine _
     · rintro (i : s)
       specialize hs' i
-      haveI : is_affine _ := (top_is_affine_open Y).basicOpen_is_affine i.1
+      haveI : is_affine _ := (top_is_affine_open Y).basicOpenIsAffine i.1
       delta morphism_restrict at hs'
       rwa [affine_cancel_left_is_iso hP] at hs'
 #align algebraic_geometry.affine_target_morphism_property.is_local_of_open_cover_imply AlgebraicGeometry.AffineTargetMorphismProperty.isLocalOfOpenCoverImply

Mathbin/AlgebraicGeometry/Morphisms/QuasiCompact.lean

@@ -91,7 +91,7 @@ theorem isCompact_open_iff_eq_basicOpen_union {X : Scheme} [IsAffine X] (U : Set
       ∃ s : Set (X.Presheaf.obj (op ⊤)),
         s.Finite ∧ U = ⋃ (i : X.Presheaf.obj (op ⊤)) (h : i ∈ s), X.basicOpen i :=
   (isBasis_basicOpen X).isCompact_open_iff_eq_finite_iUnion _
-    (fun i => ((top_isAffineOpen _).basicOpen_is_affine _).IsCompact) _
+    (fun i => ((topIsAffineOpen _).basicOpenIsAffine _).IsCompact) _
 #align algebraic_geometry.is_compact_open_iff_eq_basic_open_union AlgebraicGeometry.isCompact_open_iff_eq_basicOpen_union
 
 theorem quasiCompact_iff_forall_affine :

Mathbin/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

@@ -277,7 +277,7 @@ instance quasiSeparatedSpace_of_isAffine (X : Scheme) [IsAffine X] :
     intro i' hi'
     change IsCompact (X.basic_open i ⊓ X.basic_open i').1
     rw [← Scheme.basic_open_mul]
-    exact ((top_is_affine_open _).basicOpen_is_affine _).IsCompact
+    exact ((top_is_affine_open _).basicOpenIsAffine _).IsCompact
 #align algebraic_geometry.quasi_separated_space_of_is_affine AlgebraicGeometry.quasiSeparatedSpace_of_isAffine
 
 theorem IsAffineOpen.isQuasiSeparated {X : Scheme} {U : Opens X.carrier} (hU : IsAffineOpen U) :

Mathbin/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -217,7 +217,7 @@ theorem affineLocally_iff_affineOpens_le (hP : RingHom.RespectsIso @P) {X Y : Sc
       convert V.2
       infer_instance
   · intro H V
-    specialize H ⟨_, V.2.image_isOpenImmersion (X.of_restrict _)⟩ (Subtype.coe_image_subset _ _)
+    specialize H ⟨_, V.2.imageIsOpenImmersion (X.of_restrict _)⟩ (Subtype.coe_image_subset _ _)
     erw [← X.presheaf.map_comp]
     rw [← hP.cancel_right_is_iso _ (X.presheaf.map (eq_to_hom _)), category.assoc, ←
       X.presheaf.map_comp]
@@ -238,12 +238,12 @@ theorem scheme_restrict_basicOpen_of_localizationPreserves (h₁ : RingHom.Respe
               U.1.OpenEmbedding ≫
             f ∣_ Y.basicOpen r).op) :=
   by
-  specialize H ⟨_, U.2.image_isOpenImmersion (X.of_restrict _)⟩
+  specialize H ⟨_, U.2.imageIsOpenImmersion (X.of_restrict _)⟩
   convert(h₁.of_restrict_morphism_restrict_iff _ _ _ _ _).mpr _ using 1
   pick_goal 5
   · exact h₂.away r H
   · infer_instance
-  · exact U.2.image_isOpenImmersion _
+  · exact U.2.imageIsOpenImmersion _
   · ext1
     exact (Set.preimage_image_eq _ Subtype.coe_injective).symm
 #align algebraic_geometry.Scheme_restrict_basic_open_of_localization_preserves AlgebraicGeometry.scheme_restrict_basicOpen_of_localizationPreserves
@@ -272,7 +272,7 @@ theorem sourceAffineLocallyIsLocal (h₁ : RingHom.RespectsIso @P)
       intro V hV
       rw [Scheme.preimage_basic_open] at hV
       subst hV
-      exact U.2.map_restrict_basicOpen (Scheme.Γ.map f.op r.1)
+      exact U.2.mapRestrictBasicOpen (Scheme.Γ.map f.op r.1)
 #align algebraic_geometry.source_affine_locally_is_local AlgebraicGeometry.sourceAffineLocallyIsLocal
 
 variable {P} (hP : RingHom.PropertyIsLocal @P)