Nyll.EtaleFundamentalGroups.GeometricFiber.GeometricallyConnectedSectionDescent

Module documentation

Descending an actual finite etale section along connected fibres

Full faithfulness of pullback for a flat finitely presented morphism with geometrically connected fibres descends an actual map into a finite etale cover of the base. The construction preserves its equality with the original map after composition, so it can be used on a chosen fibre section in the homotopy sequence.

theorem

exists_section_descent_of_flat_geometricallyConnected

L29 ↗

AlgebraicGeometry.FiniteEtale.exists_section_descent_of_flat_geometricallyConnected

Documentation

An actual section of a pulled-back finite etale cover descends along a flat morphism locally of finite presentation with connected geometric fibres.

Source context 4 commands

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

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

Lean source · statement

theorem exists_section_descent_of_flat_geometricallyConnected
    {X S : Scheme.{u}} (f : X ⟶ S) [Flat f] [LocallyOfFinitePresentation f]
    [GeometricallyConnected f] [ConnectedSpace S]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω] (xi : Spec (CommRingCat.of Ω) ⟶ X)
    (T : FiniteEtale S) (a : X ⟶ T.left) (ha : a ≫ T.hom = f) :
    ∃ t : S ⟶ T.left, t ≫ T.hom = 𝟙 S ∧ f ≫ t = a

Module documentation

Descending an actual finite etale section along connected fibres

Declarations

exists_section_descent_of_flat_geometricallyConnected