Module

ConnectedFiberSections.lean

Nyll.SchemeTheory.FiniteEtale.ConnectedFiberSections

3 declarations indexed from sourceView source ↗

Module documentation

Descent of finite etale sections through connected fibres

An open surjection with connected fibres descends every clopen subset. Applied to the image of a section of a finite etale cover after base change, this constructs a clopen subscheme of the original cover. Its degree is one because degree one is detected after surjective base change. Its inverse therefore gives the actual descended section. No connectedness assumption on either scheme is needed.

Imports6

Mathlib.AlgebraicGeometry.Geometrically.Connected
Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.Topology.Connected.Clopen

Imported by2

theorem

exists_isClopen_preimage_eq_of_universallyOpen_geometricallyConnected

L40 ↗

AlgebraicGeometry.exists_isClopen_preimage_eq_of_universallyOpen_geometricallyConnected

Documentation

Clopen subsets descend along an open map with connected geometric fibres.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem exists_isClopen_preimage_eq_of_universallyOpen_geometricallyConnected
    {X S : Scheme.{u}} (f : X ⟶ S) [UniversallyOpen f] [GeometricallyConnected f]
    (V : Set X) (hV : IsClopen V) :
    ∃ U : Set S, IsClopen U ∧ f ⁻¹' U = V

theorem

isIso_of_isIso_pullback_of_surjective

L67 ↗

AlgebraicGeometry.isIso_of_isIso_pullback_of_surjective

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem isIso_of_isIso_pullback_of_surjective
    {X Y S : Scheme.{u}} (f : X ⟶ S) [Surjective f]
    (π : Y ⟶ S) [IsFinite π] [Etale π]
    (h : IsIso (pullback.snd π f)) : IsIso π

theorem

exists_section_descent_of_universallyOpen_geometricallyConnected

L80 ↗

AlgebraicGeometry.exists_section_descent_of_universallyOpen_geometricallyConnected

Documentation

Every section of a finite etale cover after a universally open base change with connected geometric fibres descends to the original base.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem exists_section_descent_of_universallyOpen_geometricallyConnected
    {X Y S : Scheme.{u}} (f : X ⟶ S) [UniversallyOpen f] [GeometricallyConnected f]
    (π : Y ⟶ S) [IsFinite π] [Etale π]
    (a : X ⟶ Y) (ha : a ≫ π = f) :
    ∃ t : S ⟶ Y, t ≫ π = 𝟙 S ∧ f ≫ t = a

Module documentation

Descent of finite etale sections through connected fibres

Declarations

exists_isClopen_preimage_eq_of_universallyOpen_geometricallyConnected

isIso_of_isIso_pullback_of_surjective

exists_section_descent_of_universallyOpen_geometricallyConnected