NYLL
Module

RationalPointLift.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.RationalPointLift
2 declarations indexed from sourceView source ↗

Module documentation

Actual rational and closed points above points of a finite étale cover

Imports3
Imported by2

Declarations

theorem

exists_rationalPoint_lift

L23 ↗
AlgebraicGeometry.FiniteEtale.exists_rationalPoint_lift
Documentation

A nonempty finite étale cover of a connected scheme has a rational point over each geometric point with algebraically closed residue field.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem exists_rationalPoint_lift
    {K : Type u} [Field K] [IsAlgClosed K]
    {X : Scheme.{u}} [PreconnectedSpace X]
    (W : FiniteEtale X) [Nonempty W.left]
    (x : Spec (.of K) ⟶ X) :
    ∃ y : Spec (.of K) ⟶ W.left, y ≫ W.hom = x
theorem

exists_closedPoint_above

L43 ↗
AlgebraicGeometry.FiniteEtale.exists_closedPoint_above
Documentation

For a curve over an algebraically closed field, a finite étale cover has an actual closed point over every closed point of the base.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem exists_closedPoint_above
    {K : Type u} [Field K] [IsAlgClosed K]
    {X : Scheme.{u}} [PreconnectedSpace X]
    (c : X ⟶ Spec (.of K)) [LocallyOfFiniteType c]
    (W : FiniteEtale X) [Nonempty W.left] (x : closedPoints X) :
    ∃ y : closedPoints W.left, W.hom y.val = x.val

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