Module

OpenImmersionNormalizationEquivalence.lean

Nyll.EtaleFundamentalGroups.Purity.OpenImmersionNormalizationEquivalence

2 declarations indexed from sourceView source ↗

Module documentation

Fundamental-group equivalence from canonical normalization extensions

For a quasi-compact open immersion, it suffices to prove that the canonical function-field normalization attached to every connected Galois cover is finite etale. The normalization supplies the extension objects, and open normal quotients then detect injectivity of the fundamental-group map.

Imports2

Imported by1

Nyll.EtaleFundamentalGroups.Purity.All

def

fundamentalGroupEquivOfOpenImmersionCanonicalNormalizations

L31 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivOfOpenImmersionCanonicalNormalizations

Documentation

Finite etaleness of every canonical Galois-cover normalization across a nonempty quasi-compact open immersion identifies the two etale fundamental groups.

Source context 5 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · full declaration

def fundamentalGroupEquivOfOpenImmersionCanonicalNormalizations
    {U X : Scheme.{u}}
    [IsIntegral U] [IsNormalIntegral U] [IsLocallyNoetherian U]
    [ConnectedSpace U]
    [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] [Nonempty U]
    [QuasiCompact j] [QuasiSeparated j]
    (hEtale : ∀ (W : FiniteEtale U) (hW : IsGalois W),
      letI : IsGalois W := hW
      IsFiniteEtale
        (connectedCoverGenericComposite W ≫ j).fromNormalization)
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ U) :
    π₁ᵉᵗ(xi) ≃ₜ* π₁ᵉᵗ(xi ≫ j) := by
  apply fundamentalGroupEquivOfOpenImmersionGaloisExtensions j ?_ xi
  intro W hW
  letI : IsGalois W := hW
  exact connectedCoverExtensionOfNormalization W j (hEtale W hW)

theorem

fundamentalGroupEquivOfOpenImmersionCanonicalNormalizations_apply

L51 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivOfOpenImmersionCanonicalNormalizations_apply