Module

RegularBoundarySurjective.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.RegularBoundarySurjective

3 declarations indexed from sourceView source ↗

Module documentation

Connectedness across a regular Cartier boundary

Regularity is required only along the boundary. Applying connectedness of Cartier complements to each connected finite étale cover proves the surjectivity assertion of Lemma 1.1 by the connected-object criterion.

Imports7

Imported by7

theorem

boundaryComplement_connectedSpace

L35 ↗

AlgebraicGeometry.FiniteEtale.boundaryComplement_connectedSpace

Documentation

Removing a Cartier boundary with regular ambient stalks preserves connectedness.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [ConnectedSpace X] [IsLocallyNoetherian X]

Lean source · statement

theorem boundaryComplement_connectedSpace
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport) :
    ConnectedSpace D.1.supportComplement

theorem

boundaryComplement_pullback_isConnected

L44 ↗

AlgebraicGeometry.FiniteEtale.boundaryComplement_pullback_isConnected

Documentation

Connected finite étale covers remain connected on the boundary complement.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [ConnectedSpace X] [IsLocallyNoetherian X]

Lean source · statement

theorem boundaryComplement_pullback_isConnected
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    [ConnectedSpace D.1.supportComplement]
    (W : FiniteEtale X) [IsConnected W] :
    IsConnected ((pullback D.1.supportComplement.ι).obj W)

theorem

boundaryComplement_fundamentalGroupHom_surjective

L65 ↗

AlgebraicGeometry.FiniteEtale.boundaryComplement_fundamentalGroupHom_surjective

Documentation

The morphism on fundamental groups in Lemma 1.1 is surjective.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [ConnectedSpace X] [IsLocallyNoetherian X]

Lean source · statement

theorem boundaryComplement_fundamentalGroupHom_surjective
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    [ConnectedSpace D.1.supportComplement]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ D.1.supportComplement) :
    Function.Surjective (fundamentalGroupHom D.1.supportComplement.ι point)

Module documentation

Connectedness across a regular Cartier boundary

Declarations

boundaryComplement_connectedSpace

boundaryComplement_pullback_isConnected

boundaryComplement_fundamentalGroupHom_surjective