Module

KummerSequence.lean

Nyll.EtaleCohomology.Classical.KummerSequence

11 declarations indexed from sourceView source ↗

Module documentation

Geometric local surjectivity in the actual étale Kummer sequence

A global unit has an nth root on an actual finite étale surjective cover when n is positive and invertible. We pull the explicit affine root cover back along the canonical map to the spectrum of global sections. Thus the construction works on arbitrary schemes, without choosing affine charts.

This proves epimorphy of the actual power morphism on the small étale multiplicative-group sheaf. The kernel gives the actual roots-of-unity sheaf and an actual short exact Kummer sequence.

Imports10

Nyll.EtaleCohomology.Classical.MultiplicativeGroup
Nyll.EtaleCohomology.Classical.FreeAbelianYoneda
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt
Nyll.EtaleCohomology.Classical.KummerRootCover
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.CategoryTheory.Sites.LocallySurjective
Mathlib.CategoryTheory.Sites.EpiMono
Mathlib.Algebra.Homology.ShortComplex.ShortExact
Mathlib.Algebra.Category.Grp.AB
Mathlib.AlgebraicGeometry.Sites.AffineEtale

Imported by1

Nyll.EtaleCohomology.Classical.All

theorem

exists_finiteEtale_unit_root

L40 ↗

EtaleCohomology.exists_finiteEtale_unit_root

Documentation

An actual unit on any scheme acquires an actual root on a finite étale surjective cover.

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_unit_root (X : Scheme.{u}) {n : ℕ}
    (hn : 0 < n) (hnX : IsUnit (n : Γ(X, ⊤))) (a : (Γ(X, ⊤) : Type u)ˣ) :
    ∃ (Y : Scheme.{u}) (f : Y ⟶ X), IsFiniteEtale f ∧ Function.Surjective f ∧
      (∀ x : X, f.finrank x = n) ∧ ∃ b : (Γ(Y, ⊤) : Type u)ˣ,
        b ^ n = Units.map f.appTop.hom.toMonoidHom a

theorem

exists_finiteEtale_power_lift

L72 ↗

EtaleCohomology.exists_finiteEtale_power_lift

Documentation

Local power lifts retain their actual finite étale cover and degree.

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_power_lift (X : Scheme.{u}) {n : ℕ}
    (hn : 0 < n) (hnX : IsUnit (n : Γ(X, ⊤))) (V : X.Etale)
    (s : (etaleMultiplicativeGroupSheaf X).obj.obj (op V)) :
    ∃ (W : X.Etale) (g : W ⟶ V), IsFiniteEtale g.left ∧
      Function.Surjective g.left ∧ (∀ x : V.left, g.left.finrank x = n) ∧
      ∃ t : (etaleMultiplicativeGroupSheaf X).obj.obj (op W),
        (etaleMultiplicativeGroupPower X n).hom.app (op W) t =
          (etaleMultiplicativeGroupSheaf X).obj.map g.op s

theorem

etaleMultiplicativeGroupPower_isLocallySurjective

L99 ↗

EtaleCohomology.etaleMultiplicativeGroupPower_isLocallySurjective

Documentation

The actual small-étale power morphism is locally surjective because the geometric root cover supplies local preimages.

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 etaleMultiplicativeGroupPower_isLocallySurjective (X : Scheme.{u})
    {n : ℕ} (hn : 0 < n) (hnX : IsUnit (n : Γ(X, ⊤))) :
    Presheaf.IsLocallySurjective X.smallEtaleTopology
      (etaleMultiplicativeGroupPower X n).hom

theorem

etaleMultiplicativeGroupPower_epi

L121 ↗

EtaleCohomology.etaleMultiplicativeGroupPower_epi

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 etaleMultiplicativeGroupPower_epi (X : Scheme.{u}) {n : ℕ}
    (hn : 0 < n) (hnX : IsUnit (n : Γ(X, ⊤))) :
    Epi (etaleMultiplicativeGroupPower X n)

abbrev

etaleRootsOfUnitySheaf

L130 ↗

EtaleCohomology.etaleRootsOfUnitySheaf

