NYLL
Module

FieldResolutionEffacement.lean

Nyll.EtaleCohomology.Classical.FieldResolutionEffacement
2 declarations indexed from sourceView source ↗

Module documentation

Finite étale local primitives for field cohomology

A closed global section of an exact complex of abelian sheaves over a field becomes an actual boundary after a connected finite étale cover. Applying this to an injective resolution supplies finite-cover local primitives in every positive degree. These are the actual resolutions computing classical sheaf cohomology, not an assumed field/Galois comparison.

Imports5
Imported by1

Declarations

theorem

exists_finiteEtale_primitive_of_exact_of_field

L31 ↗
EtaleCohomology.exists_finiteEtale_primitive_of_exact_of_field
Documentation

Exactness of abelian sheaves over a field supplies a finite étale local primitive for every closed global section.

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_primitive_of_exact_of_field
    (K : Type u) [Field K]
    (S : ShortComplex (Sheaf (Spec (.of K)).smallEtaleTopology AddCommGrpCat.{u}))
    (hS : S.Exact)
    (t : S.X₂.obj.obj (op (Scheme.Etale.mk (𝟙 (Spec (.of K))))))
    (ht : S.g.hom.app _ t = 0) :
    ∃ (V : (Spec (.of K)).Etale)
      (f : V ⟶ Scheme.Etale.mk (𝟙 (Spec (.of K)))),
      IsFinite V.hom ∧ ConnectedSpace V.left ∧ Function.Surjective V.hom ∧
        ∃ s : S.X₁.obj.obj (op V), S.f.hom.app (op V) s = S.X₂.obj.map f.op t
theorem

exists_finiteEtale_resolution_primitive_of_field

L75 ↗
EtaleCohomology.exists_finiteEtale_resolution_primitive_of_field
Documentation

Every positive-degree closed section of an actual injective resolution over a field acquires an actual primitive on a connected finite étale cover.

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_resolution_primitive_of_field
    (K : Type u) [Field K]
    (F : Sheaf (Spec (.of K)).smallEtaleTopology AddCommGrpCat.{u})
    (I : InjectiveResolution F) (n : ℕ)
    (t : (I.cocomplex.X (n + 1)).obj.obj
      (op (Scheme.Etale.mk (𝟙 (Spec (.of K))))))
    (ht : (I.cocomplex.d (n + 1) (n + 2)).hom.app _ t = 0) :
    ∃ (V : (Spec (.of K)).Etale)
      (f : V ⟶ Scheme.Etale.mk (𝟙 (Spec (.of K)))),
      IsFinite V.hom ∧ ConnectedSpace V.left ∧ Function.Surjective V.hom ∧
        ∃ s : (I.cocomplex.X n).obj.obj (op V),
          (I.cocomplex.d n (n + 1)).hom.app (op V) s =
            (I.cocomplex.X (n + 1)).obj.map f.op t

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.