Nyll.EtaleFundamentalGroups.Purity.PrincipalNormalizationSpreading

Module documentation

Finite normalization over a principal affine chart

The finite source over the principal localization is replaced by its actual affine spectrum. The structure map supplies the algebra structures, and the canonical source-normalization isomorphism preserves every base change. The ring-level spreading theorem therefore applies to the original scheme normalization, without a global normality assumption on the affine base.

theorem

finiteEtale_normalization_of_principal_factorization

L34 ↗

EtaleFundamentalGroups.finiteEtale_normalization_of_principal_factorization

Documentation

For a finite morphism over a principal localization, finite etaleness of the actual normalization over every base local ring spreads globally when the base is normal along the principal boundary.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem finiteEtale_normalization_of_principal_factorization
    (R : Type u) [CommRing R] [IsNoetherianRing R] (d : R)
    (A : Type u) [CommRing A] [Algebra R A] [IsLocalization.Away d A]
    {Y : Scheme.{u}} (g : Y ⟶ Spec (.of A)) [IsFinite g]
    (hnormal : ∀ (p : Ideal R) [p.IsPrime], d ∈ p →
      IsDomain (Localization.AtPrime p) ∧ IsIntegrallyClosed (Localization.AtPrime p))
    (hlocal : ∀ p : PrimeSpectrum R,
      IsFiniteEtale (pullback.snd
        (g ≫ Spec.map (CommRingCat.ofHom (algebraMap R A))).fromNormalization
        (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.AtPrime p.asIdeal)))))) :
    IsFiniteEtale
      (g ≫ Spec.map (CommRingCat.ofHom (algebraMap R A))).fromNormalization

Module documentation

Finite normalization over a principal affine chart

Declarations

finiteEtale_normalization_of_principal_factorization