Module

FiniteEtale.lean

Nyll.EtaleFundamentalGroups.Normalization.Localization.IntegralClosure.FiniteEtale

2 declarations indexed from sourceView source ↗

Module documentation

Finite etaleness of a relative normalization from affine charts

The standard affine open cover of a relative normalization is built from integral closures. This file turns formal etaleness of the corresponding prime-local algebra maps into finite etaleness of the actual global normalization morphism. A boundary form allows the local calculation to be restricted to points outside an open locus where etaleness is already known.

Imports2

Imported by1

Nyll.EtaleFundamentalGroups.Normalization.Localization.IntegralClosure.All

theorem

isFiniteEtale_fromNormalization_of_chartPrimeLocalizations

L31 ↗

EtaleFundamentalGroups.isFiniteEtale_fromNormalization_of_chartPrimeLocalizations

Documentation

A finite relative normalization is finite etale if the prime-local map on every affine integral-closure chart is formally etale.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open CategoryTheory
open AlgebraicGeometry
universe u

Lean source · full declaration

theorem isFiniteEtale_fromNormalization_of_chartPrimeLocalizations
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [QuasiCompact f] [QuasiSeparated f] [IsLocallyNoetherian Y]
    [IsFinite f.fromNormalization]
    (hlocal :
      ∀ (U : Y.Opens) (_hU : IsAffineOpen U)
        (Q : PrimeSpectrum
          (letI := (f.app U).hom.toAlgebra
           integralClosure Γ(Y, U) Γ(X, f ⁻¹ᵁ U))),
        letI := (f.app U).hom.toAlgebra
        let C := integralClosure Γ(Y, U) Γ(X, f ⁻¹ᵁ U)
        let φ : Γ(Y, U) →+* C := algebraMap Γ(Y, U) C
        (Localization.localRingHom
          (Q.comap φ).asIdeal Q.asIdeal φ rfl).FormallyEtale) :
    IsFiniteEtale f.fromNormalization := by
  apply isFiniteEtale_of_isFinite_of_stalkMap_formallyEtale
    f.fromNormalization
  intro y
  obtain ⟨U, Q, hQ⟩ := f.normalizationOpenCover.exists_eq y
  subst y
  exact
    (RingHom.FormallyEtale.respectsIso.arrow_mk_iso_iff
      (normalizationChartStalkPrimeLocalizationArrowIso f U.2 Q)).mpr
        (hlocal U.1 U.2 Q)

theorem

isFiniteEtale_fromNormalization_of_restrict_etale_of_boundary_chartPrimeLocalizations

L59 ↗

EtaleFundamentalGroups.isFiniteEtale_fromNormalization_of_restrict_etale_of_boundary_chartPrimeLocalizations