Module

AdicH1Comparison.lean

Nyll.EtaleFundamentalGroups.Cohomology.AdicH1Comparison

7 declarations indexed from sourceView source ↗

Module documentation

Classical ℓ-adic H¹ and compatible finite characters

The finite-coefficient comparison is compatible with reduction. It therefore identifies classical ℓ-adic H¹, defined on the ordinary étale site, with compatible systems of continuous characters into ℤ/ℓ^(n+1)ℤ. Neither pro-étale cohomology nor an unproved limit comparison is used.

Imports2

Imported by2

abbrev

finiteLevelCharacters

L31 ↗

EtaleFundamentalGroups.Cohomology.finiteLevelCharacters

Documentation

Continuous finite cyclic characters, with the character group written additively.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)

Lean source · statement

abbrev finiteLevelCharacters (ℓ n : ℕ) : Type (u + 1)

instance

finiteLevelCharactersAddCommGroup

L36 ↗

EtaleFundamentalGroups.Cohomology.finiteLevelCharactersAddCommGroup

Documentation

Pointwise addition uses the same discrete topology on finite coefficients.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)

Lean source · statement

instance finiteLevelCharactersAddCommGroup (ℓ n : ℕ) :
    AddCommGroup (finiteLevelCharacters ξ ℓ n)

def

finiteLevelCharacterReduction

L44 ↗

EtaleFundamentalGroups.Cohomology.finiteLevelCharacterReduction

Documentation

Reduction of the values of a finite continuous character.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)

Lean source · statement

def finiteLevelCharacterReduction (ℓ n : ℕ) :
    finiteLevelCharacters ξ ℓ (n + 1) →+ finiteLevelCharacters ξ ℓ n

def

compatibleFiniteCharacters

L64 ↗

EtaleFundamentalGroups.Cohomology.compatibleFiniteCharacters

Documentation

Compatible families of actual finite continuous characters.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)

Lean source · statement

def compatibleFiniteCharacters (ℓ : ℕ) :
    AddSubgroup (∀ n, finiteLevelCharacters ξ ℓ n)

def

levelEquiv

L71 ↗

EtaleFundamentalGroups.Cohomology.levelEquiv

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
variable (ℓ : ℕ) [Fact ℓ.Prime]

Lean source · statement

def levelEquiv (n : ℕ) :
    finiteLevelCohomology X ℓ n 1 ≃+ finiteLevelCharacters ξ ℓ n

theorem

levelEquiv_reduction

L76 ↗

EtaleFundamentalGroups.Cohomology.levelEquiv_reduction

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
variable (ℓ : ℕ) [Fact ℓ.Prime]

Lean source · statement

theorem levelEquiv_reduction (n : ℕ)
    (a : finiteLevelCohomology X ℓ (n + 1) 1) :
    finiteLevelCharacterReduction ξ ℓ n (levelEquiv ξ ℓ (n + 1) a) =
      levelEquiv ξ ℓ n (finiteLevelReduction X ℓ n 1 a)

def

ellAdicH1CompatibleCharacterEquiv

L87 ↗

EtaleFundamentalGroups.Cohomology.ellAdicH1CompatibleCharacterEquiv

Documentation

Classical ℓ-adic H¹ is canonically the group of compatible finite continuous fundamental-group characters. The compatibility is proved from the original maps of constant coefficient sheaves.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
variable (ℓ : ℕ) [Fact ℓ.Prime]

Lean source · full declaration

def ellAdicH1CompatibleCharacterEquiv :
    ellAdicCohomology X ℓ 1 ≃+ compatibleFiniteCharacters ξ ℓ where
  toFun a := ⟨fun n => levelEquiv ξ ℓ n (a.val n), fun n =>
    (levelEquiv_reduction ξ ℓ n (a.val (n + 1))).trans
      (congrArg (levelEquiv ξ ℓ n) (a.property n))⟩
  invFun χ := ⟨fun n => (levelEquiv ξ ℓ n).symm (χ.val n), fun n => by
    apply (levelEquiv ξ ℓ n).injective
    exact (levelEquiv_reduction ξ ℓ n
      ((levelEquiv ξ ℓ (n + 1)).symm (χ.val (n + 1)))).symm.trans
        ((congrArg (finiteLevelCharacterReduction ξ ℓ n)
          ((levelEquiv ξ ℓ (n + 1)).apply_symm_apply (χ.val (n + 1)))).trans
            ((χ.property n).trans ((levelEquiv ξ ℓ n).apply_symm_apply (χ.val n)).symm))⟩
  left_inv a := Subtype.ext (funext fun n => (levelEquiv ξ ℓ n).symm_apply_apply (a.val n))
  right_inv χ := Subtype.ext (funext fun n => (levelEquiv ξ ℓ n).apply_symm_apply (χ.val n))
  map_add' a b := Subtype.ext (funext fun n => (levelEquiv ξ ℓ n).map_add (a.val n) (b.val n))

Module documentation

Classical ℓ-adic H¹ and compatible finite characters

Declarations

finiteLevelCharacters

finiteLevelCharactersAddCommGroup

finiteLevelCharacterReduction

compatibleFiniteCharacters

levelEquiv

levelEquiv_reduction

ellAdicH1CompatibleCharacterEquiv