NYLL
Module

ProperHomotopyNormal.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.ProperHomotopyNormal
2 declarations indexed from sourceView source ↗

Module documentation

Normality of the proper geometric-fibre image

The native Stein comparison identifies a connected cover with a pullback from the base whenever the cover has a section on one fibre. Over a separably closed fibre this proves the finite-cover criterion for normality of the actual image on fundamental groups.

Imports8
Imported by2

Declarations

theorem

essImage_pullback_of_connected_fiber_section

L34 ↗
AlgebraicGeometry.FiniteEtale.essImage_pullback_of_connected_fiber_section
Documentation

A connected finite etale cover with a section on one field-valued fibre comes from an actual finite etale cover of the base.

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 essImage_pullback_of_connected_fiber_section
    {X S : Scheme.{u}} [ConnectedSpace X]
    (f : X ⟶ S) [IsProper f] [Flat f] [LocallyOfFinitePresentation f]
    [GeometricallyReduced f]
    [GeometricallyConnected f] (Y : FiniteEtale X) [IsConnected Y]
    {K : Type u} [Field K] (s : Spec (.of K) ⟶ S)
    (a : Limits.pullback s f ⟶ Y.left)
    (ha : a ≫ Y.hom = Limits.pullback.snd s f) :
    (pullback f).essImage Y
theorem

fundamentalGroupHom_proper_geometricFiber_range_normal

L72 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_proper_geometricFiber_range_normal
Documentation

The image of the actual geometric-fibre fundamental group in a proper flat family with geometrically reduced connected fibres is normal.

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_range_normal
    {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 (Limits.pullback.snd s f) xi).toMonoidHom.range.Normal

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