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.