Module

UnibranchOpenSurjective.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.UnibranchOpenSurjective

3 declarations indexed from sourceView source ↗

Module documentation

Nonempty opens of irreducible geometrically unibranch schemes

The local hypothesis uses the original definition through normalization of each stalk's reduction. Its actual geometric stalk has irreducible spectrum. Outside the nonempty open, the generic point lifts to a nonclosed prime of the ordinary stalk; faithful flatness lifts that point to the strict stalk. Thus the punctured strict stalk is nonempty and irreducible, hence connected.

The original finite-component local-connectedness criterion gives fully faithful finite étale restriction, and the actual fiber comparison gives surjectivity of the canonical fundamental group map. The scheme is arbitrary: normality, reducedness, Noetherianity, and quasi-compactness are not assumed.

Imports9

Nyll.EtaleFundamentalGroups.GeometricFiber.OpenImmersionSurjective
Nyll.EtaleFundamentalGroups.Purity.LocallyConnectedRestriction
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkUnibranchCriterion
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkFlat
Nyll.SchemeTheory.LocalGeometry.PuncturedSpectrum
Mathlib.AlgebraicGeometry.Stalk
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Mathlib.RingTheory.RingHom.FaithfullyFlat
Mathlib.Topology.Sober

Imported by2

theorem

puncturedGeometricStalk_nonempty_of_nonempty_open_complement

L42 ↗

AlgebraicGeometry.FiniteEtale.puncturedGeometricStalk_nonempty_of_nonempty_open_complement

Source context 6 commands

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

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

Lean source · statement

theorem puncturedGeometricStalk_nonempty_of_nonempty_open_complement
    {X : Scheme.{u}} [IrreducibleSpace X]
    (U : X.Opens) (hU : (U : Set X).Nonempty) (x : X) (hx : x ∉ U)
    {Ω : Type u} [Field Ω]
    (φ : X.presheaf.stalk x →+* Ω) [IsLocalHom φ] :
    Nonempty (Scheme.puncturedSpectrum
      (geometricStalk (Spec.map (CommRingCat.ofHom φ))))

def

nonemptyOpenPullbackFullyFaithful_of_geometricallyUnibranch

L77 ↗

AlgebraicGeometry.FiniteEtale.nonemptyOpenPullbackFullyFaithful_of_geometricallyUnibranch

Documentation

Restriction to any nonempty open of an irreducible geometrically unibranch scheme is fully faithful on the actual finite étale categories.

Source context 6 commands

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

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

Lean source · statement

def nonemptyOpenPullbackFullyFaithful_of_geometricallyUnibranch
    {X : Scheme.{u}} [IrreducibleSpace X]
    (hX : ∀ x : X, IsLocalRing.IsGeometricallyUnibranch (X.presheaf.stalk x))
    (U : X.Opens) (hU : (U : Set X).Nonempty) :
    (FiniteEtale.pullback U.ι).FullyFaithful

theorem

fundamentalGroupHom_surjective_nonemptyOpen_of_geometricallyUnibranch

L117 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_surjective_nonemptyOpen_of_geometricallyUnibranch

Documentation

The original open-immersion conclusion of Stacks 58.10.7: every nonempty open of an arbitrary irreducible geometrically unibranch scheme surjects onto its actual étale fundamental group.

Source context 6 commands

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

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

Lean source · statement

theorem fundamentalGroupHom_surjective_nonemptyOpen_of_geometricallyUnibranch
    {X : Scheme.{u}} [IrreducibleSpace X]
    (hX : ∀ x : X, IsLocalRing.IsGeometricallyUnibranch (X.presheaf.stalk x))
    (U : X.Opens) (hU : (U : Set X).Nonempty)
    {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ U.toScheme) :
    Function.Surjective (fundamentalGroupHom U.ι ξ)

Module documentation

Nonempty opens of irreducible geometrically unibranch schemes

Declarations

puncturedGeometricStalk_nonempty_of_nonempty_open_complement

nonemptyOpenPullbackFullyFaithful_of_geometricallyUnibranch

fundamentalGroupHom_surjective_nonemptyOpen_of_geometricallyUnibranch