Module

AlgebraicallyClosedConstantExtension.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.AlgebraicallyClosedConstantExtension

1 declaration indexed from sourceView source ↗

Module documentation

Full faithfulness under algebraically closed constant extension

For any scheme over an algebraically closed field, every extension of constants induces a fully faithful functor on finite etale covers. The extension may be transcendental and its target need not be algebraically closed. No properness or finite-type assumption is needed for this part of the comparison.

The field extension is geometrically irreducible and universally open. Actual descent of finite etale sections along its base change supplies fullness, without a connectedness assumption or a chosen geometric point.

This supplies full faithfulness in Stacks 0A49. Essential surjectivity for proper schemes is separate.

Imports3

Imported by1

Nyll.EtaleFundamentalGroups.GeometricFiber.All

def

pullbackFullyFaithful_of_isAlgClosed_constant_extension

L38 ↗

AlgebraicGeometry.FiniteEtale.pullbackFullyFaithful_of_isAlgClosed_constant_extension

Documentation

Finite etale covers and their morphisms are fully faithfully preserved by any extension of an algebraically closed constant field.

Source context 4 commands

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

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

Lean source · statement

def pullbackFullyFaithful_of_isAlgClosed_constant_extension
    (k K : Type u) [Field k] [IsAlgClosed k] [Field K] [Algebra k K]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of k)) :
    (pullback (Limits.pullback.fst f
      (Spec.map (CommRingCat.ofHom (algebraMap k K))))).FullyFaithful

Module documentation

Full faithfulness under algebraically closed constant extension

Declarations

pullbackFullyFaithful_of_isAlgClosed_constant_extension