NYLL
Module

FieldHilbert90.lean

Nyll.EtaleCohomology.Classical.FieldHilbert90
3 declarations indexed from sourceView source ↗

Module documentation

Hilbert 90 for actual etale sheaf extensions over a field

A lift over a finite Galois field extension of a Galois-invariant quotient section can be corrected to an invariant lift when the kernel is the actual unit sheaf. The correction is obtained from its actual difference cocycle, the proved equivariance of unit sections, and Noether's Hilbert 90.

Imports6
Imported by1

Declarations

theorem

exists_fieldGalois_invariant_lift

L32 ↗
EtaleCohomology.exists_fieldGalois_invariant_lift
Documentation

Hilbert 90 corrects a local lift in an actual short exact sequence with unit-sheaf kernel to a Galois-invariant lift of the same quotient section.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open AlgebraicGeometry.FiniteEtale
namespace EtaleCohomology
Lean source · statement
theorem exists_fieldGalois_invariant_lift
    (K L : Type u) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    {B Q : Sheaf (Spec (.of K)).smallEtaleTopology AddCommGrpCat.{u}}
    (i : etaleMultiplicativeGroupSheaf (Spec (.of K)) ⟶ B) (p : B ⟶ Q)
    (hz : i ≫ p = 0) (hS : (ShortComplex.mk i p hz).ShortExact)
    (e : B.obj.obj (op ((finiteEtaleInclusion (Spec (.of K))).obj
      (FiniteEtale.mk (ξ K L)))))
    (he : ∀ σ : Gal(L/K),
      (fieldGaloisSheafAction K L Q σ).hom
        (p.hom.app (op ((finiteEtaleInclusion (Spec (.of K))).obj
          (FiniteEtale.mk (ξ K L)))) e) =
        p.hom.app (op ((finiteEtaleInclusion (Spec (.of K))).obj
          (FiniteEtale.mk (ξ K L)))) e) :
    ∃ e' : B.obj.obj (op ((finiteEtaleInclusion (Spec (.of K))).obj
        (FiniteEtale.mk (ξ K L)))),
      p.hom.app (op ((finiteEtaleInclusion (Spec (.of K))).obj
        (FiniteEtale.mk (ξ K L)))) e' =
          p.hom.app (op ((finiteEtaleInclusion (Spec (.of K))).obj
            (FiniteEtale.mk (ξ K L)))) e ∧
      ∀ σ : Gal(L/K), (fieldGaloisSheafAction K L B σ).hom e' = e'
theorem

exists_section_lift_of_units_kernel_of_field

L131 ↗
EtaleCohomology.exists_section_lift_of_units_kernel_of_field
Documentation

Over a characteristic-zero field, global sections of an actual short exact sequence with unit-sheaf kernel surject onto quotient sections. A finite Galois local lift is corrected by Hilbert 90 and then descended.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open AlgebraicGeometry.FiniteEtale
namespace EtaleCohomology
Lean source · statement
theorem exists_section_lift_of_units_kernel_of_field
    (K : Type u) [Field K] [CharZero K]
    {B Q : Sheaf (Spec (.of K)).smallEtaleTopology AddCommGrpCat.{u}}
    (i : etaleMultiplicativeGroupSheaf (Spec (.of K)) ⟶ B) (p : B ⟶ Q)
    (hz : i ≫ p = 0) (hS : (ShortComplex.mk i p hz).ShortExact)
    (q : Q.obj.obj (op (Scheme.Etale.mk (𝟙 (Spec (.of K)))))) :
    ∃ b : B.obj.obj (op (Scheme.Etale.mk (𝟙 (Spec (.of K))))),
      p.hom.app (op (Scheme.Etale.mk (𝟙 (Spec (.of K))))) b = q
theorem

etaleMultiplicativeGroup_H1_eq_zero_of_field

L195 ↗
EtaleCohomology.etaleMultiplicativeGroup_H1_eq_zero_of_field
Documentation

The actual derived etale H1 of Gm over a characteristic-zero field vanishes. Its extension representative is split using the proved geometric Galois descent and Hilbert 90, not an assumed comparison with Galois H1.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open AlgebraicGeometry.FiniteEtale
namespace EtaleCohomology
Lean source · statement
theorem etaleMultiplicativeGroup_H1_eq_zero_of_field
    (K : Type u) [Field K] [CharZero K]
    (a : Sheaf.H.{u} (etaleMultiplicativeGroupSheaf (Spec (.of K))) 1) : a = 0

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