NYLL
Module

TorsionH1Comparison.lean

Nyll.EtaleFundamentalGroups.Cohomology.TorsionH1Comparison
17 declarations indexed from sourceView source ↗

Module documentation

Finite-torsion étale H¹ and the full abelian fundamental group

The direct limit of actual finite-coefficient étale H¹ is the discrete Pontryagin character group of the actual topological abelianization. Factorization through finite quotients proves surjectivity. Thus finite torsion is retained, unlike a comparison using only rational ℓ-adic values.

Imports10
Imported by2

Declarations

instance

coefficientTopology

L36 ↗
EtaleFundamentalGroups.Cohomology.coefficientTopology
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
Lean source · statement
instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n))
instance

coefficientDiscrete

L38 ↗
EtaleFundamentalGroups.Cohomology.coefficientDiscrete
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
Lean source · statement
instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n))
def

coefficientCircle

L41 ↗
EtaleFundamentalGroups.Cohomology.coefficientCircle
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
Lean source · full declaration
def coefficientCircle (n : ℕ) :
    Multiplicative (finiteTorsionCoefficients.{u} n) →ₜ* Circle where
  toFun a := a.toAdd.down.toMul.val
  map_one' := rfl
  map_mul' _ _ := rfl
  continuous_toFun := continuous_of_discreteTopology
theorem

coefficientCircle_injective

L48 ↗
EtaleFundamentalGroups.Cohomology.coefficientCircle_injective
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
Lean source · statement
theorem coefficientCircle_injective (n : ℕ) :
    Function.Injective (coefficientCircle.{u} n)
abbrev

P

L58 ↗
EtaleFundamentalGroups.Cohomology.P
Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
abbrev P
instance

(anonymous instance)

L60 ↗
Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
instance : TotallyDisconnectedSpace (P ξ)
def

finiteTorsionStageCharacter

L66 ↗
EtaleFundamentalGroups.Cohomology.finiteTorsionStageCharacter
Documentation

The finite H¹ comparison followed by the actual inclusion into the circle.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · full declaration
def finiteTorsionStageCharacter (n : ℕ) :
    finiteTorsionLevel X 1 n →+ Additive (PontryaginDual (P ξ)) where
  toFun a := Additive.ofMul ((coefficientCircle n).comp
    (finiteH1AbelianCharacterEquiv (finiteTorsionCoefficients n) ξ a).toMul)
  map_zero' := by
    apply ContinuousMonoidHom.ext
    intro g
    change coefficientCircle n
      ((finiteH1AbelianCharacterEquiv (finiteTorsionCoefficients n) ξ 0).toMul g) = 1
    rw [map_zero]
    exact (coefficientCircle.{u} n).map_one
  map_add' a b := by
    apply ContinuousMonoidHom.ext
    intro g
    change coefficientCircle n
      ((finiteH1AbelianCharacterEquiv (finiteTorsionCoefficients n) ξ (a + b)).toMul g) = _
    exact (congrArg (fun χ : Additive (P ξ →ₜ*
      Multiplicative (finiteTorsionCoefficients n)) => coefficientCircle n (χ.toMul g))
        ((finiteH1AbelianCharacterEquiv (finiteTorsionCoefficients n) ξ).map_add a b)).trans
      ((coefficientCircle n).map_mul _ _)
theorem

stageCharacter_injective

L87 ↗
EtaleFundamentalGroups.Cohomology.stageCharacter_injective
Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem stageCharacter_injective (n : ℕ) :
    Function.Injective (finiteTorsionStageCharacter ξ n)
theorem

stageCharacter_compatible

L96 ↗
EtaleFundamentalGroups.Cohomology.stageCharacter_compatible
Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem stageCharacter_compatible (m n : ℕ) (h : m ≤ n)
    (a : finiteTorsionLevel X 1 m) :
    finiteTorsionStageCharacter ξ m a =
      finiteTorsionStageCharacter ξ n (finiteTorsionTransition X 1 m n h a)
def

directLimitAddHom

