NYLL
Module

AbelianH1Duality.lean

Nyll.EtaleFundamentalGroups.Cohomology.AbelianH1Duality
10 declarations indexed from sourceView source ↗

Module documentation

The abelian étale fundamental group as a cohomological dual

For a connected scheme and a geometric point, the actual topological abelianization is the Pontryagin dual of the discrete direct limit of its ordinary finite-coefficient étale H¹ groups. Both maps and both continuity statements are proved, and the isomorphism is the monodromy evaluation pairing.

This retains finite torsion. No smoothness, properness, noetherianity or characteristic hypothesis is needed. Identifying the displayed direct limit with derived cohomology of an infinite constant sheaf is a separate issue.

Imports7
Imported by2

Declarations

instance

torsionH1Topology

L36 ↗
EtaleFundamentalGroups.Cohomology.torsionH1Topology
Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
Lean source · statement
instance torsionH1Topology (X : Scheme.{u}) :
    TopologicalSpace (Multiplicative (finiteTorsionCohomology X 1))
instance

torsionH1Discrete

L38 ↗
EtaleFundamentalGroups.Cohomology.torsionH1Discrete
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
local instance torsionH1Topology (X : Scheme.{u}) :
    TopologicalSpace (Multiplicative (finiteTorsionCohomology X 1)) := ⊥
Lean source · statement
instance torsionH1Discrete (X : Scheme.{u}) :
    DiscreteTopology (Multiplicative (finiteTorsionCohomology X 1))
abbrev

P

L44 ↗
EtaleFundamentalGroups.Cohomology.P
Source context 7 commands

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

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

(anonymous instance)

L46 ↗
Source context 7 commands

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

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

finiteTorsionH1ContinuousCharacterEquiv

L53 ↗
EtaleFundamentalGroups.Cohomology.finiteTorsionH1ContinuousCharacterEquiv
Documentation

The finite-coefficient H¹ character comparison respects the actual discrete topology on cohomology and the compact-open topology on the character group.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
local instance torsionH1Topology (X : Scheme.{u}) :
    TopologicalSpace (Multiplicative (finiteTorsionCohomology X 1)) := ⊥
