Finite étale covers of punctured spectra and local purity

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremThe 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.

TauCeti.Algebra.etale_iff_isUnit_discr.{u_1, u_2, u_3} {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)
Lean

Formalized in Tau Ceti as TauCeti.Algebra.etale_iff_isUnit_discr.

Sources
LeanTauCeti.Algebra.etale_iff_isUnit_discr
Uses 1 · Used by 2
Proof usesTauCeti.Algebra.etale_iff_traceForm_nondegenerate
Used byTauCeti.Algebra.etale_iff_etale_fiber_of_height_le_one · TauCeti.Algebra.isUnit_discr_localization_iff

TheoremTauCeti.Algebra.etale_iff_traceForm_nondegenerate#

A finite-dimensional 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).

TauCeti.Algebra.etale_iff_traceForm_nondegenerate.{u_1, u_2} (K : Type u_1) (B : Type u_2) [Field K]
  [CommRing B] [Algebra K B] [FiniteDimensional K B] :
  Algebra.Etale K B ↔ (Algebra.traceForm K B).Nondegenerate
Lean

Formalized in Tau Ceti as TauCeti.Algebra.etale_iff_traceForm_nondegenerate.

Sources
LeanTauCeti.Algebra.etale_iff_traceForm_nondegenerate
Used by 2
Used byTauCeti.Algebra.etale_iff_etale_fiber_of_height_le_one · The discriminant criterion

TheoremTauCeti.Algebra.etale_iff_etale_fiber_of_height_le_one#

A finite free algebra over a Noetherian ring is étale if and only if its fibres over all primes of height at most one are étale. Minimal primes must be included; no generic étaleness assumption is imposed.

TauCeti.Algebra.etale_iff_etale_fiber_of_height_le_one.{u_1, u_2} {A : Type u_1} {B : Type u_2}
  [CommRing A] [CommRing B] [Algebra A B] [IsNoetherianRing A] [Module.Finite A B]
  [Module.Free A B] :
  Algebra.Etale A B ↔
    ∀ (p : Ideal A) [inst : p.IsPrime], p.height ≤ 1 → Algebra.Etale p.ResidueField (p.Fiber B)
Lean

Formalized in Tau Ceti as TauCeti.Algebra.etale_iff_etale_fiber_of_height_le_one.

Sources
LeanTauCeti.Algebra.etale_iff_etale_fiber_of_height_le_one
Uses 2 · Used by 1
Proof usesThe discriminant criterion · TauCeti.Algebra.etale_iff_traceForm_nondegenerate
Used byTauCeti.Algebra.etale_of_isUnramifiedAt_of_two_le_ringKrullDim

TheoremTauCeti.Algebra.etale_of_isUnramifiedAt_of_two_le_ringKrullDim#

A finite flat algebra over a Noetherian local ring of dimension at least two is étale everywhere if it is unramified at each prime not lying over the closed point. This is the finite flat case of local purity, with no regularity or normality assumptions.

TauCeti.Algebra.etale_of_isUnramifiedAt_of_two_le_ringKrullDim.{u_1, u_2} {A : Type u_1}
  {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsNoetherianRing A] [IsLocalRing A]
  [Module.Finite A B] [Module.Flat A B] (hdim : 2 ≤ ringKrullDim A)
  (h :
    ∀ (q : Ideal B) [inst : q.IsPrime],
      Ideal.under A q ≠ IsLocalRing.maximalIdeal A → Algebra.IsUnramifiedAt A q) :
  Algebra.Etale A B
Lean

Formalized in Tau Ceti as TauCeti.Algebra.etale_of_isUnramifiedAt_of_two_le_ringKrullDim.

Sources
LeanTauCeti.Algebra.etale_of_isUnramifiedAt_of_two_le_ringKrullDim
Uses 1
Proof usesTauCeti.Algebra.etale_iff_etale_fiber_of_height_le_one

TheoremA regular local ring is Cohen–Macaulay#

Stacks, Lemma 10.106.3 (00NQ).

TauCeti.IsRegularLocalRing.isCohenMacaulay.{u} {R : Type u} [CommRing R] [IsRegularLocalRing R] :
  Module.IsCohenMacaulay R R
Lean

Formalized in Tau Ceti as TauCeti.IsRegularLocalRing.isCohenMacaulay.

Sources
LeanTauCeti.IsRegularLocalRing.isCohenMacaulay
Used by 1
Used byKunz's theorem

TheoremTauCeti.Algebra.isUnit_discr_localization_iff#

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_𝔭.

TauCeti.Algebra.isUnit_discr_localization_iff.{u_1, u_2, u_3} {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)
Lean

Formalized in Tau Ceti as TauCeti.Algebra.isUnit_discr_localization_iff.

Sources
LeanTauCeti.Algebra.isUnit_discr_localization_iff
Uses 1
Proof usesThe discriminant criterion

TheoremTauCeti.IsRegularLocalRing.isRegular_pair_of_finite_normal#

Over a two-dimensional regular local ring, every pair generating the maximal ideal is regular on any finite injective normal local algebra, considered as a module over the base.

TauCeti.IsRegularLocalRing.isRegular_pair_of_finite_normal.{u_1, u_2} {A : Type u_1} {B : Type u_2}
  [CommRing A] [CommRing B] [Algebra A B] [IsRegularLocalRing A] [IsLocalRing B] [IsDomain B]
  [IsIntegrallyClosed B] [Module.Finite A B] [IsLocalHom (algebraMap A B)]
  (hinj : Function.Injective ⇑(algebraMap A B)) (hdim : ringKrullDim A = 2) {x y : A}
  (hxy : Ideal.span {x, y} = IsLocalRing.maximalIdeal A) : RingTheory.Sequence.IsRegular B [x, y]
Lean

Formalized in Tau Ceti as TauCeti.IsRegularLocalRing.isRegular_pair_of_finite_normal.

Sources
LeanTauCeti.IsRegularLocalRing.isRegular_pair_of_finite_normal

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.