Module

GenericPointOpenFull.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.GenericPointOpenFull

5 declarations indexed from sourceView source ↗

Module documentation

The generic-point map from full restriction to nonempty opens

For an irreducible scheme, the residue field of the generic point maps surjectively onto the spectrum of its actual stalk. The map is a closed immersion and hence a universal homeomorphism, even for nonreduced schemes. An etale section over the generic residue field therefore lifts to the actual stalk and spreads to an open neighborhood by the proved filtered stalk finite-presentation descent. Fullness of restriction to that open then gives a global section. The Galois-category section criterion gives the original fundamental-group surjection and full faithfulness.

The nonempty-open fullness premise is an ordinary intermediate implication; it is supplied by the geometric-unibranch theorem in the original endpoint.

Imports5

Nyll.SchemeTheory.Descent.StalkSpreadingOpen
Nyll.SchemeTheory.Etale.UniversalHomeomorphismSections
Nyll.EtaleFundamentalGroups.GeometricFiber.OpenImmersionSurjective
Mathlib.AlgebraicGeometry.FunctionField
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Imported by2

theorem

specMap_residue_genericPoint_surjective

L40 ↗

AlgebraicGeometry.FiniteEtale.specMap_residue_genericPoint_surjective

Documentation

The generic residue field covers the entire spectrum of the generic stalk, without a reducedness assumption.

Source context 5 commands

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

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

Lean source · statement

theorem specMap_residue_genericPoint_surjective
    (X : Scheme.{u}) [IrreducibleSpace X] :
    Surjective (Spec.map (X.residue (genericPoint X)))

theorem

exists_section_of_full_pullback

L60 ↗

AlgebraicGeometry.FiniteEtale.exists_section_of_full_pullback

Source context 5 commands

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

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

Lean source · statement

theorem exists_section_of_full_pullback
    {X T : Scheme.{u}} (j : T ⟶ X) [(pullback j).Full]
    (W : FiniteEtale X) (a : T ⟶ W.left) (ha : a ≫ W.hom = j) :
    ∃ b : X ⟶ W.left, b ≫ W.hom = 𝟙 X

theorem

exists_section_of_genericPoint_of_nonemptyOpenFull

L76 ↗

AlgebraicGeometry.FiniteEtale.exists_section_of_genericPoint_of_nonemptyOpenFull

Documentation

If restriction to every nonempty open is full, a finite-etale cover with a section at the generic residue field has a global section.

Source context 5 commands

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

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

Lean source · statement

theorem exists_section_of_genericPoint_of_nonemptyOpenFull
    {X : Scheme.{u}} [IrreducibleSpace X]
    (hFull : ∀ (U : X.Opens), (U : Set X).Nonempty → (pullback U.ι).Full)
    (W : FiniteEtale X)
    (a : Spec (X.residueField (genericPoint X)) ⟶ W.left)
    (ha : a ≫ W.hom = X.fromSpecResidueField (genericPoint X)) :
    ∃ b : X ⟶ W.left, b ≫ W.hom = 𝟙 X

theorem

genericPoint_fundamentalGroupHom_surjective_of_nonemptyOpenFull

L98 ↗

AlgebraicGeometry.FiniteEtale.genericPoint_fundamentalGroupHom_surjective_of_nonemptyOpenFull

Documentation

The literal generic-point morphism induces a surjection on fundamental groups whenever all nonempty-open finite-etale restrictions are full. The chosen geometric point of the generic residue field is retained.

Source context 5 commands

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

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

Lean source · statement

theorem genericPoint_fundamentalGroupHom_surjective_of_nonemptyOpenFull
    {X : Scheme.{u}} [IrreducibleSpace X]
    (hFull : ∀ (U : X.Opens), (U : Set X).Nonempty → (pullback U.ι).Full)
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶ Spec (X.residueField (genericPoint X))) :
    Function.Surjective
      (fundamentalGroupHom (X.fromSpecResidueField (genericPoint X)) ξ)

def

genericPointPullbackFullyFaithful_of_nonemptyOpenFull

L139 ↗

AlgebraicGeometry.FiniteEtale.genericPointPullbackFullyFaithful_of_nonemptyOpenFull

Documentation

Full faithfulness of the actual generic-residue-field pullback follows from full restriction to all nonempty opens, with no normality or reducedness assumption.

Source context 5 commands

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

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

Lean source · statement

def genericPointPullbackFullyFaithful_of_nonemptyOpenFull
    {X : Scheme.{u}} [IrreducibleSpace X]
    (hFull : ∀ (U : X.Opens), (U : Set X).Nonempty → (pullback U.ι).Full) :
    (pullback (X.fromSpecResidueField (genericPoint X))).FullyFaithful

Module documentation

The generic-point map from full restriction to nonempty opens

Declarations

specMap_residue_genericPoint_surjective

exists_section_of_full_pullback

exists_section_of_genericPoint_of_nonemptyOpenFull

genericPoint_fundamentalGroupHom_surjective_of_nonemptyOpenFull

genericPointPullbackFullyFaithful_of_nonemptyOpenFull