NYLL
Module

GlobalLocalUnramifiedCriterion.lean

Nyll.EtaleFundamentalGroups.Normalization.GlobalLocalUnramifiedCriterion
3 declarations indexed from sourceView source ↗

Module documentation

The global local-ring criterion for unramified normalization

The actual affine normalization square and the affine-chart stalk isomorphism identify each base-prime localization with the literal pullback over the original scheme stalk. The non-Noetherian ring criterion then supplies étaleness on every affine open, hence globally.

This proves the original implication (5) ⇒ (4) in Stacks Project Tag 0BTF for an arbitrary finite function-field extension.

Imports9
Imported by2

Declarations

instance

fieldSpecQuasiCompact

L39 ↗
EtaleFundamentalGroups.fieldSpecQuasiCompact
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u
Lean source · full declaration
instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
theorem

localized_normalizationChart_unramified_of_stalk

L44 ↗
EtaleFundamentalGroups.localized_normalizationChart_unramified_of_stalk
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
Lean source · full declaration
theorem localized_normalizationChart_unramified_of_stalk
    (X : Scheme.{u}) [IsIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L]
    (U : X.Opens) (hU : IsAffineOpen U) [Nonempty U]
    (p : PrimeSpectrum Γ(X, U))
    (hlocal : FormallyUnramified (pullback.snd
        (X.genericExtensionMorphism L).fromNormalization
        (X.fromSpecStalk (hU.fromSpec p))) ∧
      LocallyOfFiniteType (pullback.snd
        (X.genericExtensionMorphism L).fromNormalization
        (X.fromSpecStalk (hU.fromSpec p)))) :
    let : Algebra Γ(X, U) L := X.affineExtensionAlgebra U L
    Algebra.FiniteType (Localization.AtPrime p.asIdeal)
        (Localization.AtPrime p.asIdeal ⊗[Γ(X, U)] integralClosure Γ(X, U) L) ∧
      Algebra.FormallyUnramified (Localization.AtPrime p.asIdeal)
        (Localization.AtPrime p.asIdeal ⊗[Γ(X, U)] integralClosure Γ(X, U) L) := by
  intro actualAlgebra
  let R := Γ(X, U)
  let B := integralClosure R L
  let Rp := Localization.AtPrime p.asIdeal
  let BP := Rp ⊗[R] B
  let f := (X.genericExtensionMorphism L).fromNormalization
  let b := X.fromSpecStalk (hU.fromSpec p)
  let a := Spec.map (hU.stalkIsoLocalization p).hom
  let v := Spec.map (CommRingCat.ofHom (algebraMap R Rp))
  let q := Spec.map (CommRingCat.ofHom (algebraMap Rp BP))
  let d := Spec.map (CommRingCat.ofHom
    (Algebra.TensorProduct.includeRight : B →ₐ[R] BP).toRingHom)
  let P : MorphismProperty Scheme.{u} := @FormallyUnramified ⊓ @LocallyOfFiniteType
  have : MorphismProperty.IsStableUnderBaseChange
      (@FormallyUnramified : MorphismProperty Scheme.{u}) :=
    HasRingHomProperty.isStableUnderBaseChange
      RingHom.FormallyUnramified.isStableUnderBaseChange
  have : P.IsStableUnderBaseChange := MorphismProperty.IsStableUnderBaseChange.inf
  have : P.RespectsIso :=
    inferInstanceAs (MorphismProperty.RespectsIso
      ((@FormallyUnramified : MorphismProperty Scheme.{u}) ⊓ @LocallyOfFiniteType))
  have hbase : P (pullback.snd (pullback.snd f b) a) :=
    MorphismProperty.of_isPullback
      (IsPullback.of_hasPullback (pullback.snd f b) a) hlocal
  have hpaste : P (pullback.snd (pullback.snd f b) a) ↔
      P (pullback.snd f (a ≫ b)) := by
    rw [← pullbackLeftPullbackSndIso_hom_snd f b a]
    exact P.cancel_left_of_respectsIso (pullbackLeftPullbackSndIso f b a).hom _
  have hab : a ≫ b = v ≫ hU.fromSpec :=
    hU.SpecMap_stalkIsoLocalization_fromSpecStalk p
  have hcanonical : P (pullback.snd f (v ≫ hU.fromSpec)) := by
    rw [← hab]
    exact hpaste.mp hbase
  have htensor : IsPullback q d v
      (Spec.map (CommRingCat.ofHom (algebraMap R B))) :=
    isPullback_SpecMap_of_isPushout _ _ _ _ (CommRingCat.isPushout_tensorProduct R Rp B)
  have htotal := htensor.paste_vert (isPullback_genericNormalizationChart X L U hU)
  have hq : P q := by
    rw [← htotal.flip.isoPullback_hom_snd]
    exact (P.cancel_left_of_respectsIso htotal.flip.isoPullback.hom _).mpr hcanonical
  exact ⟨RingHom.finiteType_algebraMap.mp
      ((HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)).mp hq.2),
    RingHom.formallyUnramified_algebraMap.mp
      ((HasRingHomProperty.Spec_iff (P := @FormallyUnramified)).mp hq.1)⟩
theorem

finiteEtale_normalization_of_stalk_unramified

L108 ↗
EtaleFundamentalGroups.finiteEtale_normalization_of_stalk_unramified
Documentation

Original Tag 0BTF (5) ⇒ (4): if the actual normalization becomes unramified over every scheme local ring, it is globally finite étale. The finite function-field extension need not be Galois or separable.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
Lean source · statement
theorem finiteEtale_normalization_of_stalk_unramified
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L]
    [FiniteDimensional X.functionField L]
    (hlocal : ∀ x : X,
      FormallyUnramified (pullback.snd
          (X.genericExtensionMorphism L).fromNormalization (X.fromSpecStalk x)) ∧
        LocallyOfFiniteType (pullback.snd
          (X.genericExtensionMorphism L).fromNormalization (X.fromSpecStalk x))) :
    IsFinite (X.genericExtensionMorphism L).fromNormalization ∧
      Etale (X.genericExtensionMorphism L).fromNormalization

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.