Documentation

The actual roots-of-unity sheaf, as the kernel of the actual power map.

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

abbrev etaleRootsOfUnitySheaf (X : Scheme.{u}) (n : ℕ) :
    Sheaf X.smallEtaleTopology AddCommGrpCat.{u}

abbrev

etaleKummerComplex

L135 ↗

EtaleCohomology.etaleKummerComplex

Documentation

The actual Kummer complex on the small étale site.

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

abbrev etaleKummerComplex (X : Scheme.{u}) (n : ℕ) :
    ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u})

theorem

etaleKummerComplex_shortExact

L141 ↗

EtaleCohomology.etaleKummerComplex_shortExact

Documentation

The actual Kummer sequence is short exact when n is invertible.

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 etaleKummerComplex_shortExact (X : Scheme.{u}) {n : ℕ}
    (hn : 0 < n) (hnX : IsUnit (n : Γ(X, ⊤))) :
    (etaleKummerComplex X n).ShortExact

def

etaleKummerBoundary

L150 ↗

EtaleCohomology.etaleKummerBoundary

Documentation

The actual Ext connecting class of a unit section in the Kummer sequence.

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 etaleKummerBoundary (X : Scheme.{u}) {n : ℕ} (hn : 0 < n)
    (hnX : IsUnit (n : Γ(X, ⊤))) (V : X.Etale)
    (s : (etaleMultiplicativeGroupSheaf X).obj.obj (op V)) :
    Sheaf.H'.{u} (etaleRootsOfUnitySheaf X n) 1 V

theorem

etaleKummerBoundary_eq_zero_iff

L160 ↗

EtaleCohomology.etaleKummerBoundary_eq_zero_iff

Documentation

The connecting class vanishes exactly when the unit already has a root on the given étale object.

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 etaleKummerBoundary_eq_zero_iff (X : Scheme.{u}) {n : ℕ}
    (hn : 0 < n) (hnX : IsUnit (n : Γ(X, ⊤))) (V : X.Etale)
    (s : (etaleMultiplicativeGroupSheaf X).obj.obj (op V)) :
    etaleKummerBoundary X hn hnX V s = 0 ↔
      ∃ t, (etaleMultiplicativeGroupPower X n).hom.app (op V) t = s

theorem

etaleKummerBoundary_restrict

L200 ↗

EtaleCohomology.etaleKummerBoundary_restrict

Documentation

Naturality uses the actual restriction map of 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 etaleKummerBoundary_restrict (X : Scheme.{u}) {n : ℕ}
    (hn : 0 < n) (hnX : IsUnit (n : Γ(X, ⊤))) {V W : X.Etale}
    (f : W ⟶ V) (s : (etaleMultiplicativeGroupSheaf X).obj.obj (op V)) :
    ((etaleRootsOfUnitySheaf X n).cohomologyPresheaf 1).map f.op
      (etaleKummerBoundary X hn hnX V s) =
        etaleKummerBoundary X hn hnX W
          ((etaleMultiplicativeGroupSheaf X).obj.map f.op s)

theorem

exists_degree_n_cover_killing_etaleKummerBoundary

L230 ↗

EtaleCohomology.exists_degree_n_cover_killing_etaleKummerBoundary

Documentation

The actual Kummer class is killed by an actual finite étale cover of degree exactly n, not merely by an unspecified local covering.

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_degree_n_cover_killing_etaleKummerBoundary
    (X : Scheme.{u}) {n : ℕ} (hn : 0 < n) (hnX : IsUnit (n : Γ(X, ⊤)))
    (V : X.Etale) (s : (etaleMultiplicativeGroupSheaf X).obj.obj (op V)) :
    ∃ (W : X.Etale) (g : W ⟶ V), IsFiniteEtale g.left ∧
      Function.Surjective g.left ∧ (∀ x : V.left, g.left.finrank x = n) ∧
      ((etaleRootsOfUnitySheaf X n).cohomologyPresheaf 1).map g.op
        (etaleKummerBoundary X hn hnX V s) = 0

Module documentation

Geometric local surjectivity in the actual étale Kummer sequence

Declarations