chore(AlgebraicGeometry/Smooth): rename IsSmooth to Smooth and IsEtale to Etale (leanprover-community#35028)

This way it matches `Algebra.Smooth` and `Algebra.Etale`. Also there is no possible confusion, because these are clearly adjectives.

Author: chrisflav

Mathlib/AlgebraicGeometry/Morphisms/Etale.lean

@@ -31,23 +31,25 @@ open CategoryTheory MorphismProperty Limits
 namespace AlgebraicGeometry
 
 /-- A morphism of schemes is étale if it is smooth of relative dimension zero. -/
-abbrev IsEtale {X Y : Scheme.{u}} (f : X ⟶ Y) := IsSmoothOfRelativeDimension 0 f
+abbrev Etale {X Y : Scheme.{u}} (f : X ⟶ Y) := SmoothOfRelativeDimension 0 f
 
-namespace IsEtale
+@[deprecated (since := "2026-02-09")] alias IsEtale := Etale
+
+namespace Etale
 
 variable {X Y : Scheme.{u}} (f : X ⟶ Y)
 
-instance [IsEtale f] : IsSmooth f :=
-  IsSmoothOfRelativeDimension.isSmooth 0 f
+instance [Etale f] : Smooth f :=
+  SmoothOfRelativeDimension.smooth 0 f
 
-instance : IsStableUnderBaseChange @IsEtale :=
-  isSmoothOfRelativeDimension_isStableUnderBaseChange 0
+instance : IsStableUnderBaseChange @Etale :=
+  smoothOfRelativeDimension_isStableUnderBaseChange 0
 
 open RingHom in
-instance (priority := 900) [IsEtale f] : FormallyUnramified f where
+instance (priority := 900) [Etale f] : FormallyUnramified f where
   formallyUnramified_appLE {U} hU {V} hV e := by
     have : Locally (IsStandardSmoothOfRelativeDimension 0) (f.appLE U V e).hom :=
-      HasRingHomProperty.appLE (P := @IsSmoothOfRelativeDimension 0) _
+      HasRingHomProperty.appLE (P := @SmoothOfRelativeDimension 0) _
         inferInstance ⟨U, hU⟩ ⟨V, hV⟩ _
     have : Locally RingHom.FormallyUnramified (f.appLE U V e).hom := by
       apply locally_of_locally _ this
@@ -59,37 +61,37 @@ instance (priority := 900) [IsEtale f] : FormallyUnramified f where
       FormallyUnramified.respectsIso FormallyUnramified.ofLocalizationSpanTarget]
 
 instance : MorphismProperty.HasOfPostcompProperty
-    @IsEtale (@LocallyOfFiniteType ⊓ @FormallyUnramified) := by
+    @Etale (@LocallyOfFiniteType ⊓ @FormallyUnramified) := by
   rw [MorphismProperty.hasOfPostcompProperty_iff_le_diagonal]
   intro X Y f ⟨hft, hfu⟩
-  exact inferInstanceAs <| IsEtale (pullback.diagonal f)
+  exact inferInstanceAs <| Etale (pullback.diagonal f)
 
 /-- If `f ≫ g` is étale and `g` unramified, then `f` is étale. -/
