Module

FieldFiniteCover.lean

Nyll.EtaleCohomology.Sites.FieldFiniteCover

4 declarations indexed from sourceView source ↗

Module documentation

Finite étale refinements over a field

Every covering sieve of the terminal object of the small étale site of a field contains a connected finite étale surjective cover. We select an actual spectrum of a finite separable field from the established geometric decomposition of an étale neighborhood.

Consequently an epimorphism of abelian sheaves admits a lift of any given global section after an actual connected finite étale cover. This is the local lifting input for comparing field étale cohomology with finite Galois stages; no cohomology comparison is assumed.

Imports8

Nyll.EtaleCohomology.Sites.ConstantPresentation
Nyll.SchemeTheory.Etale.OverField.Decomposition
Mathlib.RingTheory.Etale.Field
Mathlib.CategoryTheory.Sites.EpiMono
Mathlib.CategoryTheory.Sites.LocallySurjective
Mathlib.Algebra.Category.Grp.AB
Mathlib.FieldTheory.Galois.GaloisClosure
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Imported by4

theorem

exists_finiteEtale_mem_covering_sieve_of_field

L38 ↗

EtaleCohomology.exists_finiteEtale_mem_covering_sieve_of_field

Documentation

An arbitrary étale covering sieve over a field has a connected finite étale surjective refinement.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

theorem exists_finiteEtale_mem_covering_sieve_of_field
    (K : Type u) [Field K]
    (S : Sieve (Scheme.Etale.mk (𝟙 (Spec (.of K)))))
    (hS : S ∈ (Spec (.of K)).smallEtaleTopology _) :
    ∃ (V : (Spec (.of K)).Etale)
      (f : V ⟶ Scheme.Etale.mk (𝟙 (Spec (.of K)))),
      IsFinite V.hom ∧ ConnectedSpace V.left ∧
        Function.Surjective V.hom ∧ S f

theorem

exists_finiteEtale_lift_sheaf_epi_section_of_field

L80 ↗

EtaleCohomology.exists_finiteEtale_lift_sheaf_epi_section_of_field

Documentation

A global section of an abelian sheaf locally lifts through an epimorphism on an actual connected finite étale cover of the field.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

theorem exists_finiteEtale_lift_sheaf_epi_section_of_field
    (K : Type u) [Field K]
    {F G : Sheaf (Spec (.of K)).smallEtaleTopology AddCommGrpCat.{u}}
    (η : F ⟶ G) [Epi η]
    (t : G.obj.obj (op (Scheme.Etale.mk (𝟙 (Spec (.of K)))))) :
    ∃ (V : (Spec (.of K)).Etale)
      (f : V ⟶ Scheme.Etale.mk (𝟙 (Spec (.of K)))),
      IsFinite V.hom ∧ ConnectedSpace V.left ∧ Function.Surjective V.hom ∧
        ∃ s : F.obj.obj (op V), η.hom.app (op V) s = G.obj.map f.op t

def

finiteGaloisEtaleObject

L99 ↗

EtaleCohomology.finiteGaloisEtaleObject

Documentation

The actual spectrum of a finite Galois intermediate field, as an object of the small étale site.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

def finiteGaloisEtaleObject (K : Type u) [Field K]
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K)) :
    (Spec (.of K)).Etale

theorem

exists_finiteGalois_mem_covering_sieve_of_field

L115 ↗

EtaleCohomology.exists_finiteGalois_mem_covering_sieve_of_field

Documentation

In characteristic zero, the refinement can be chosen inside the actual algebraic closure, finite and Galois over the original field.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

theorem exists_finiteGalois_mem_covering_sieve_of_field
    (K : Type u) [Field K] [CharZero K]
    (S : Sieve (Scheme.Etale.mk (𝟙 (Spec (.of K)))))
    (hS : S ∈ (Spec (.of K)).smallEtaleTopology _) :
    ∃ (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
      (f : finiteGaloisEtaleObject K E ⟶ Scheme.Etale.mk (𝟙 (Spec (.of K)))),
      S f

Module documentation

Finite étale refinements over a field

Declarations

exists_finiteEtale_mem_covering_sieve_of_field

exists_finiteEtale_lift_sheaf_epi_section_of_field

finiteGaloisEtaleObject

exists_finiteGalois_mem_covering_sieve_of_field