Module

DeckAbelianH1Duality.lean

Nyll.EtaleFundamentalGroups.Cohomology.DeckAbelianH1Duality

3 declarations indexed from sourceView source ↗

Module documentation

Equivariance of actual abelian H¹ duality for pointed deck actions

The existing duality is reused. Its scheme naturality and base-point naturality give equivariance for any specified pointed geometric pullback. For a deck transformation, the actual comparison with conjugation is the one constructed by the geometric fiber functor.

Imports3

Imported by1

Nyll.EtaleFundamentalGroups.Cohomology.All

instance

torsionTopology

L29 ↗

EtaleFundamentalGroups.Cohomology.torsionTopology

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open EtaleCohomology.Classical
namespace EtaleFundamentalGroups.Cohomology

Lean source · statement

instance torsionTopology (X : Scheme.{u}) :
    TopologicalSpace (Multiplicative (finiteTorsionCohomology X 1))

theorem

abelianizationFiniteTorsionH1DualEquiv_pointedPullback

L34 ↗

EtaleFundamentalGroups.Cohomology.abelianizationFiniteTorsionH1DualEquiv_pointedPullback

Documentation

The existing duality intertwines actual inverse image with the abelianization map from any pointed geometric fiber comparison.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open EtaleCohomology.Classical
namespace EtaleFundamentalGroups.Cohomology
local instance torsionTopology (X : Scheme.{u}) :
    TopologicalSpace (Multiplicative (finiteTorsionCohomology X 1)) := ⊥

Lean source · statement

theorem abelianizationFiniteTorsionH1DualEquiv_pointedPullback
    {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
    (f : X ⟶ Y)
    {Ω Ω' : Type u} [Field Ω] [IsSepClosed Ω] [Field Ω'] [IsSepClosed Ω']
    (ξ : Spec (.of Ω) ⟶ X) (η : Spec (.of Ω') ⟶ Y)
    (t : FiniteEtale.pullback f ⋙ FiniteEtale.fiber ξ ≅ FiniteEtale.fiber η)
    (g : TopologicalAbelianization (Aut (FiniteEtale.fiber ξ))) :
    abelianizationFiniteTorsionH1DualEquiv η
      (ProCGroups.Abelian.TopologicalAbelianization.map
        (autHomOfCompIso (FiniteEtale.pullback f) t) g) =
      (abelianizationFiniteTorsionH1DualEquiv ξ g).comp
        (finiteTorsionH1PullbackHom f)

theorem

abelianizationFiniteTorsionH1DualEquiv_deck

L72 ↗

EtaleFundamentalGroups.Cohomology.abelianizationFiniteTorsionH1DualEquiv_deck

Documentation

Equivariance for the actual pointed deck action, with no assumed compatibility between the deck action and cohomological duality.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open EtaleCohomology.Classical
namespace EtaleFundamentalGroups.Cohomology
local instance torsionTopology (X : Scheme.{u}) :
    TopologicalSpace (Multiplicative (finiteTorsionCohomology X 1)) := ⊥

Lean source · statement

theorem abelianizationFiniteTorsionH1DualEquiv_deck
    {S : Scheme.{u}} [ConnectedSpace S]
    (A : FiniteEtale S) [ConnectedSpace A.left]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶ A.left)
    (σ : Aut A) (g : Aut (FiniteEtale.fiber (ξ ≫ A.hom)))
    (h : (FiniteEtale.fiber (ξ ≫ A.hom)).map σ.hom
      (FiniteEtale.liftedFiberPoint A ξ) =
        g • FiniteEtale.liftedFiberPoint A ξ)
    (a : TopologicalAbelianization (Aut (FiniteEtale.fiber ξ))) :
    abelianizationFiniteTorsionH1DualEquiv ξ
      (ProCGroups.Abelian.TopologicalAbelianization.map
        (autHomOfCompIso (FiniteEtale.pullback σ.hom.left)
          (FiniteEtale.deckPointedGeometricFiberIso A ξ σ g h)) a) =
      (abelianizationFiniteTorsionH1DualEquiv ξ a).comp
        (finiteTorsionH1PullbackHom σ.hom.left)

Module documentation

Equivariance of actual abelian H¹ duality for pointed deck actions

Declarations

torsionTopology

abelianizationFiniteTorsionH1DualEquiv_pointedPullback

abelianizationFiniteTorsionH1DualEquiv_deck