-lemma of_comp {Z : Scheme.{u}} (g : Y ⟶ Z) [IsEtale (f ≫ g)] [LocallyOfFiniteType g]
-    [FormallyUnramified g] : IsEtale f :=
+lemma of_comp {Z : Scheme.{u}} (g : Y ⟶ Z) [Etale (f ≫ g)] [LocallyOfFiniteType g]
+    [FormallyUnramified g] : Etale f :=
   of_postcomp _ (W' := @LocallyOfFiniteType ⊓ @FormallyUnramified) f g ⟨‹_›, ‹_›⟩ ‹_›
 
-instance : MorphismProperty.HasOfPostcompProperty @IsEtale @IsEtale := by
-  apply MorphismProperty.HasOfPostcompProperty.of_le (W := @IsEtale)
+instance : MorphismProperty.HasOfPostcompProperty @Etale @Etale := by
+  apply MorphismProperty.HasOfPostcompProperty.of_le (W := @Etale)
     (Q := (@LocallyOfFiniteType ⊓ @FormallyUnramified))
   intro X Y f hf
   constructor <;> infer_instance
 
-end IsEtale
+end Etale
 
 namespace Scheme
 
 /-- The category `Etale X` is the category of schemes étale over `X`. -/
-def Etale (X : Scheme.{u}) : Type _ := MorphismProperty.Over @IsEtale ⊤ X
+protected def Etale (X : Scheme.{u}) : Type _ := MorphismProperty.Over @Etale ⊤ X
 
 variable (X : Scheme.{u})
 
 instance : Category X.Etale :=
-  inferInstanceAs <| Category (MorphismProperty.Over @IsEtale ⊤ X)
+  inferInstanceAs <| Category (MorphismProperty.Over @Etale ⊤ X)
 
 /-- The forgetful functor from schemes étale over `X` to schemes over `X`. -/
 def Etale.forget : X.Etale ⥤ Over X :=
-  MorphismProperty.Over.forget @IsEtale ⊤ X
+  MorphismProperty.Over.forget @Etale ⊤ X
 
 /-- The forgetful functor from schemes étale over `X` to schemes over `X` is fully faithful. -/
 def Etale.forgetFullyFaithful : (Etale.forget X).FullyFaithful :=
@@ -101,7 +103,7 @@ instance : (Etale.forget X).Faithful :=
   inferInstanceAs <| (MorphismProperty.Comma.forget _ _ _ _ _).Faithful
 
 instance : HasPullbacks X.Etale := by
-  unfold Etale
+  unfold Scheme.Etale
   infer_instance
 
 end Scheme

Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

@@ -24,12 +24,12 @@ to the property of ring homomorphisms `Locally IsStandardSmooth`
 
 ## Implementation details
 
-- Our definition is equivalent to defining `IsSmooth` as the associated scheme morphism property of
+- Our definition is equivalent to defining `Smooth` as the associated scheme morphism property of
 the property of ring maps induced by `Algebra.Smooth`. The equivalence will follow from the
-equivalence of `Locally IsStandardSmooth` and `Algebra.IsSmooth`, but the latter is a (hard) TODO.
+equivalence of `Locally IsStandardSmooth` and `Algebra.Smooth`, but the latter is a (hard) TODO.
 
 The reason why we choose the definition via `IsStandardSmooth`, is because verifying that
-`Algebra.IsSmooth` is local in the sense of `RingHom.PropertyIsLocal` is a (hard) TODO.
+`Algebra.Smooth` is local in the sense of `RingHom.PropertyIsLocal` is a (hard) TODO.
 
 ## Notes
 
@@ -60,85 +60,99 @@ exists an affine open neighborhood `V` of `x` and an affine open neighborhood `U
 standard smooth.
 -/
 @[mk_iff]
-class IsSmooth : Prop where
+class Smooth : Prop where
   exists_isStandardSmooth : ∀ (x : X), ∃ (U : Y.affineOpens) (V : X.affineOpens) (_ : x ∈ V.1)
     (e : V.1 ≤ f ⁻¹ᵁ U.1), IsStandardSmooth (f.appLE U V e).hom
 
-/-- The property of scheme morphisms `IsSmooth` is associated with the ring
+@[deprecated (since := "2026-02-09")] alias IsSmooth := Smooth
+
+/-- The property of scheme morphisms `Smooth` is associated with the ring
 homomorphism property `Locally IsStandardSmooth`. -/
-instance : HasRingHomProperty @IsSmooth (Locally IsStandardSmooth) := by
+instance : HasRingHomProperty @Smooth (Locally IsStandardSmooth) := by
   apply HasRingHomProperty.locally_of_iff
   · exact isStandardSmooth_localizationPreserves.away
   · exact isStandardSmooth_stableUnderCompositionWithLocalizationAway
   · intro X Y f
-    rw [isSmooth_iff]
+    rw [smooth_iff]
 
 /-- Being smooth is stable under composition. -/
-instance : MorphismProperty.IsStableUnderComposition @IsSmooth :=
+instance : MorphismProperty.IsStableUnderComposition @Smooth :=
   HasRingHomProperty.stableUnderComposition <| locally_stableUnderComposition
     isStandardSmooth_respectsIso isStandardSmooth_localizationPreserves
       isStandardSmooth_stableUnderComposition
 
 /-- The composition of smooth morphisms is smooth. -/
-instance isSmooth_comp {Z : Scheme.{u}} (g : Y ⟶ Z) [IsSmooth f] [IsSmooth g] :
-    IsSmooth (f ≫ g) :=
-  MorphismProperty.comp_mem _ f g ‹IsSmooth f› ‹IsSmooth g›
+instance smooth_comp {Z : Scheme.{u}} (g : Y ⟶ Z) [Smooth f] [Smooth g] :
+    Smooth (f ≫ g) :=
+  MorphismProperty.comp_mem _ f g ‹Smooth f› ‹Smooth g›
 
 /-- Smooth of relative dimension `n` is stable under base change. -/
-lemma isSmooth_isStableUnderBaseChange : MorphismProperty.IsStableUnderBaseChange @IsSmooth :=
+lemma smooth_isStableUnderBaseChange : MorphismProperty.IsStableUnderBaseChange @Smooth :=
   HasRingHomProperty.isStableUnderBaseChange <| locally_isStableUnderBaseChange
     isStandardSmooth_respectsIso isStandardSmooth_isStableUnderBaseChange
 
+@[deprecated (since := "2026-02-09")]
+alias isSmooth_isStableUnderBaseChange := smooth_isStableUnderBaseChange
+
 /--
 A morphism of schemes `f : X ⟶ Y` is smooth of relative dimension `n` if for each `x : X` there
 exists an affine open neighborhood `V` of `x` and an affine open neighborhood `U` of
 `f.base x` with `V ≤ f ⁻¹ᵁ U` such that the induced map `Γ(Y, U) ⟶ Γ(X, V)` is
 standard smooth of relative dimension `n`.
 -/
 @[mk_iff]
-class IsSmoothOfRelativeDimension : Prop where
+class SmoothOfRelativeDimension : Prop where
   exists_isStandardSmoothOfRelativeDimension : ∀ (x : X), ∃ (U : Y.affineOpens)
     (V : X.affineOpens) (_ : x ∈ V.1) (e : V.1 ≤ f ⁻¹ᵁ U.1),
     IsStandardSmoothOfRelativeDimension n (f.appLE U V e).hom
 
+@[deprecated (since := "2026-02-09")] alias IsSmoothOfRelativeDimension := SmoothOfRelativeDimension
+
 /-- If `f` is smooth of any relative dimension, it is smooth. -/
-lemma IsSmoothOfRelativeDimension.isSmooth [IsSmoothOfRelativeDimension n f] : IsSmooth f where
+lemma SmoothOfRelativeDimension.smooth [SmoothOfRelativeDimension n f] : Smooth f where
   exists_isStandardSmooth x := by
     obtain ⟨U, V, hx, e, hf⟩ := exists_isStandardSmoothOfRelativeDimension (n := n) (f := f) x
     exact ⟨U, V, hx, e, hf.isStandardSmooth⟩
 
-/-- The property of scheme morphisms `IsSmoothOfRelativeDimension n` is associated with the ring
+@[deprecated (since := "2026-02-09")]
+alias IsSmoothOfRelativeDimension.isSmooth := SmoothOfRelativeDimension.smooth
+
+/-- The property of scheme morphisms `SmoothOfRelativeDimension n` is associated with the ring
 homomorphism property `Locally (IsStandardSmoothOfRelativeDimension n)`. -/
-instance : HasRingHomProperty (@IsSmoothOfRelativeDimension n)
+instance : HasRingHomProperty (@SmoothOfRelativeDimension n)
     (Locally (IsStandardSmoothOfRelativeDimension n)) := by
   apply HasRingHomProperty.locally_of_iff
   · exact (isStandardSmoothOfRelativeDimension_localizationPreserves n).away
   · exact isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway n
   · intro X Y f
-    rw [isSmoothOfRelativeDimension_iff]
+    rw [smoothOfRelativeDimension_iff]
 
 /-- Smooth of relative dimension `n` is stable under base change. -/
-lemma isSmoothOfRelativeDimension_isStableUnderBaseChange :
-    MorphismProperty.IsStableUnderBaseChange (@IsSmoothOfRelativeDimension n) :=
+lemma smoothOfRelativeDimension_isStableUnderBaseChange :
+    MorphismProperty.IsStableUnderBaseChange (@SmoothOfRelativeDimension n) :=
   HasRingHomProperty.isStableUnderBaseChange <| locally_isStableUnderBaseChange
     isStandardSmoothOfRelativeDimension_respectsIso
     (isStandardSmoothOfRelativeDimension_isStableUnderBaseChange n)
 
+@[deprecated (since := "2026-02-09")]
+alias isSmoothOfRelativeDimension_isStableUnderBaseChange :=
+  smoothOfRelativeDimension_isStableUnderBaseChange
+
 /-- Open immersions are smooth of relative dimension `0`. -/
-instance (priority := 900) [IsOpenImmersion f] : IsSmoothOfRelativeDimension 0 f :=
+instance (priority := 900) [IsOpenImmersion f] : SmoothOfRelativeDimension 0 f :=
   HasRingHomProperty.of_isOpenImmersion
     (locally_holdsForLocalizationAway <|
       isStandardSmoothOfRelativeDimension_holdsForLocalizationAway).containsIdentities
 
 /-- Open immersions are smooth. -/
-instance (priority := 900) [IsOpenImmersion f] : IsSmooth f :=
-  IsSmoothOfRelativeDimension.isSmooth 0 f
+instance (priority := 900) [IsOpenImmersion f] : Smooth f :=
+  SmoothOfRelativeDimension.smooth 0 f
 
 /-- If `f` is smooth of relative dimension `n` and `g` is smooth of relative dimension
 `m`, then `f ≫ g` is smooth of relative dimension `n + m`. -/
-instance isSmoothOfRelativeDimension_comp {Z : Scheme.{u}} (g : Y ⟶ Z)
-    [hf : IsSmoothOfRelativeDimension n f] [hg : IsSmoothOfRelativeDimension m g] :
-    IsSmoothOfRelativeDimension (n + m) (f ≫ g) where
+instance smoothOfRelativeDimension_comp {Z : Scheme.{u}} (g : Y ⟶ Z)
+    [hf : SmoothOfRelativeDimension n f] [hg : SmoothOfRelativeDimension m g] :
+    SmoothOfRelativeDimension (n + m) (f ≫ g) where
   exists_isStandardSmoothOfRelativeDimension x := by
     obtain ⟨U₂, V₂, hfx₂, e₂, hf₂⟩ := hg.exists_isStandardSmoothOfRelativeDimension (f x)
     obtain ⟨U₁', V₁', hx₁', e₁', hf₁'⟩ := hf.exists_isStandardSmoothOfRelativeDimension x
@@ -159,20 +173,20 @@ instance isSmoothOfRelativeDimension_comp {Z : Scheme.{u}} (g : Y ⟶ Z)
     exact (isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway n).left
       _ r _ hf₁
 
-instance {Z : Scheme.{u}} (g : Y ⟶ Z) [IsSmoothOfRelativeDimension 0 f]
-    [IsSmoothOfRelativeDimension 0 g] :
-    IsSmoothOfRelativeDimension 0 (f ≫ g) :=
-  inferInstanceAs <| IsSmoothOfRelativeDimension (0 + 0) (f ≫ g)
+instance {Z : Scheme.{u}} (g : Y ⟶ Z) [SmoothOfRelativeDimension 0 f]
+    [SmoothOfRelativeDimension 0 g] :
+    SmoothOfRelativeDimension 0 (f ≫ g) :=
+  inferInstanceAs <| SmoothOfRelativeDimension (0 + 0) (f ≫ g)
 
 /-- Smooth of relative dimension `0` is multiplicative. -/
-instance : MorphismProperty.IsMultiplicative (@IsSmoothOfRelativeDimension 0) where
+instance : MorphismProperty.IsMultiplicative (@SmoothOfRelativeDimension 0) where
   id_mem _ := inferInstance
   comp_mem _ _ _ _ := inferInstance
 
 /-- Smooth morphisms are locally of finite presentation. -/
-instance (priority := 100) [hf : IsSmooth f] : LocallyOfFinitePresentation f := by
+instance (priority := 100) [hf : Smooth f] : LocallyOfFinitePresentation f := by
   rw [HasRingHomProperty.eq_affineLocally @LocallyOfFinitePresentation]
-  rw [HasRingHomProperty.eq_affineLocally @IsSmooth] at hf
+  rw [HasRingHomProperty.eq_affineLocally @Smooth] at hf
   refine affineLocally_le (fun hf ↦ ?_) f hf
   apply RingHom.locally_of_locally (Q := RingHom.FinitePresentation) at hf
   · rwa [RingHom.locally_iff_of_localizationSpanTarget finitePresentation_respectsIso

Mathlib/AlgebraicGeometry/Sites/Etale.lean

@@ -30,15 +30,15 @@ namespace AlgebraicGeometry.Scheme
 
 /-- Big étale site: the étale precoverage on the category of schemes. -/
 def etalePrecoverage : Precoverage Scheme.{u} :=
-  precoverage @IsEtale
+  precoverage @Etale
 
 /-- Big étale site: the étale pretopology on the category of schemes. -/
 def etalePretopology : Pretopology Scheme.{u} :=
-  pretopology @IsEtale
+  pretopology @Etale
 
 /-- Big étale site: the étale topology on the category of schemes. -/
 abbrev etaleTopology : GrothendieckTopology Scheme.{u} :=
-  grothendieckTopology @IsEtale
+  grothendieckTopology @Etale
 
 lemma zariskiTopology_le_etaleTopology : zariskiTopology ≤ etaleTopology := by
   apply grothendieckTopology_monotone
@@ -48,13 +48,13 @@ lemma zariskiTopology_le_etaleTopology : zariskiTopology ≤ etaleTopology := by
 /-- The small étale site of a scheme is the Grothendieck topology on the
 category of schemes étale over `X` induced from the étale topology on `Scheme.{u}`. -/
 def smallEtaleTopology (X : Scheme.{u}) : GrothendieckTopology X.Etale :=
-  X.smallGrothendieckTopology (P := @IsEtale)
+  X.smallGrothendieckTopology (P := @Etale)
 
 /-- The pretopology generating the small étale site. -/
 def smallEtalePretopology (X : Scheme.{u}) : Pretopology X.Etale :=
-  X.smallPretopology (Q := @IsEtale) (P := @IsEtale)
+  X.smallPretopology (Q := @Etale) (P := @Etale)
 
-instance {S : Scheme.{u}} (𝒰 : S.Cover (precoverage @IsEtale)) (i : 𝒰.I₀) : IsEtale (𝒰.f i) :=
+instance {S : Scheme.{u}} (𝒰 : S.Cover (precoverage @Etale)) (i : 𝒰.I₀) : Etale (𝒰.f i) :=
   𝒰.map_prop i
 
 /-- A separably closed field `Ω` defines a point on the étale topology by the fiber