An étale criterion through the Jacobi–Zariski sequence

For algebras k → A → S with S formally smooth over k, the map A → S is formally étale as soon as the base-change map S ⊗_A Ω[A⁄k] → Ω[S⁄k] is bijective ([TSPA, Tags 00S2, 00UO]):

• surjectivity gives Ω[S⁄A] = 0 (the exact sequence S ⊗_A Ω[A⁄k] → Ω[S⁄k] → Ω[S⁄A] → 0, [TSPA, Tag 00RS]), i.e. A → S is formally unramified;
• injectivity gives H¹(L_{S/A}) = 0 through the Jacobi–Zariski sequence H¹(L_{S/k}) → H¹(L_{S/A}) → S ⊗_A Ω[A⁄k] → Ω[S⁄k] [TSPA, Tag 00S2]: H¹(L_{S/k}) = 0 because S/k is formally smooth, and the connecting map is zero because the next map is injective; with Ω[S⁄A] = 0 projective, A → S is formally smooth (Mathlib's definition of formal smoothness, [TSPA, Tag 00TI]).

Finite presentation of S/A follows from that of S/k when A/k is of finite type, so A → S is étale (Algebra.Etale). The application (etale_aeval_of_span_eq_top): A = k[t_0, …, t_{n-1}] and t_i ↦ v_i ∈ S where Ω[S⁄k] is free of rank n and the d v_i generate it; the base-change map is then a surjection S^n → S^n between free modules of the same rank, hence bijective (OrzechProperty.bijective_of_surjective_of_finrank_le). This replaces the flatness argument of the obvious proof of [TSPA, Tag 054L] in given coordinates, which would need the flatness of k[t] → S before étaleness is known. Used to produce étale coordinates on a smooth scheme (Hironaka/Scheme/Smooth/EtaleCoordinates.lean).

theorem Algebra.surjective_map_self (k A S : Type u) [CommRing k] [CommRing A] [CommRing S] [Algebra k A] [Algebra k S] [Algebra A S] [IsScalarTower k A S] : Function.Surjective ⇑(KaehlerDifferential.map k A S S)

Ω[S⁄A] → Ω[S⁄A], the map induced by the identity of S, is surjective (it is the identity on the generators d s).

theorem Algebra.formallyUnramified_of_surjective_mapBaseChange (k A S : Type u) [CommRing k] [CommRing A] [CommRing S] [Algebra k A] [Algebra k S] [Algebra A S] [IsScalarTower k A S] (h : Function.Surjective ⇑(KaehlerDifferential.mapBaseChange k A S)) : FormallyUnramified A S

If S ⊗_A Ω[A⁄k] → Ω[S⁄k] is surjective then Ω[S⁄A] = 0, i.e. A → S is formally unramified [TSPA, Tag 00RS].

theorem Algebra.formallySmooth_of_bijective_mapBaseChange (k A S : Type u) [CommRing k] [CommRing A] [CommRing S] [Algebra k A] [Algebra k S] [Algebra A S] [IsScalarTower k A S] [FormallySmooth k S] (h : Function.Bijective ⇑(KaehlerDifferential.mapBaseChange k A S)) : FormallySmooth A S

If S is formally smooth over k and S ⊗_A Ω[A⁄k] → Ω[S⁄k] is bijective, then S is formally smooth over A (the Jacobi–Zariski sequence, [TSPA, Tags 00S2, 00TI]).

theorem Algebra.etale_of_bijective_mapBaseChange (k A S : Type u) [CommRing k] [CommRing A] [CommRing S] [Algebra k A] [Algebra k S] [Algebra A S] [IsScalarTower k A S] [FormallySmooth k S] [FinitePresentation k S] [FiniteType k A] (h : Function.Bijective ⇑(KaehlerDifferential.mapBaseChange k A S)) : Etale A S

The étale criterion: A → S is étale when S is smooth over k, A is of finite type over k, and S ⊗_A Ω[A⁄k] → Ω[S⁄k] is bijective.

theorem Algebra.etale_aeval_of_span_eq_top {k S : Type u} [CommRing k] [CommRing S] [Algebra k S] {n : ℕ} (v : Fin n → S) [Nontrivial S] [FormallySmooth k S] [FinitePresentation k S] [Module.Free S Ω[S⁄k]] [Module.Finite S Ω[S⁄k]] (hrank : Module.finrank S Ω[S⁄k] = n) (hspan : Submodule.span S (Set.range fun (i : Fin n) => (KaehlerDifferential.D k S) (v i)) = ⊤) : (MvPolynomial.aeval v).Etale

If Ω[S⁄k] is free of rank n and the differentials of v_0, …, v_{n-1} ∈ S generate it, then k[t_0, …, t_{n-1}] → S, t_i ↦ v_i, is étale (the argument of [TSPA, Tag 054L] in given coordinates).