Documentation

Mathlib.AlgebraicGeometry.Morphisms.Etale

Étale morphisms #

A morphism of schemes f : X ⟶ Y is étale if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, the induced map Γ(Y, U) ⟶ Γ(X, V) is étale.

Main results #

source
class AlgebraicGeometry.Etale {X Y : Scheme} (f : X ⟶ Y) :
Prop

A morphism of schemes f : X ⟶ Y is étale if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is étale.

Instances
    source
    theorem AlgebraicGeometry.etale_iff {X Y : Scheme} (f : X ⟶ Y) :
    Etale f ↔ ∀ {U : Y.Opens}, IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Etale
    source
    theorem AlgebraicGeometry.Scheme.Hom.etale_appLE {X Y : Scheme} (f : X ⟶ Y) [self : Etale f] {U : Y.Opens} :
    IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (appLE f U V e)).Etale

    Alias of AlgebraicGeometry.Etale.etale_appLE.

    source
    @[deprecated AlgebraicGeometry.Etale (since := "2026-02-09")]
    def AlgebraicGeometry.IsEtale {X Y : Scheme} (f : X ⟶ Y) :
    Prop

    Alias of AlgebraicGeometry.Etale.

    A morphism of schemes f : X ⟶ Y is étale if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is étale.

    Equations
    Instances For
      source
      instance AlgebraicGeometry.Etale.instHasRingHomPropertyEtale :
      HasRingHomProperty @Etale fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.Etale

      The property of scheme morphisms Etale is associated with the ring homomorphism property Etale.

      source
      instance AlgebraicGeometry.Etale.instIsMultiplicativeScheme :
      CategoryTheory.MorphismProperty.IsMultiplicative @Etale

      Being étale is multiplicative.

      source
      instance AlgebraicGeometry.Etale.etale_comp {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) [Etale f] [Etale g] :
      Etale (CategoryTheory.CategoryStruct.comp f g)

      The composition of étale morphisms is étale.

      source
      instance AlgebraicGeometry.Etale.etale_isStableUnderBaseChange :
      CategoryTheory.MorphismProperty.IsStableUnderBaseChange @Etale

      Etale is stable under base change.

      source
      @[instance 900]
      instance AlgebraicGeometry.Etale.instOfIsOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] :
      Etale f

      Open immersions are étale.

      source
      instance AlgebraicGeometry.Etale.instFstScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [Etale g] :
      Etale (CategoryTheory.Limits.pullback.fst f g)
      source
      instance AlgebraicGeometry.Etale.instSndScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [Etale f] :
      Etale (CategoryTheory.Limits.pullback.snd f g)
      source
      instance AlgebraicGeometry.Etale.instMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [Etale f] :
      Etale (f ∣_ V)
      source
      instance AlgebraicGeometry.Etale.instResLE {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [Etale f] :
      Etale (Scheme.Hom.resLE f V U e)
      source
      theorem AlgebraicGeometry.Etale.eq_smoothOfRelativeDimension_zero :
      @Etale = @SmoothOfRelativeDimension 0
      source
      theorem AlgebraicGeometry.Etale.iff_smoothOfRelativeDimension_zero {X Y : Scheme} (f : X ⟶ Y) :
      Etale f ↔ SmoothOfRelativeDimension 0 f
      source
      instance AlgebraicGeometry.Etale.instSmoothOfRelativeDimensionOfNatNat {X Y : Scheme} (f : X ⟶ Y) [Etale f] :
      SmoothOfRelativeDimension 0 f
      source
      @[instance 100]
      instance AlgebraicGeometry.Etale.instSmooth {X Y : Scheme} (f : X ⟶ Y) [Etale f] :
      Smooth f
      source
      @[instance 900]
      instance AlgebraicGeometry.Etale.instFormallyUnramified {X Y : Scheme} (f : X ⟶ Y) [Etale f] :
      FormallyUnramified f
      source
      instance AlgebraicGeometry.Etale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified :
      CategoryTheory.MorphismProperty.HasOfPostcompProperty (@Etale) (@LocallyOfFiniteType ⊓ @FormallyUnramified)
      source
      theorem AlgebraicGeometry.Etale.of_comp {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) [Etale (CategoryTheory.CategoryStruct.comp f g)] [LocallyOfFiniteType g] [FormallyUnramified g] :
      Etale f

      If f ≫ g is étale and g unramified, then f is étale.

      source
      instance AlgebraicGeometry.Etale.instHasOfPostcompPropertyScheme :
      CategoryTheory.MorphismProperty.HasOfPostcompProperty @Etale @Etale
      source
      def AlgebraicGeometry.Scheme.Etale (X : Scheme) :
      Type (u + 1)

      The category Etale X is the category of schemes étale over X.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance AlgebraicGeometry.Scheme.instCategoryEtale (X : Scheme) :
        CategoryTheory.Category.{u, u + 1} X.Etale
        Equations
        source
        def AlgebraicGeometry.Scheme.Etale.forget (X : Scheme) :
        CategoryTheory.Functor X.Etale (CategoryTheory.Over X)

        The forgetful functor from schemes étale over X to schemes over X.

        Equations
        Instances For
          source
          def AlgebraicGeometry.Scheme.Etale.forgetFullyFaithful (X : Scheme) :
          (forget X).FullyFaithful

          The forgetful functor from schemes étale over X to schemes over X is fully faithful.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            instance AlgebraicGeometry.Scheme.instFullEtaleOverForget (X : Scheme) :
            (Etale.forget X).Full
            source
            instance AlgebraicGeometry.Scheme.instFaithfulEtaleOverForget (X : Scheme) :
            (Etale.forget X).Faithful
            source
            instance AlgebraicGeometry.Scheme.instHasPullbacksEtale (X : Scheme) :
            CategoryTheory.Limits.HasPullbacks X.Etale