NYLL
Module

HomotopySequenceMaps.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.HomotopySequenceMaps
3 declarations indexed from sourceView source ↗

Module documentation

The maps in the homotopy sequence

For the actual geometric-fiber pullback, the two original fundamental-group maps have trivial composite. The proof factors their composite through the fundamental group of the separably closed field, preserving the canonical fiber comparisons and the equalities of geometric points.

For a universally open morphism with geometrically connected fibers, the map to the fundamental group of a connected base is surjective. This follows from connectedness of actual pullbacks of connected finite étale covers. The flat, locally finitely presented case is retained as a corollary. These are the composite and surjectivity inputs to Stacks Project, Proposition 58.15.2 (tag 0C0J); middle exactness is separate.

Imports8
Imported by4

Declarations

theorem

fundamentalGroupHom_geometricFiber_comp_eq_one

L42 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_geometricFiber_comp_eq_one
Documentation

The two original maps from a geometric fiber to its total space and base have trivial composite.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem fundamentalGroupHom_geometricFiber_comp_eq_one
    {X S : Scheme.{u}} (f : X ⟶ S)
    {L : Type u} [Field L] [IsSepClosed L] (s : Spec (.of L) ⟶ S)
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ Limits.pullback s f) :
    (fundamentalGroupHom f (xi ≫ Limits.pullback.snd s f)).comp
      (fundamentalGroupHom (Limits.pullback.snd s f) xi) = 1
theorem

fundamentalGroupHom_surjective_of_universallyOpen_geometricallyConnected

L80 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_surjective_of_universallyOpen_geometricallyConnected
Documentation

Universally open morphisms with geometrically connected fibers induce surjections on fundamental groups of connected bases.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem fundamentalGroupHom_surjective_of_universallyOpen_geometricallyConnected
    {X S : Scheme.{u}} (f : X ⟶ S)
    [UniversallyOpen f] [GeometricallyConnected f]
    [ConnectedSpace S]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ X) :
    Function.Surjective (fundamentalGroupHom f xi)
theorem

fundamentalGroupHom_surjective_of_flat_geometricallyConnected

L110 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_surjective_of_flat_geometricallyConnected
Documentation

Flat morphisms locally of finite presentation with geometrically connected fibers induce surjections on fundamental groups of connected bases.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem fundamentalGroupHom_surjective_of_flat_geometricallyConnected
    {X S : Scheme.{u}} (f : X ⟶ S)
    [Flat f] [LocallyOfFinitePresentation f] [GeometricallyConnected f]
    [ConnectedSpace S]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ X) :
    Function.Surjective (fundamentalGroupHom f xi)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.