Module

FieldCohomologyEffacement.lean

Nyll.EtaleCohomology.Classical.FieldCohomologyEffacement

4 declarations indexed from sourceView source ↗

Module documentation

Finite étale effacement of actual field cohomology classes

Every positive-degree class in the actual Ext-defined cohomology presheaf over a field vanishes after a connected finite étale cover. The proof uses the actual injective presentation and the Ext long exact sequence. In degree one, the connecting class vanishes after locally lifting the corresponding section; higher degrees follow by dimension shifting and naturality of Ext composition. No field/Galois comparison or acyclicity assumption is introduced.

Imports4

Nyll.EtaleCohomology.Classical.FreeAbelianYoneda
Nyll.EtaleCohomology.Sites.FieldFiniteCover
Mathlib.CategoryTheory.Abelian.Injective.Resolution
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt

Imported by1

Nyll.EtaleCohomology.Classical.All

theorem

exists_finiteEtale_killing_cohomologyPresheaf_class_of_field

L33 ↗

EtaleCohomology.exists_finiteEtale_killing_cohomologyPresheaf_class_of_field

Documentation

Positive-degree actual sheaf cohomology classes over a field vanish after restriction to a connected finite étale surjective cover. Here restriction is precisely the map in mathlib's Ext-defined cohomology presheaf.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CategoryTheory.Abelian
namespace EtaleCohomology

Lean source · statement

theorem exists_finiteEtale_killing_cohomologyPresheaf_class_of_field
    (K : Type u) [Field K]
    (F : Sheaf (Spec (.of K)).smallEtaleTopology AddCommGrpCat.{u})
    (n : ℕ)
    (c : Sheaf.H'.{u} F (n + 1) (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 ∧
        (F.cohomologyPresheaf (n + 1)).map f.op c = 0

def

fieldEtaleTerminal

L90 ↗

EtaleCohomology.fieldEtaleTerminal

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CategoryTheory.Abelian
namespace EtaleCohomology

Lean source · statement

def fieldEtaleTerminal (K : Type u) [Field K] :
    IsTerminal (Scheme.Etale.mk (𝟙 (Spec (.of K))))

theorem

exists_finiteEtale_killing_sheafCohomology_class_of_field

L106 ↗

EtaleCohomology.exists_finiteEtale_killing_sheafCohomology_class_of_field

Documentation

Actual classical sheaf cohomology over a field has finite étale effacement in every positive degree, via its canonical terminal-object identification with the actual cohomology presheaf.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CategoryTheory.Abelian
namespace EtaleCohomology

Lean source · statement

theorem exists_finiteEtale_killing_sheafCohomology_class_of_field
    (K : Type u) [Field K]
    (F : Sheaf (Spec (.of K)).smallEtaleTopology AddCommGrpCat.{u})
    (n : ℕ) (c : Sheaf.H.{u} F (n + 1)) :
    ∃ (V : (Spec (.of K)).Etale)
      (f : V ⟶ Scheme.Etale.mk (𝟙 (Spec (.of K)))),
      IsFinite V.hom ∧ ConnectedSpace V.left ∧ Function.Surjective V.hom ∧
        (F.cohomologyPresheaf (n + 1)).map f.op
          (sheafCohomologyTerminalEquiv _ (fieldEtaleTerminal K) F (n + 1) c) = 0

theorem

exists_finiteGalois_killing_cohomologyPresheaf_class_of_field

L120 ↗

EtaleCohomology.exists_finiteGalois_killing_cohomologyPresheaf_class_of_field

Documentation

The effacing cover may be taken from the actual finite Galois intermediate fields of the algebraic closure in characteristic zero.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CategoryTheory.Abelian
namespace EtaleCohomology

Lean source · statement

theorem exists_finiteGalois_killing_cohomologyPresheaf_class_of_field
    (K : Type u) [Field K] [CharZero K]
    (F : Sheaf (Spec (.of K)).smallEtaleTopology AddCommGrpCat.{u})
    (n : ℕ)
    (c : Sheaf.H'.{u} F (n + 1) (Scheme.Etale.mk (𝟙 (Spec (.of K))))) :
    ∃ (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
      (f : finiteGaloisEtaleObject K E ⟶ Scheme.Etale.mk (𝟙 (Spec (.of K)))),
      (F.cohomologyPresheaf (n + 1)).map f.op c = 0

Module documentation

Finite étale effacement of actual field cohomology classes

Declarations

exists_finiteEtale_killing_cohomologyPresheaf_class_of_field

fieldEtaleTerminal

exists_finiteEtale_killing_sheafCohomology_class_of_field

exists_finiteGalois_killing_cohomologyPresheaf_class_of_field