L119 ↗
EtaleFundamentalGroups.Cohomology.directLimitAddHom
Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · full declaration
def directLimitAddHom (G : ℕ → Type u) [∀ n, AddCommGroup (G n)]
    (f : ∀ m n, m ≤ n → G m →+ G n) [DirectedSystem G (f · · ·)]
    {A : Type v} [AddCommGroup A] (g : ∀ n, G n →+ A)
    (h : ∀ m n h a, g m a = g n (f m n h a)) : DirectLimit G f →+ A where
  toFun := DirectLimit.lift f (fun n => g n) h
  map_zero' := DirectLimit.lift_zero g h
  map_add' := DirectLimit.lift_add g h
def

finiteTorsionH1Character

L128 ↗
EtaleFundamentalGroups.Cohomology.finiteTorsionH1Character
Documentation

The character of a finite-coefficient direct-limit étale H¹ class.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
def finiteTorsionH1Character :
    finiteTorsionCohomology X 1 →+ Additive (PontryaginDual (P ξ))
theorem

finiteTorsionH1Character_injective

L134 ↗
EtaleFundamentalGroups.Cohomology.finiteTorsionH1Character_injective
Documentation

The character comparison on the direct limit is injective.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem finiteTorsionH1Character_injective :
    Function.Injective (finiteTorsionH1Character ξ)
def

quotientCoefficientCharacter

L140 ↗
EtaleFundamentalGroups.Cohomology.quotientCoefficientCharacter
Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
def quotientCoefficientCharacter (χ : PontryaginDual (P ξ))
    (U : OpenNormalSubgroup (P ξ)) (hU : (U : Subgroup (P ξ)) ≤ χ.toMonoidHom.ker) :
    (P ξ ⧸ (U : Subgroup (P ξ))) →ₜ*
      Multiplicative (finiteTorsionCoefficients.{u} (Nat.card (P ξ ⧸ (U : Subgroup (P ξ)))))
theorem

finiteTorsionH1Character_surjective

L159 ↗
EtaleFundamentalGroups.Cohomology.finiteTorsionH1Character_surjective
Documentation

Every circle character comes from actual finite-coefficient étale H¹.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem finiteTorsionH1Character_surjective :
    Function.Surjective (finiteTorsionH1Character ξ)
def

finiteTorsionH1CharacterEquiv

L177 ↗
EtaleFundamentalGroups.Cohomology.finiteTorsionH1CharacterEquiv
Documentation

Actual finite-torsion étale H¹ is the full character group of the actual topological abelianization, including torsion characters.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
def finiteTorsionH1CharacterEquiv :
    finiteTorsionCohomology X 1 ≃+ Additive (PontryaginDual (P ξ))
theorem

finiteTorsionH1Character_basePoint

L186 ↗
EtaleFundamentalGroups.Cohomology.finiteTorsionH1Character_basePoint
Documentation

Base-point transport preserves the monodromy pairing on the actual finite-coefficient direct limit. This uses finite-level derived H¹, not cohomology of an infinite constant sheaf.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem finiteTorsionH1Character_basePoint
    {Ω' : Type u} [Field Ω'] [IsSepClosed Ω'] (η : Spec (.of Ω') ⟶ X)
    (τ : FiniteEtale.fiber ξ ≅ FiniteEtale.fiber η)
    (a : finiteTorsionCohomology X 1) :
    (finiteTorsionH1Character η a).toMul.comp
        (ProCGroups.Abelian.TopologicalAbelianization.map
          (ContinuousMonoidHom.toContinuousMonoidHom
            (PreGaloisCategory.continuousConjAut τ))) =
      (finiteTorsionH1Character ξ a).toMul
theorem

finiteTorsionH1Character_schemePullback

L219 ↗
EtaleFundamentalGroups.Cohomology.finiteTorsionH1Character_schemePullback
Documentation

Geometric inverse image of the actual finite-coefficient direct limit is dual to the actual induced map on topological abelianizations.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open ProCGroups.ProC
universe u v
namespace EtaleFundamentalGroups.Cohomology
local instance coefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⊥
local instance coefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (finiteTorsionCoefficients.{u} n)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem finiteTorsionH1Character_schemePullback
    {Y : Scheme.{u}} [ConnectedSpace Y] (f : X ⟶ Y)
    (a : finiteTorsionCohomology Y 1) :
    (finiteTorsionH1Character ξ (finiteTorsionCohomologyPullback f 1 a)).toMul =
      (finiteTorsionH1Character (ξ ≫ f) a).toMul.comp
        (ProCGroups.Abelian.TopologicalAbelianization.map
          (FiniteEtale.fundamentalGroupHom f ξ))

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