Module

OpenImmersionExtensions.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.OpenImmersionExtensions

6 declarations indexed from sourceView source ↗

Module documentation

Fundamental-group equivalences from finite-etale extensions

For a nonempty open subscheme of a normal locally Noetherian integral scheme, the induced map on etale fundamental groups is always surjective. If every finite-etale cover of the open subscheme actually extends across the open immersion, pullback is essentially surjective and the same map is injective. Compact-to-Hausdorff continuity then upgrades that specific map to a continuous multiplicative equivalence.

Imports4

Imported by2

def

fundamentalGroupEquivOfOpenImmersionEssSurj

L35 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivOfOpenImmersionEssSurj

Documentation

Essential surjectivity of finite-etale pullback across a nonempty open immersion upgrades the induced fundamental-group homomorphism itself to a continuous multiplicative equivalence.

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 · statement

def fundamentalGroupEquivOfOpenImmersionEssSurj
    {U X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] [Nonempty U]
    (hEss : (pullback j).EssSurj)
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ U) :
    π₁ᵉᵗ(xi) ≃ₜ* π₁ᵉᵗ(xi ≫ j)

theorem

fundamentalGroupEquivOfOpenImmersionEssSurj_apply

L54 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivOfOpenImmersionEssSurj_apply

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 · statement

theorem fundamentalGroupEquivOfOpenImmersionEssSurj_apply
    {U X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] [Nonempty U]
    (hEss : (pullback j).EssSurj)
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ U) (gamma : π₁ᵉᵗ(xi)) :
    fundamentalGroupEquivOfOpenImmersionEssSurj j hEss xi gamma =
      fundamentalGroupHom j xi gamma

def

fundamentalGroupEquivOfOpenImmersionGaloisExtensions

L68 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivOfOpenImmersionGaloisExtensions

Documentation

Actual extensions of all finite-etale Galois covers already suffice to identify the two fundamental groups. This avoids first reconstructing essential surjectivity for arbitrary disconnected covers.

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 · statement

def fundamentalGroupEquivOfOpenImmersionGaloisExtensions
    {U X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] [Nonempty U] [ConnectedSpace U]
    (extend : ∀ (W : FiniteEtale U) (_hW : IsGalois W),
      Σ Z : FiniteEtale X, (pullback j).obj Z ≅ W)
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ U) :
    π₁ᵉᵗ(xi) ≃ₜ* π₁ᵉᵗ(xi ≫ j)

theorem

fundamentalGroupEquivOfOpenImmersionGaloisExtensions_apply

L86 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivOfOpenImmersionGaloisExtensions_apply

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 · statement

theorem fundamentalGroupEquivOfOpenImmersionGaloisExtensions_apply
    {U X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] [Nonempty U] [ConnectedSpace U]
    (extend : ∀ (W : FiniteEtale U) (_hW : IsGalois W),
      Σ Z : FiniteEtale X, (pullback j).obj Z ≅ W)
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ U) (gamma : π₁ᵉᵗ(xi)) :
    fundamentalGroupEquivOfOpenImmersionGaloisExtensions
        j extend xi gamma =
      fundamentalGroupHom j xi gamma

def

fundamentalGroupEquivOfOpenImmersionExtensions

L102 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivOfOpenImmersionExtensions

Documentation

Actual extension objects for every finite-etale cover of the open subscheme provide the essential-surjectivity input and hence identify 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 · statement

def fundamentalGroupEquivOfOpenImmersionExtensions
    {U X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] [Nonempty U]
    (extend : ∀ W : FiniteEtale U,
      Σ Z : FiniteEtale X, (pullback j).obj Z ≅ W)
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ U) :
    π₁ᵉᵗ(xi) ≃ₜ* π₁ᵉᵗ(xi ≫ j)

theorem

fundamentalGroupEquivOfOpenImmersionExtensions_apply

L118 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupEquivOfOpenImmersionExtensions_apply

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 · statement

theorem fundamentalGroupEquivOfOpenImmersionExtensions_apply
    {U X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] [Nonempty U]
    (extend : ∀ W : FiniteEtale U,
      Σ Z : FiniteEtale X, (pullback j).obj Z ≅ W)
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ U) (gamma : π₁ᵉᵗ(xi)) :
    fundamentalGroupEquivOfOpenImmersionExtensions j extend xi gamma =
      fundamentalGroupHom j xi gamma

Module documentation

Fundamental-group equivalences from finite-etale extensions

Declarations

fundamentalGroupEquivOfOpenImmersionEssSurj

fundamentalGroupEquivOfOpenImmersionEssSurj_apply

fundamentalGroupEquivOfOpenImmersionGaloisExtensions

fundamentalGroupEquivOfOpenImmersionGaloisExtensions_apply

fundamentalGroupEquivOfOpenImmersionExtensions

fundamentalGroupEquivOfOpenImmersionExtensions_apply