chore(AlgebraicGeometry/AffineScheme): rename isAffine_of_isIso to IsAffine.of_isIso (#23475)

This is useful for anonymous dot notation.

From Toric

Author: YaelDillies

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -113,9 +113,11 @@ instance (R : CommRingCatᵒᵖ) : IsAffine (Scheme.Spec.obj R) :=
 instance isAffine_Spec (R : CommRingCat) : IsAffine (Spec R) :=
   AlgebraicGeometry.isAffine_affineScheme ⟨_, Scheme.Spec.obj_mem_essImage (op R)⟩
 
-theorem isAffine_of_isIso {X Y : Scheme} (f : X ⟶ Y) [IsIso f] [h : IsAffine Y] : IsAffine X := by
+theorem IsAffine.of_isIso {X Y : Scheme} (f : X ⟶ Y) [IsIso f] [h : IsAffine Y] : IsAffine X := by
   rw [← mem_Spec_essImage] at h ⊢; exact Functor.essImage.ofIso (asIso f).symm h
 
+@[deprecated (since := "2025-03-31")] alias isAffine_of_isIso := IsAffine.of_isIso
+
 /-- If `f : X ⟶ Y` is a morphism between affine schemes, the corresponding arrow is isomorphic
 to the arrow of the morphism on prime spectra induced by the map on global sections. -/
 noncomputable
@@ -221,7 +223,7 @@ instance {Y : Scheme.{u}} (U : Y.affineOpens) : IsAffine U :=
 
 theorem isAffineOpen_opensRange {X Y : Scheme} [IsAffine X] (f : X ⟶ Y)
     [H : IsOpenImmersion f] : IsAffineOpen (Scheme.Hom.opensRange f) := by
-  refine isAffine_of_isIso (IsOpenImmersion.isoOfRangeEq f (Y.ofRestrict _) ?_).inv
+  refine .of_isIso (IsOpenImmersion.isoOfRangeEq f (Y.ofRestrict _) ?_).inv
   exact Subtype.range_val.symm
 
 theorem isAffineOpen_top (X : Scheme) [IsAffine X] : IsAffineOpen (⊤ : X.Opens) := by
@@ -444,19 +446,19 @@ theorem image_of_isOpenImmersion (f : X ⟶ Y) [H : IsOpenImmersion f] :
 theorem preimage_of_isIso {U : Y.Opens} (hU : IsAffineOpen U) (f : X ⟶ Y) [IsIso f] :
     IsAffineOpen (f ⁻¹ᵁ U) :=
   haveI : IsAffine _ := hU
-  isAffine_of_isIso (f ∣_ U)
+  .of_isIso (f ∣_ U)
 
 theorem _root_.AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion
     (f : AlgebraicGeometry.Scheme.Hom X Y) [H : IsOpenImmersion f] {U : X.Opens} :
-    IsAffineOpen (f ''ᵁ U) ↔ IsAffineOpen U := by
-  refine ⟨fun hU => @isAffine_of_isIso _ _
-    (IsOpenImmersion.isoOfRangeEq (X.ofRestrict U.isOpenEmbedding ≫ f) (Y.ofRestrict _) ?_).hom
-      ?_ hU, fun hU => hU.image_of_isOpenImmersion f⟩
-  · rw [Scheme.comp_base, TopCat.coe_comp, Set.range_comp]
+    IsAffineOpen (f ''ᵁ U) ↔ IsAffineOpen U where
+  mp hU := by
+    refine .of_isIso (IsOpenImmersion.isoOfRangeEq (X.ofRestrict U.isOpenEmbedding ≫ f)
+      (Y.ofRestrict _) ?_).hom (h := hU)
+    rw [Scheme.comp_base, TopCat.coe_comp, Set.range_comp]
     dsimp [Opens.coe_inclusion', Scheme.restrict]
     rw [Subtype.range_coe, Subtype.range_coe]
     rfl
-  · infer_instance
+  mpr hU := hU.image_of_isOpenImmersion f
 
 /-- The affine open sets of an open subscheme corresponds to
 the affine open sets containing in the image. -/

Mathlib/AlgebraicGeometry/AffineSpace.lean

@@ -233,7 +233,7 @@ lemma isoOfIsAffine_inv_over [IsAffine S] :
     (isoOfIsAffine n S).inv ≫ 𝔸(n; S) ↘ S = Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv :=
   pullback.lift_fst _ _ _
 
-instance [IsAffine S] : IsAffine 𝔸(n; S) := isAffine_of_isIso (isoOfIsAffine n S).hom
+instance [IsAffine S] : IsAffine 𝔸(n; S) := .of_isIso (isoOfIsAffine n S).hom
 
 variable (n) in
 /-- The affine space over an affine base is isomorphic to the spectrum of the polynomial ring. -/

Mathlib/AlgebraicGeometry/Limits.lean

@@ -49,7 +49,7 @@ instance : HasTerminal Scheme :=
   hasTerminal_of_hasTerminal_of_preservesLimit Scheme.Spec
 
 instance : IsAffine (⊤_ Scheme.{u}) :=
-  isAffine_of_isIso (PreservesTerminal.iso Scheme.Spec).inv
+  .of_isIso (PreservesTerminal.iso Scheme.Spec).inv
 
 instance : HasFiniteLimits Scheme :=
   hasFiniteLimits_of_hasTerminal_and_pullbacks
@@ -116,7 +116,7 @@ noncomputable def specPunitIsInitial : IsInitial (Spec (.of PUnit.{u+1})) :=
   emptyIsInitial.ofIso (asIso <| emptyIsInitial.to _)
 
 instance (priority := 100) isAffine_of_isEmpty {X : Scheme} [IsEmpty X] : IsAffine X :=
-  isAffine_of_isIso (inv (emptyIsInitial.to X) ≫ emptyIsInitial.to (Spec (.of PUnit)))
+  .of_isIso (inv (emptyIsInitial.to X) ≫ emptyIsInitial.to (Spec (.of PUnit)))
 
 instance : HasInitial Scheme.{u} :=
   hasInitial_of_unique ∅
@@ -627,10 +627,10 @@ instance [Finite ι] (R : ι → CommRingCat.{u}) : IsIso (sigmaSpec R) := by
   infer_instance
 
 instance [Finite ι] [∀ i, IsAffine (f i)] : IsAffine (∐ f) :=
-  isAffine_of_isIso ((Sigma.mapIso (fun i ↦ (f i).isoSpec)).hom ≫ sigmaSpec _)
+  .of_isIso ((Sigma.mapIso (fun i ↦ (f i).isoSpec)).hom ≫ sigmaSpec _)
 
 instance [IsAffine X] [IsAffine Y] : IsAffine (X ⨿ Y) :=
-  isAffine_of_isIso ((coprod.mapIso X.isoSpec Y.isoSpec).hom ≫ coprodSpec _ _)
+  .of_isIso ((coprod.mapIso X.isoSpec Y.isoSpec).hom ≫ coprodSpec _ _)
 
 end Coproduct
 

Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

@@ -149,7 +149,7 @@ instance : HasAffineProperty @IsAffineHom fun X _ _ _ ↦ IsAffine X where
     · apply AffineTargetMorphismProperty.respectsIso_mk
       · rintro X Y Z e _ _ H
         have : IsAffine _ := H
-        exact isAffine_of_isIso e.hom
+        exact .of_isIso e.hom
       · exact fun _ _ _ ↦ id
     · intro X Y _ f r H
       have : IsAffine X := H

Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean

@@ -51,9 +51,9 @@ lemma affineAnd_respectsIso (hP : RingHom.RespectsIso Q) :
     (affineAnd Q).toProperty.RespectsIso := by
   refine RespectsIso.mk _ ?_ ?_
   · intro X Y Z e f ⟨hZ, ⟨hY, hf⟩⟩
-    simpa [hP.cancel_right_isIso, isAffine_of_isIso e.hom]
+    simpa [hP.cancel_right_isIso, IsAffine.of_isIso e.hom]
   · intro X Y Z e f ⟨hZ, hf⟩
-    simpa [AffineTargetMorphismProperty.toProperty, isAffine_of_isIso e.inv, hP.cancel_left_isIso]
+    simpa [AffineTargetMorphismProperty.toProperty, IsAffine.of_isIso e.inv, hP.cancel_left_isIso]
 
 /-- `affineAnd P` is local if `P` is local on the (algebraic) source. -/
 lemma affineAnd_isLocal (hPi : RingHom.RespectsIso Q) (hQl : RingHom.LocalizationAwayPreserves Q)

Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

@@ -362,18 +362,18 @@ theorem arrow_mk_iso_iff
     (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso]
     {X Y X' Y' : Scheme} {f : X ⟶ Y} {f' : X' ⟶ Y'}
     (e : Arrow.mk f ≅ Arrow.mk f') {h : IsAffine Y} :
-    letI : IsAffine Y' := isAffine_of_isIso (Y := Y) e.inv.right
+    letI : IsAffine Y' := .of_isIso (Y := Y) e.inv.right
     P f ↔ P f' := by
   rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.arrow_mk_iso_iff e]
 
 theorem respectsIso_mk {P : AffineTargetMorphismProperty}
     (h₁ : ∀ {X Y Z} (e : X ≅ Y) (f : Y ⟶ Z) [IsAffine Z], P f → P (e.hom ≫ f))
     (h₂ : ∀ {X Y Z} (e : Y ≅ Z) (f : X ⟶ Y) [IsAffine Y],
-      P f → @P _ _ (f ≫ e.hom) (isAffine_of_isIso e.inv)) :
+      P f → @P _ _ (f ≫ e.hom) (.of_isIso e.inv)) :
     P.toProperty.RespectsIso := by
   apply MorphismProperty.RespectsIso.mk
   · rintro X Y Z e f ⟨a, h⟩; exact ⟨a, h₁ e f h⟩
-  · rintro X Y Z e f ⟨a, h⟩; exact ⟨isAffine_of_isIso e.inv, h₂ e f h⟩
+  · rintro X Y Z e f ⟨a, h⟩; exact ⟨.of_isIso e.inv, h₂ e f h⟩
 
 instance respectsIso_of
     (P : MorphismProperty Scheme) [P.RespectsIso] :

Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

@@ -247,7 +247,7 @@ theorem isAffine_surjective_of_isAffine [IsClosedImmersion f] :
   haveI := IsClosedImmersion.of_comp_isClosedImmersion (affineTargetImageFactorization f)
     (affineTargetImageInclusion f)
   haveI := isIso_of_injective_of_isAffine (affineTargetImageFactorization_app_injective f)
-  exact ⟨isAffine_of_isIso (affineTargetImageFactorization f),
+  exact ⟨.of_isIso (affineTargetImageFactorization f),
     (ConcreteCategory.bijective_of_isIso
       ((affineTargetImageFactorization f).appTop)).surjective.comp <|
       affineTargetImageInclusion_app_surjective f⟩

Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean

@@ -40,7 +40,7 @@ instance : HasAffineProperty (isomorphisms Scheme) fun X _ f _ ↦ IsAffine X 
   convert HasAffineProperty.of_isLocalAtTarget (isomorphisms Scheme) with X Y f hY
   exact ⟨fun ⟨_, _⟩ ↦ (arrow_mk_iso_iff (isomorphisms _) (arrowIsoSpecΓOfIsAffine f)).mpr
     (inferInstanceAs (IsIso (Spec.map (f.appTop)))),
-    fun (_ : IsIso f) ↦ ⟨isAffine_of_isIso f, inferInstance⟩⟩
+    fun (_ : IsIso f) ↦ ⟨.of_isIso f, inferInstance⟩⟩
 
 instance : IsLocalAtTarget (monomorphisms Scheme) :=
   diagonal_isomorphisms (C := Scheme).symm ▸ inferInstance

Mathlib/AlgebraicGeometry/Pullbacks.lean

@@ -451,7 +451,7 @@ instance : HasPullbacks Scheme :=
 instance isAffine_of_isAffine_isAffine_isAffine {X Y Z : Scheme}
     (f : X ⟶ Z) (g : Y ⟶ Z) [IsAffine X] [IsAffine Y] [IsAffine Z] :
     IsAffine (pullback f g) :=
-  isAffine_of_isIso
+  .of_isIso
     (pullback.map f g (Spec.map (Γ.map f.op)) (Spec.map (Γ.map g.op))
         X.toSpecΓ Y.toSpecΓ Z.toSpecΓ
         (Scheme.toSpecΓ_naturality f) (Scheme.toSpecΓ_naturality g) ≫