The discriminant criterion for étaleness

An algebra over a field is étale iff its trace form is nondegenerate, and a finite free algebra over any commutative ring is étale iff the discriminant of a basis is a unit (Stacks, Lemma 49.3.1 (0BJF), affine form).

Main results

• TauCeti.Algebra.etale_iff_traceForm_nondegenerate: an algebra over a field is étale iff its trace form is nondegenerate.
• TauCeti.Algebra.algebraMap_discr_ne_zero_iff_etale_baseChange: the discriminant of a basis has nonzero image in a field K iff the fibre K ⊗[A] B is étale over K.
• TauCeti.Algebra.etale_of_isUnit_discr: a finite free algebra over any ring whose basis has unit discriminant is étale.
• TauCeti.Algebra.etale_iff_isUnit_discr: a finite free algebra is étale iff the discriminant of a basis is a unit.
• TauCeti.Algebra.isUnit_algebraMap_discr_iff_etale_baseChange: the discriminant of a basis maps to a unit in an A-algebra A' iff the base change to A' is étale.
• TauCeti.Algebra.isUnit_discr_localization_iff: the discriminant of a basis is a unit at a prime 𝔭 iff the base change to A_𝔭 is étale over A_𝔭.

References

• Stacks Project, Lemma 49.3.1.
• Ported from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit 9a20b3f351446d64e6015d704198bc71c7002008 (Apache-2.0), lean/Pcf/Stacks/Purity/DiscriminantFiber.lean and lean/Pcf/Stacks/Purity/DiscriminantGlobal.lean, namespace Pcf.Stacks: etale_iff_traceForm_nondegenerate combines its Algebra.traceForm_nondegenerate_of_formallyEtale and Algebra.formallyEtale_of_discr_ne_zero_of_basis_global; etale_of_isUnit_discr generalizes its Algebra.etale_of_isUnit_discr_of_basis_global from a local base to any base; etale_iff_isUnit_discr adds the converse, its Algebra.isUnit_discr_of_etale_of_basis, likewise generalized from a local base to any base; and isUnit_discr_localization_iff extends its Algebra.isUnit_map_discr_of_etale_baseChange to an equivalence.

theorem TauCeti.Algebra.etale_iff_traceForm_nondegenerate (K : Type u_1) (B : Type u_2) [Field K] [CommRing B] [Algebra K B] : Algebra.Etale K B ↔ (Algebra.traceForm K B).Nondegenerate

An algebra over a field is étale iff its trace form is nondegenerate. The fibre case in the proof of Stacks, Lemma 49.3.1 (0BJF).

theorem TauCeti.Algebra.algebraMap_discr_ne_zero_iff_etale_baseChange {A : Type u_1} {B : Type u_2} {ι : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι A B) (K : Type u_4) [Field K] [Algebra A K] : (algebraMap A K) (Algebra.discr A ⇑b) ≠ 0 ↔ Algebra.Etale K (TensorProduct A K B)

The discriminant of a basis of a finite free A-algebra B has nonzero image in a field K over A iff the fibre K ⊗[A] B is étale over K.

theorem TauCeti.Algebra.etale_of_isUnit_discr {A : Type u_1} {B : Type u_2} {ι : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι A B) (hb : IsUnit (Algebra.discr A ⇑b)) : Algebra.Etale A B

A finite free algebra whose basis has unit discriminant is étale.

theorem TauCeti.Algebra.etale_iff_isUnit_discr {A : Type u_1} {B : Type u_2} {ι : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι A B) : Algebra.Etale A B ↔ IsUnit (Algebra.discr A ⇑b)

The discriminant criterion. A finite free algebra is étale iff the discriminant of a basis is a unit. Stacks, Lemma 49.3.1 (0BJF), affine form.

theorem TauCeti.Algebra.isUnit_algebraMap_discr_iff_etale_baseChange {A : Type u_1} {B : Type u_2} {ι : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι A B) (A' : Type u_4) [CommRing A'] [Algebra A A'] : IsUnit ((algebraMap A A') (Algebra.discr A ⇑b)) ↔ Algebra.Etale A' (TensorProduct A A' B)

The discriminant of a basis of a finite free A-algebra B maps to a unit in an A-algebra A' iff the base change A' ⊗[A] B is étale over A'.

theorem TauCeti.Algebra.isUnit_discr_localization_iff {A : Type u_1} {B : Type u_2} {ι : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι A B) (p : Ideal A) [p.IsPrime] : IsUnit ((algebraMap A (Localization.AtPrime p)) (Algebra.discr A ⇑b)) ↔ Algebra.Etale (Localization.AtPrime p) (TensorProduct A (Localization.AtPrime p) B)

The discriminant of a basis of a finite free algebra is a unit at a prime 𝔭 iff the base change to the localization A_𝔭 is étale over A_𝔭.