local instance torsionH1Discrete (X : Scheme.{u}) :
    DiscreteTopology (Multiplicative (finiteTorsionCohomology X 1)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · full declaration
def finiteTorsionH1ContinuousCharacterEquiv :
    Multiplicative (finiteTorsionCohomology X 1) ≃ₜ* PontryaginDual (P ξ) where
  toMulEquiv := AddEquiv.toMultiplicativeLeft (finiteTorsionH1CharacterEquiv ξ)
  continuous_toFun := continuous_of_discreteTopology
  continuous_invFun := continuous_of_discreteTopology
def

abelianizationFiniteTorsionH1DualEquiv

L61 ↗
EtaleFundamentalGroups.Cohomology.abelianizationFiniteTorsionH1DualEquiv
Documentation

The full topological abelianization of the étale fundamental group is the actual Pontryagin dual of the finite-coefficient direct-limit étale H¹ group.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
local instance torsionH1Topology (X : Scheme.{u}) :
    TopologicalSpace (Multiplicative (finiteTorsionCohomology X 1)) := ⊥
local instance torsionH1Discrete (X : Scheme.{u}) :
    DiscreteTopology (Multiplicative (finiteTorsionCohomology X 1)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
def abelianizationFiniteTorsionH1DualEquiv :
    TopologicalAbelianization (Aut (FiniteEtale.fiber ξ)) ≃ₜ*
      PontryaginDual (Multiplicative (finiteTorsionCohomology X 1))
theorem

abelianizationFiniteTorsionH1DualEquiv_apply

L74 ↗
EtaleFundamentalGroups.Cohomology.abelianizationFiniteTorsionH1DualEquiv_apply
Documentation

The duality isomorphism evaluates a cohomology class by its actual finite-coefficient monodromy character on the abelianized fundamental group.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
local instance torsionH1Topology (X : Scheme.{u}) :
    TopologicalSpace (Multiplicative (finiteTorsionCohomology X 1)) := ⊥
local instance torsionH1Discrete (X : Scheme.{u}) :
    DiscreteTopology (Multiplicative (finiteTorsionCohomology X 1)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem abelianizationFiniteTorsionH1DualEquiv_apply
    (g : TopologicalAbelianization (Aut (FiniteEtale.fiber ξ)))
    (a : finiteTorsionCohomology X 1) :
    abelianizationFiniteTorsionH1DualEquiv ξ g (Multiplicative.ofAdd a) =
      (finiteTorsionH1Character ξ a).toMul g
theorem

abelianizationFiniteTorsionH1DualEquiv_basePoint

L85 ↗
EtaleFundamentalGroups.Cohomology.abelianizationFiniteTorsionH1DualEquiv_basePoint
Documentation

The actual Pontryagin duality is independent of the geometric base point, with transport on the topological abelianization induced by the given isomorphism of fiber functors. Scheme-pullback equivariance is a separate comparison; it is not an assumption of this theorem.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
local instance torsionH1Topology (X : Scheme.{u}) :
    TopologicalSpace (Multiplicative (finiteTorsionCohomology X 1)) := ⊥
local instance torsionH1Discrete (X : Scheme.{u}) :
    DiscreteTopology (Multiplicative (finiteTorsionCohomology X 1)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem abelianizationFiniteTorsionH1DualEquiv_basePoint
    {Ω' : Type u} [Field Ω'] [IsSepClosed Ω'] (η : Spec (.of Ω') ⟶ X)
    (τ : FiniteEtale.fiber ξ ≅ FiniteEtale.fiber η)
    (g : TopologicalAbelianization (Aut (FiniteEtale.fiber ξ))) :
    abelianizationFiniteTorsionH1DualEquiv η
        (ProCGroups.Abelian.TopologicalAbelianization.map
          (ContinuousMonoidHom.toContinuousMonoidHom
            (PreGaloisCategory.continuousConjAut τ)) g) =
      abelianizationFiniteTorsionH1DualEquiv ξ g
def

finiteTorsionH1PullbackHom

L107 ↗
EtaleFundamentalGroups.Cohomology.finiteTorsionH1PullbackHom
Documentation

Actual derived inverse image on finite-torsion H¹, with its discrete topology.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
local instance torsionH1Topology (X : Scheme.{u}) :
    TopologicalSpace (Multiplicative (finiteTorsionCohomology X 1)) := ⊥
local instance torsionH1Discrete (X : Scheme.{u}) :
    DiscreteTopology (Multiplicative (finiteTorsionCohomology X 1)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · full declaration
def finiteTorsionH1PullbackHom {Y : Scheme.{u}} (f : X ⟶ Y) :
    Multiplicative (finiteTorsionCohomology Y 1) →ₜ*
      Multiplicative (finiteTorsionCohomology X 1) where
  toMonoidHom := (finiteTorsionCohomologyPullback f 1).toMultiplicative
  continuous_toFun := continuous_of_discreteTopology
theorem

abelianizationFiniteTorsionH1DualEquiv_schemePullback

L117 ↗
EtaleFundamentalGroups.Cohomology.abelianizationFiniteTorsionH1DualEquiv_schemePullback
Documentation

The established Pontryagin duality intertwines actual geometric inverse image and the induced map of actual topological abelianizations. In particular, the comparison applies to actual deck automorphisms and is not an assumed equivariance field.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
local instance torsionH1Topology (X : Scheme.{u}) :
    TopologicalSpace (Multiplicative (finiteTorsionCohomology X 1)) := ⊥
local instance torsionH1Discrete (X : Scheme.{u}) :
    DiscreteTopology (Multiplicative (finiteTorsionCohomology X 1)) := ⟨rfl⟩
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem abelianizationFiniteTorsionH1DualEquiv_schemePullback
    {Y : Scheme.{u}} [ConnectedSpace Y] (f : X ⟶ Y)
    (g : TopologicalAbelianization (Aut (FiniteEtale.fiber ξ))) :
    abelianizationFiniteTorsionH1DualEquiv (ξ ≫ f)
        (ProCGroups.Abelian.TopologicalAbelianization.map
          (FiniteEtale.fundamentalGroupHom f ξ) g) =
      (abelianizationFiniteTorsionH1DualEquiv ξ g).comp
        (finiteTorsionH1PullbackHom f)

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