Module

ProperHomotopyExact.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.ProperHomotopyExact

1 declaration indexed from sourceView source ↗

Module documentation

The proper homotopy sequence

The kernel at the middle term is the actual image of the geometric-fibre fundamental group. Stein descent supplies descent of connected covers; finite connected-component decomposition then supplies the categorical exactness criterion. Normality and compactness identify the resulting closed normal closure with the original image.

Imports8

Imported by2

theorem

fundamentalGroupHom_proper_geometricFiber_ker_eq_range

L36 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_proper_geometricFiber_ker_eq_range

Documentation

Exactness at the middle term of the actual fundamental-group sequence for a proper flat finitely presented family with geometrically reduced connected fibres over an arbitrary connected base (Stacks Project Tag 0C0J).

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_proper_geometricFiber_ker_eq_range
    {X S : Scheme.{u}} [ConnectedSpace S]
    (f : X ⟶ S) [IsProper f] [Flat f] [LocallyOfFinitePresentation f]
    [GeometricallyReduced f]
    [GeometricallyConnected f]
    {K : Type u} [Field K] [IsSepClosed K] (s : Spec (.of K) ⟶ S)
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ Limits.pullback s f) :
    (fundamentalGroupHom f (xi ≫ Limits.pullback.snd s f)).toMonoidHom.ker =
      (fundamentalGroupHom (Limits.pullback.snd s f) xi).toMonoidHom.range

Module documentation

The proper homotopy sequence

Declarations

fundamentalGroupHom_proper_geometricFiber_ker_eq_range