Module

OpenImmersionSurjective.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.OpenImmersionSurjective

4 declarations indexed from sourceView source ↗

Module documentation

Fundamental groups and nonempty open immersions

For a normal locally Noetherian integral scheme, restriction to a nonempty open subscheme induces a surjection on etale fundamental groups. The proof uses the connected-object criterion for surjectivity: a connected finite-etale cover has integral source, so its pullback to a nonempty open remains connected.

Imports3

Imported by15

theorem

pullback_preservesTerminal

L30 ↗

AlgebraicGeometry.FiniteEtale.pullback_preservesTerminal

Source context 5 commands

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

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

Lean source · statement

theorem pullback_preservesTerminal {X U : Scheme.{u}}
    (j : U ⟶ X) :
    PreservesLimitsOfShape (Discrete PEmpty.{1}) (pullback j)

theorem

pullback_preservesLimitsOfShape_pempty

L92 ↗

AlgebraicGeometry.FiniteEtale.pullback_preservesLimitsOfShape_pempty

Documentation

Base change of finite-etale covers along an arbitrary scheme morphism preserves the terminal object. This is the empty-limit input needed by the Galois-category criteria for full faithfulness and surjectivity.

Source context 5 commands

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

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

Lean source · statement

theorem pullback_preservesLimitsOfShape_pempty
    {X U : Scheme.{u}} (j : U ⟶ X) :
    PreservesLimitsOfShape (Discrete PEmpty.{1}) (pullback j)

theorem

pullback_fullyFaithful_of_preserves_connected

L102 ↗

AlgebraicGeometry.FiniteEtale.pullback_fullyFaithful_of_preserves_connected

Documentation

If base change along a morphism of connected schemes preserves connected finite-etale covers, then that base-change functor is fully faithful.

This is the connected-object form of the Galois-category surjectivity criterion, applied to the actual geometric fiber comparison.

Source context 5 commands

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

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

Lean source · statement

theorem pullback_fullyFaithful_of_preserves_connected
    {X U : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace U]
    (j : U ⟶ X)
    (hconnected : ∀ W : FiniteEtale X, IsConnected W →
      IsConnected ((pullback j).obj W)) :
    Nonempty (pullback j).FullyFaithful

theorem

fundamentalGroupHom_surjective_of_isOpenImmersion

L122 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_surjective_of_isOpenImmersion

Documentation

A nonempty open immersion into a normal locally Noetherian integral scheme induces a surjection on etale fundamental groups.

Source context 5 commands

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

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

Lean source · statement

theorem fundamentalGroupHom_surjective_of_isOpenImmersion
    {X U : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] [Nonempty U]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶ U) :
    Function.Surjective (fundamentalGroupHom j ξ)

Module documentation

Fundamental groups and nonempty open immersions

Declarations

pullback_preservesTerminal

pullback_preservesLimitsOfShape_pempty

pullback_fullyFaithful_of_preserves_connected

fundamentalGroupHom_surjective_of_isOpenImmersion