Zariski's main theorem

Stream: mathlib4

[Andrew Yang]

I am here to advertise that #32534 contains a sorry free proof of Zariski's main theorem for affine morphisms, Which says that:

/--
**Zariski's main theorem** for affine morphisms.

Recall that any qcqs morphism `f : X ⟶ Y` factors through the relative normalization via
`f.toNormalization : X ⟶ f.normalization` (a dominant morphism) and
`f.fromNormalization : f.normalization ⟶ Y` (an integral morphism).

Let `f : X ⟶ Y` be an affine morphism locally of finite type.

then there exists `U : f.normalization.Opens`, such that
1. `f.toNormalization ∣_ U` is an isomorphism
2. `f.toNormalization ⁻¹ᵁ U` is the quasi-finite locus of `f`

The full version for non-affine morphisms is much harder.
-/
@[stacks 03GT]
lemma Scheme.Hom.exists_isIso_morphismRestrict_toNormalization
    {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsAffineHom f] :
    ∃ U : f.normalization.Opens, IsIso (f.toNormalization ∣_ U) ∧
      (f.toNormalization ⁻¹ᵁ U).1 = f.quasiFiniteLocus

And I would love to see this in mathlib sooner rather than later. Here is a list of prerequisite PRs that are currently open for review, a fair chunk of them are also interesting in and of themselves.

• #32530: API about IsDiscrete (topology)
• #32528: Going-down for integrally closed domains
• #32429: IsIntegrallyClosed R[X]
• #32375: More API for Ideal.ResidueField
• #32536: If A/I is R-finite and I is fg and nilpotent then so is A.
• #32537: Strongly transcendental elements
• #32596: localization commutes with integral closure
• #32595: "Relative Spec for 𝒪ₓ-algebras" (algebraic geometry)

[Andrew Yang]

I am back with more advertisements, about applications of Zariski's main theorem:

