Module

ArithmeticConnected.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticConnected

3 declarations indexed from sourceView source ↗

Module documentation

Arithmetic Connected

Connectedness after a separably closed constant extension descends to the base.

Imports1

Nyll.EtaleFundamentalGroups.GeometricFiber.ArithmeticSurjective

Imported by5

theorem

connectedSpace_of_connected_constantField

L20 ↗

AlgebraicGeometry.FiniteEtale.connectedSpace_of_connected_constantField

Documentation

Connectedness after a separably closed constant extension descends to the base.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem connectedSpace_of_connected_constantField
    (k L : Type u) [Field k] [Field L] [Algebra k L]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)] :
    ConnectedSpace X

theorem

isConnected_pullback_of_connected_constantField

L32 ↗

AlgebraicGeometry.FiniteEtale.isConnected_pullback_of_connected_constantField

Documentation

A connected finite étale cover of the field stays connected over a scheme whose extension to a separably closed constant field is connected.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem isConnected_pullback_of_connected_constantField
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsSepClosed L]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)]
    (W : FiniteEtale (Spec (.of k))) [IsConnected W] :
    IsConnected ((pullback f).obj W)

theorem

fundamentalGroupHom_surjective_of_connected_constantField

L71 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_surjective_of_connected_constantField

Documentation

The arithmetic fundamental-group map is surjective under exactly the geometric connectedness test needed for the arithmetic exact sequence.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem fundamentalGroupHom_surjective_of_connected_constantField
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsSepClosed L]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (.of Ω) ⟶ X) :
    Function.Surjective (fundamentalGroupHom f xi)

Module documentation

Arithmetic Connected

Declarations

connectedSpace_of_connected_constantField

isConnected_pullback_of_connected_constantField

fundamentalGroupHom_surjective_of_connected_constantField