NYLL
Module

ConnectedReduction.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ConnectedReduction
1 declaration indexed from sourceView source ↗

Module documentation

Reducing essential surjectivity to connected finite-etale covers

A finite-etale cover of a connected scheme is a finite coproduct of connected covers. Since pullback preserves finite coproducts, extending every connected cover is therefore enough to extend an arbitrary (possibly disconnected) cover. This file records that categorical reduction for the actual finite-etale categories of schemes.

Imports2
Imported by3

Declarations

theorem

pullback_essSurj_of_connected

L34 ↗
AlgebraicGeometry.FiniteEtale.pullback_essSurj_of_connected
Documentation

Pullback along f is essentially surjective once every connected finite-etale cover of the connected source of f is in its essential image.

The conclusion includes disconnected covers: they are reconstructed as the finite coproduct of their connected summands.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem pullback_essSurj_of_connected
    {X Y : Scheme.{u}} [ConnectedSpace X] (f : X ⟶ Y)
    (h : ∀ Z : FiniteEtale X, IsConnected Z →
      ∃ W : FiniteEtale Y, Nonempty ((pullback f).obj W ≅ Z)) :
    (pullback f).EssSurj

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