• etale algebras are locally standard etale
• etale lifting property of henselian local rings
• unramified + flat => etale (technically doesn't need ZMT but is part of the branch anyways)
• classification of finite etale algebras over henselian local rings, which in turn imply the classification of unramified extensions of local fields. This was my main motivation and it somehow took ages.

import Mathlib.CFT.Junk
import Mathlib.CFT.Nonsense
import Mathlib.CFT.SeparableResidueStruct

open IsLocalRing

local notation "𝓀[" R "]" => ResidueField R
local notation "𝓂[" R "]" => maximalIdeal R

/-! Let `R` be a complete DVR. -/
variable {R : Type} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [IsAdicComplete 𝓂[R] R]

/-! ## Essentially surjective
    Each finite separable extension over `𝓀[R]` comes from some finite unramified extension. -/
example {K : Type} [Field K] [Algebra 𝓀[R] K]
    [FiniteDimensional 𝓀[R] K] [Algebra.IsSeparable 𝓀[R] K] :
    ∃ (S : Type) (_ : CommRing S) (_ : IsDomain S) (_ : IsDiscreteValuationRing S)
      (_ : Algebra R S) (_ : FaithfulSMul R S) (_ : Module.Finite R S)
      (_ : Algebra.Unramified R S), Nonempty (𝓀[S] ≃ₐ[𝓀[R]] K) := by
  obtain ⟨𝓟, ⟨e⟩⟩ := SeparableResidueStruct.exists_of_isSeparable (R := R) (K := K)
  exact ⟨𝓟.Ring, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance,
    inferInstance, inferInstance, ⟨e⟩⟩

variable {A B : Type*} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    [IsDomain A] [IsDiscreteValuationRing A]
    [FaithfulSMul R A] [Module.Finite R A] [Algebra.Unramified R A]
    [IsDomain B] [IsDiscreteValuationRing B]
    [FaithfulSMul R B] [Module.Finite R B] [Algebra.Unramified R B]

/-! ## Full
    Every map between residue fields lifts to a map between the unramified extension. -/
example (f : 𝓀[A] →ₐ[𝓀[R]] 𝓀[B]) :
    ∃ (g : A →ₐ[R] B), ResidueField.map g.toRingHom = f.toRingHom :=
  ⟨_, (HenselianLocalRing.exist_residueFieldMap_eq_of_etale f).choose_spec.choose_spec⟩

/-! ## Faithful
    Maps between unramified extensions are equal if they are equal on the residue field. -/
example (f₁ f₂ : 𝓀[A] →ₐ[𝓀[R]] 𝓀[B])
    (H : ResidueField.map f₁.toRingHom = ResidueField.map f₂.toRingHom) : f₁ = f₂ :=
  HenselianLocalRing.eq_of_residueFieldMap_eq _ _ H

/-! ## Reflects isos
    Unramified extensions with isomorphic residue fields are isomorphic. -/
example (e : 𝓀[A] ≃ₐ[𝓀[R]] 𝓀[B]) :
    ∃ (g : A ≃ₐ[R] B), ResidueField.map g.toRingHom = e.toRingHom :=
  ⟨_, (HenselianLocalRing.exist_algEquiv_residueFieldMap_eq_of_etale e).choose_spec.choose_spec⟩

All of them are sorry free and could be in mathlib today if you click the big shiny merge button :wink:
(terms and conditions may apply)

But if you rather review the prerequisites instead, here are the new PRs

• #32540: properties on Algebra.TensorProduct.map.
• #32529: etale locus
• #32665: quasi-finite algebras
• #32617: field extension over perfect fields are smooth 

Half of the PRs last time are also still open for review.

[Joël Riou]

I have merged #32540 and delegated #32529. I would let others (who know the Algebra/RingTheory hierarchy better than I know) look at the two other prerequisites, but this looks great!

[Andrew Yang]

Thanks a lot for the reviews! The new batch of PRs just arrived, all ready for review, and I believe we are two or three PRs away from the proof of Zariski's main theorem after they are reviewed.

• #32823: construct etale neighborhood that isolates point in fiber
• #32823: relative normalization of schemes (algebraic geometry)
• #32811: the statement of Zariski's main theorem
• #32809: residue field of I[X]
• #32806: base change of ideal with flat quotients
• #32803: more-linear version of tensorKaehlerEquiv
• #32802: more ergonomic version of jacobi criterion for smoothness
• #32837: noetherian model for etale algebras

[Andrew Yang]

Final update (at least for this year):
I had planned to stop here but I was very surprised to learn that the full version of Zariski's main theorem also has a purely algebraic proof (i.e. no cohomology) so naturally I had to formalize it as well. This is sorry free here in the same PR #32534 as before.

lemma Scheme.Hom.exists_isIso_morphismRestrict_toNormalization
    [LocallyOfFiniteType f] [IsSeparated f] [QuasiCompact f] :
    ∃ U : f.normalization.Opens, IsIso (f.toNormalization ∣_ U) ∧
      (f.toNormalization ⁻¹ᵁ U).1 = f.quasiFiniteLocus

As a corollary, we also get that finite = proper + finite fibers

lemma IsFinite.iff_isProper_and_locallyQuasiFinite :
    IsFinite f ↔ IsProper f ∧ LocallyQuasiFinite f

One can see the currently open PRs leading toward this at #32534:

• #32665: quasi-finite algebras
• #32823: construct etale neighborhood that isolates point in fiber
• #32811: predicate on satisfying Zariski's main theorem
• #32806: feat(RingTheory): base change of ideal with flat quotients
• #32803: more-linear version of tensorKaehlerEquiv
• #32837: noetherian model for etale algebras

[Andrew Yang]

Could I ask someone to review #32811? It had been sitting for a month now. Once this and #33718 are merged I think we are ready for the PR on the algebraic Zariski's main theorem.

[Andrew Yang]

#33469 and #32803 has been sitting for three weeks now. They are both routine generalizations of existing definitions that makes R-linear maps S-linear instead. It would be great if someone can take a look.