NYLL
Module

Connected.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.Connected
5 declarations indexed from sourceView source ↗

Module documentation

Connected finite etale covers

For a connected base scheme, categorical connectedness in the Galois category of finite etale covers agrees with connectedness of the underlying source scheme. This file records both directions, together with the nonemptiness comparison used in their proofs.

Mathlib provides the abstract Galois-category notion IsConnected and the topological class ConnectedSpace, but currently has no finite-etale scheme bridge between them.

Imports1
Imported by35

Declarations

theorem

pullback_obj_nonempty

L35 ↗
AlgebraicGeometry.FiniteEtale.pullback_obj_nonempty
Documentation

Pulling a nonempty finite etale cover of a preconnected base back to a nonempty scheme again has nonempty source.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [ConnectedSpace X]
Lean source · statement
theorem pullback_obj_nonempty {S T : Scheme.{u}} [PreconnectedSpace T]
    (f : S ⟶ T) [Nonempty S] (Y : FiniteEtale T) [Nonempty Y.left] :
    Nonempty ((pullback f).obj Y).left
theorem

notInitial_of_nonempty_left

L53 ↗
AlgebraicGeometry.FiniteEtale.notInitial_of_nonempty_left
Documentation

A nonempty finite etale cover of a connected scheme is not initial in the finite etale category.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [ConnectedSpace X]
Lean source · statement
theorem notInitial_of_nonempty_left (Y : FiniteEtale X) [Nonempty Y.left] :
    IsInitial Y → False
theorem

nonempty_left_of_notInitial

L77 ↗
AlgebraicGeometry.FiniteEtale.nonempty_left_of_notInitial
Documentation

A finite etale cover that is not initial has a nonempty source scheme.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [ConnectedSpace X]
Lean source · statement
theorem nonempty_left_of_notInitial (Y : FiniteEtale X)
    (hY : IsInitial Y → False) : Nonempty Y.left
theorem

connectedSpace_left_of_isConnected

L91 ↗
AlgebraicGeometry.FiniteEtale.connectedSpace_left_of_isConnected
Documentation

A categorically connected finite etale cover has connected source scheme.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [ConnectedSpace X]
Lean source · statement
theorem connectedSpace_left_of_isConnected (Y : FiniteEtale X)
    [IsConnected Y] : ConnectedSpace Y.left
theorem

isConnected_of_connectedSpace_left

L143 ↗
AlgebraicGeometry.FiniteEtale.isConnected_of_connectedSpace_left
Documentation

A finite etale cover with connected source scheme is categorically connected.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X : Scheme.{u}} [ConnectedSpace X]
Lean source · statement
theorem isConnected_of_connectedSpace_left (Y : FiniteEtale X)
    [ConnectedSpace Y.left] : IsConnected Y

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