Module

SmoothConnectedCovers.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.SmoothConnectedCovers

1 declaration indexed from sourceView source ↗

Module documentation

Connected finite étale covers of smooth arithmetic schemes

The arithmetic constant-field theorem, applied to the actual finite étale cover, gives geometric integrality of its generic fiber. All connectedness, integrality, normality and characteristic-zero inputs are constructed here from smoothness and the given geometric connectedness of the base generic fiber.

Imports6

Imported by2

theorem

geometricallyIntegral_genericFiber_of_connected_finiteEtale_over_smooth_integers

L32 ↗

EtaleFundamentalGroups.geometricallyIntegral_genericFiber_of_connected_finiteEtale_over_smooth_integers

Documentation

A connected finite étale cover of a smooth surjective finite-type arithmetic scheme with geometrically connected generic fiber has geometrically integral generic fiber.

Source context 3 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace EtaleFundamentalGroups

Lean source · statement

theorem geometricallyIntegral_genericFiber_of_connected_finiteEtale_over_smooth_integers
    {E : Scheme} (p : E ⟶ Spec (CommRingCat.of ℤ))
    [Smooth p] [QuasiCompact p] [Surjective p]
    [GeometricallyConnected
      (p.fiberToSpecResidueField (genericPoint (Spec (CommRingCat.of ℤ))))]
    (T : FiniteEtale E) [ConnectedSpace T.left] :
    GeometricallyIntegral
      ((T.hom ≫ p).fiberToSpecResidueField (genericPoint (Spec (CommRingCat.of ℤ))))

Module documentation

Connected finite étale covers of smooth arithmetic schemes

Declarations

geometricallyIntegral_genericFiber_of_connected_finiteEtale_over_smooth_integers