Nyll.EtaleFundamentalGroups.GeometricFiber.UnibranchSurjective

Module documentation

Fundamental group surjections for geometrically unibranch schemes

Both original conclusions of Stacks Project, Lemma 58.10.7 (Tag 0BQI), for arbitrary irreducible geometrically unibranch schemes. The hypotheses use the normalization definition at every actual scheme stalk. Both maps are the existing fundamentalGroupHom attached to the literal open immersion and the literal generic residue-field morphism.

theorem

irreducible_geometricallyUnibranch_fundamentalGroup_surjections

L31 ↗

AlgebraicGeometry.FiniteEtale.irreducible_geometricallyUnibranch_fundamentalGroup_surjections

Documentation

Every nonempty open and the generic point of an irreducible geometrically unibranch scheme induce surjections on the actual étale fundamental groups.

Source context 4 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

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

Module documentation

Fundamental group surjections for geometrically unibranch schemes

Declarations

irreducible_geometricallyUnibranch_fundamentalGroup_surjections