Zariski's Main Theorem

In this file we prove Grothendieck's reformulation of Zariski's main theorem, namely if f : X ⟶ Y is separated and of finite type, then the map from the quasi-finite locus U ⊆ X of f to the relative normalization X' of Y in X is an open immersion.

We then have the following corollaries

• Scheme.Hom.isOpen_quasiFiniteAt : If f is separated and of finite type, then the quasi-finite locus of f is open.
• If f is itself quasi-finite, then the map f.toNormalization : X ⟶ X' is an open immersion. This can be accessed via inferInstance.
• IsFinite.of_isProper_of_locallyQuasiFinite: If f is proper and quasi-finite, then the map f.toNormalization : X ⟶ X' is an isomorphism, which implies that f itself is finite.

theorem AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt {X S : Scheme} (f : X ⟶ S) [LocallyOfFiniteType f] [IsSeparated f] {x : ↥X} {s : ↥S} (h : f x = s) (hx : Scheme.Hom.QuasiFiniteAt f x) : ∃ (U : Scheme) (g : U ⟶ S), Etale g ∧ s ∈ Set.range ⇑g ∧ ∃ (V : (CategoryTheory.Limits.pullback f g).Opens) (W : (CategoryTheory.Limits.pullback f g).Opens) (v : ↥V), IsCompl V W ∧ IsFinite (CategoryTheory.CategoryStruct.comp V.ι (CategoryTheory.Limits.pullback.snd f g)) ∧ (CategoryTheory.Limits.pullback.fst f g) ↑v = x

theorem AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsSeparated f] [QuasiCompact f] (x : ↥X) (hx : QuasiFiniteAt f x) : ∃ (V : (normalization f).Opens), (toNormalization f) x ∈ V ∧ CategoryTheory.IsIso (toNormalization f ∣_ V)

theorem AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsSeparated f] [QuasiCompact f] : ∃ (U : (normalization f).Opens), CategoryTheory.IsIso (toNormalization f ∣_ U) ∧ ((TopologicalSpace.Opens.map (toNormalization f).base).obj U).carrier = {x : ↥X | QuasiFiniteAt f x}

Zariski's main theorem

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 separated and 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

theorem AlgebraicGeometry.Scheme.Hom.isOpen_quasiFiniteAt {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] : IsOpen {x : ↥X | QuasiFiniteAt f x}

def AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] : X.Opens

The set of quasi-finite points of a morphism f : X ⟶ Y as an X.Opens.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.mem_quasiFiniteLocus {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} : x ∈ quasiFiniteLocus f ↔ QuasiFiniteAt f x

instance AlgebraicGeometry.instIsOpenImmersionCompSchemeιQuasiFiniteLocusToNormalization {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsSeparated f] [QuasiCompact f] : IsOpenImmersion (CategoryTheory.CategoryStruct.comp (Scheme.Hom.quasiFiniteLocus f).ι (Scheme.Hom.toNormalization f))

theorem AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [LocallyOfFiniteType f] : quasiFiniteLocus f = ⊤

theorem AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_comp {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} [IsOpenImmersion f] (g : Y ⟶ Z) [LocallyOfFiniteType g] : quasiFiniteLocus (CategoryTheory.CategoryStruct.comp f g) = (TopologicalSpace.Opens.map f.base).obj (quasiFiniteLocus g)

theorem AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top_iff {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] : quasiFiniteLocus f = ⊤ ↔ LocallyQuasiFinite f

instance AlgebraicGeometry.instLocallyQuasiFiniteCompSchemeιQuasiFiniteLocus {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] : LocallyQuasiFinite (CategoryTheory.CategoryStruct.comp (Scheme.Hom.quasiFiniteLocus f).ι f)

instance AlgebraicGeometry.instIsOpenImmersionToNormalizationOfLocallyQuasiFiniteOfLocallyOfFiniteType {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [LocallyOfFiniteType f] [IsSeparated f] [QuasiCompact f] : IsOpenImmersion (Scheme.Hom.toNormalization f)

instance AlgebraicGeometry.instUniversallyClosedToNormalization {X Y : Scheme} (f : X ⟶ Y) [QuasiSeparated f] [UniversallyClosed f] : UniversallyClosed (Scheme.Hom.toNormalization f)

theorem AlgebraicGeometry.IsFinite.of_isProper_of_locallyQuasiFinite {X Y : Scheme} (f : X ⟶ Y) [IsProper f] [LocallyQuasiFinite f] : IsFinite f

theorem AlgebraicGeometry.IsFinite.iff_isProper_and_locallyQuasiFinite {X Y : Scheme} (f : X ⟶ Y) : IsFinite f ↔ IsProper f ∧ LocallyQuasiFinite f

Stacks Tag 02LS ((1) <=> (3))

theorem AlgebraicGeometry.IsFinite.eq_proper_inf_locallyQuasiFinite : @IsFinite = @IsProper ⊓ @LocallyQuasiFinite

theorem AlgebraicGeometry.IsClosedImmersion.iff_isProper_and_mono {X Y : Scheme} (f : X ⟶ Y) : IsClosedImmersion f ↔ IsProper f ∧ CategoryTheory.Mono f

Stacks Tag 04XV ((1) <=> (2))

theorem AlgebraicGeometry.IsClosedImmersion.eq_proper_inf_monomorphisms : @IsClosedImmersion = @IsProper ⊓ CategoryTheory.MorphismProperty.monomorphisms Scheme

theorem AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton {X Y : Scheme} (f : X ⟶ Y) [IsProper f] (y : ↥Y) (hx : (⇑f ⁻¹' {y}).Finite) : ∃ (V : Y.Opens), y ∈ V ∧ IsFinite (f ∣_ V)

Stacks Tag 02UP

theorem AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage {X Y S : Scheme} (f : X ⟶ Y) (g : Y ⟶ S) (s : ↥S) (H : (⇑f '' (⇑(CategoryTheory.CategoryStruct.comp f g) ⁻¹' {s})).Finite) [IsProper (CategoryTheory.CategoryStruct.comp f g)] [IsSeparated g] [LocallyOfFiniteType g] : ∃ (U : S.Opens), s ∈ U ∧ IsFinite (CategoryTheory.CategoryStruct.comp (Scheme.Hom.imageι f) g ∣_ U)

Stacks Tag 0AH8