Documentation

Mathlib.RingTheory.Etale.Basic

Etale morphisms #

An R-algebra A is formally étale if for every R-algebra, every square-zero ideal I : Ideal B and f : A →ₐ[R] B ⧸ I, there exists exactly one lift A →ₐ[R] B. It is étale if it is formally étale and of finite presentation.

We show that the property extends onto nilpotent ideals, and that these properties are stable under R-algebra homomorphisms and compositions.

We show that étale is stable under algebra isomorphisms, composition and localization at an element.

theorem Algebra.formallyEtale_iff (R : Type u) [CommSemiring R] (A : Type u) [Semiring A] [Algebra R A] :
Algebra.FormallyEtale R A ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = Function.Bijective (Ideal.Quotient.mkₐ R I).comp
class Algebra.FormallyEtale (R : Type u) [CommSemiring R] (A : Type u) [Semiring A] [Algebra R A] :

An R algebra A is formally étale if for every R-algebra, every square-zero ideal I : Ideal B and f : A →ₐ[R] B ⧸ I, there exists exactly one lift A →ₐ[R] B.

See https://stacks.math.columbia.edu/tag/00UQ

Instances
    theorem Algebra.FormallyEtale.comp_bijective {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] [self : Algebra.FormallyEtale R A] ⦃B : Type u⦄ [CommRing B] [Algebra R B] (I : Ideal B) :
    @[instance 100]
    Equations
    • =
    @[instance 100]
    Equations
    • =
    Equations
    • =

    We now consider a commutative square of commutative rings

    R -----> S
    |        |
    |        |
    v        v
    Rₘ ----> Sₘ
    

    where Rₘ and Sₘ are the localisations of R and S at a multiplicatively closed subset M of R.

    Let R, S, Rₘ, Sₘ be commutative rings

    Let M be a multiplicatively closed subset of R

    Assume that the rings are in a commutative diagram as above.

    and that Rₘ and Sₘ are localizations of R and S at M.

    theorem Algebra.FormallyEtale.of_isLocalization {R : Type u} {Rₘ : Type u} [CommRing R] [CommRing Rₘ] (M : Submonoid R) [Algebra R Rₘ] [IsLocalization M Rₘ] :
    theorem Algebra.FormallyEtale.localization_base {R : Type u} {Rₘ : Type u} {Sₘ : Type u} [CommRing R] [CommRing Rₘ] [CommRing Sₘ] (M : Submonoid R) [Algebra R Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [IsLocalization M Rₘ] [Algebra.FormallyEtale R Sₘ] :
    theorem Algebra.FormallyEtale.localization_map {R : Type u} {S : Type u} {Rₘ : Type u} {Sₘ : Type u} [CommRing R] [CommRing S] [CommRing Rₘ] [CommRing Sₘ] (M : Submonoid R) [Algebra R S] [Algebra R Sₘ] [Algebra S Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [IsLocalization M Rₘ] [IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ] [Algebra.FormallyEtale R S] :

    The localization of a formally étale map is formally étale.

    class Algebra.Etale (R : Type u) [CommSemiring R] (A : Type u) [Semiring A] [Algebra R A] :

    An R-algebra A is étale if it is formally étale and of finite presentation.

    Note that the definition https://stacks.math.columbia.edu/tag/00U1 in the stacks project is different, but https://stacks.math.columbia.edu/tag/00UR shows that it is equivalent to the definition here.

    Instances
      theorem Algebra.Etale.of_equiv {R : Type u} [CommRing R] {A : Type u} {B : Type u} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra.Etale R A] (e : A ≃ₐ[R] B) :

      Being étale is transported via algebra isomorphisms.

      theorem Algebra.Etale.comp (R : Type u) [CommRing R] (A : Type u) (B : Type u) [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Algebra.Etale R A] [Algebra.Etale A B] :

      Etale is stable under composition.

      instance Algebra.Etale.baseChange (R : Type u) [CommRing R] (A : Type u) (B : Type u) [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra.Etale R A] :

      Etale is stable under base change.

      Equations
      • =

      Localization at an element is étale.