Module

GaloisH1Descent.lean

Nyll.EtaleFundamentalGroups.Cohomology.GaloisH1Descent

6 declarations indexed from sourceView source ↗

Module documentation

Descent of actual finite-coefficient H¹ along Galois covers

For coefficient order coprime to the covering subgroup index, a class fixed by every actual geometric deck pullback descends to the base. The proof constructs the descended character by normalized continuous transfer, using the proved geometric deck/conjugation comparison and actual derived-H¹ naturality.

Imports5

Imported by3

instance

baseFiberFunctor

L35 ↗

EtaleFundamentalGroups.Cohomology.baseFiberFunctor

Source context 8 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open ClassFieldTower.Cohomology
namespace EtaleFundamentalGroups.Cohomology
variable {S : Scheme.{u}} [ConnectedSpace S] (A : FiniteEtale S)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable (xi : Spec (.of Ω) ⟶ A.left)

Lean source · statement

instance baseFiberFunctor :
    FiberFunctor (FiniteEtale.fiber (xi ≫ A.hom))

def

pointedCoverOpenSubgroup

L41 ↗

EtaleFundamentalGroups.Cohomology.pointedCoverOpenSubgroup

Documentation

The actual open subgroup of the base fundamental group selected by the lifted geometric point of a finite étale cover.

Source context 9 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open ClassFieldTower.Cohomology
namespace EtaleFundamentalGroups.Cohomology
variable {S : Scheme.{u}} [ConnectedSpace S] (A : FiniteEtale S)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable (xi : Spec (.of Ω) ⟶ A.left)
local instance baseFiberFunctor :
    FiberFunctor (FiniteEtale.fiber (xi ≫ A.hom)) :=
  FiniteEtale.fiberFunctor (X := S) (xi ≫ A.hom)

Lean source · full declaration

def pointedCoverOpenSubgroup :
    OpenSubgroup (Aut (FiniteEtale.fiber (xi ≫ A.hom))) where
  toSubgroup := MulAction.stabilizer _ (FiniteEtale.liftedFiberPoint A xi)
  isOpen' := stabilizer_isOpen _ (FiniteEtale.liftedFiberPoint A xi)

theorem

constantH1Pullback_injective_of_coprime_index

L51 ↗

EtaleFundamentalGroups.Cohomology.constantH1Pullback_injective_of_coprime_index

Documentation

Actual derived H¹ pullback is injective for finite coefficients whose order is coprime to the index of the Galois covering subgroup.

Source context 11 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open ClassFieldTower.Cohomology
namespace EtaleFundamentalGroups.Cohomology
variable {S : Scheme.{u}} [ConnectedSpace S] (A : FiniteEtale S)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable (xi : Spec (.of Ω) ⟶ A.left)
local instance baseFiberFunctor :
    FiberFunctor (FiniteEtale.fiber (xi ≫ A.hom)) :=
  FiniteEtale.fiberFunctor (X := S) (xi ≫ A.hom)
variable [IsGalois (C := FiniteEtale S) A] [ConnectedSpace A.left]
variable (B : AddCommGrpCat.{u}) [Finite B]

Lean source · statement

theorem constantH1Pullback_injective_of_coprime_index
    (hcop : (Nat.card (Multiplicative B)).Coprime
      (pointedCoverOpenSubgroup A xi).toSubgroup.index) :
    Function.Injective (constantCohomologyPullback A.hom B 1)

theorem

exists_constantH1Pullback_eq_of_deckInvariant

L91 ↗

EtaleFundamentalGroups.Cohomology.exists_constantH1Pullback_eq_of_deckInvariant

Documentation

A deck-invariant actual derived H¹ class descends across a finite étale Galois cover of coprime index. The class downstairs is constructed by transfer.

Source context 11 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open ClassFieldTower.Cohomology
namespace EtaleFundamentalGroups.Cohomology
variable {S : Scheme.{u}} [ConnectedSpace S] (A : FiniteEtale S)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable (xi : Spec (.of Ω) ⟶ A.left)
local instance baseFiberFunctor :
    FiberFunctor (FiniteEtale.fiber (xi ≫ A.hom)) :=
  FiniteEtale.fiberFunctor (X := S) (xi ≫ A.hom)
variable [IsGalois (C := FiniteEtale S) A] [ConnectedSpace A.left]
variable (B : AddCommGrpCat.{u}) [Finite B]

Lean source · statement

theorem exists_constantH1Pullback_eq_of_deckInvariant
    (hcop : (Nat.card (Multiplicative B)).Coprime
      (pointedCoverOpenSubgroup A xi).toSubgroup.index)
    (c : Sheaf.H.{u} ((constantSheaf A.left.smallEtaleTopology AddCommGrpCat.{u}).obj B) 1)
    (hinv : ∀ σ : Aut A, constantCohomologyPullback σ.hom.left B 1 c = c) :
    ∃ b : Sheaf.H.{u} ((constantSheaf S.smallEtaleTopology AddCommGrpCat.{u}).obj B) 1,
      constantCohomologyPullback A.hom B 1 b = c

theorem

constantH1Pullback_deck_of_base

L173 ↗

EtaleFundamentalGroups.Cohomology.constantH1Pullback_deck_of_base

Documentation

Pullback of a base class is fixed by every actual geometric deck transformation. This follows from the constructed conjugation comparison.

Source context 12 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open ClassFieldTower.Cohomology
namespace EtaleFundamentalGroups.Cohomology
variable {S : Scheme.{u}} [ConnectedSpace S] (A : FiniteEtale S)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable (xi : Spec (.of Ω) ⟶ A.left)
local instance baseFiberFunctor :
    FiberFunctor (FiniteEtale.fiber (xi ≫ A.hom)) :=
  FiniteEtale.fiberFunctor (X := S) (xi ≫ A.hom)
variable [IsGalois (C := FiniteEtale S) A] [ConnectedSpace A.left]
variable (B : AddCommGrpCat.{u}) [Finite B]
include xi in

Lean source · statement

theorem constantH1Pullback_deck_of_base
    (b : Sheaf.H.{u} ((constantSheaf S.smallEtaleTopology AddCommGrpCat.{u}).obj B) 1)
    (σ : Aut A) :
    constantCohomologyPullback σ.hom.left B 1
      (constantCohomologyPullback A.hom B 1 b) =
      constantCohomologyPullback A.hom B 1 b

theorem

mem_range_constantH1Pullback_iff_deckInvariant

L221 ↗

EtaleFundamentalGroups.Cohomology.mem_range_constantH1Pullback_iff_deckInvariant

Documentation

The image of actual H¹ pullback is exactly the classes fixed by actual deck pullbacks, for coefficient order coprime to the Galois covering index.

Source context 11 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open ClassFieldTower.Cohomology
namespace EtaleFundamentalGroups.Cohomology
variable {S : Scheme.{u}} [ConnectedSpace S] (A : FiniteEtale S)
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable (xi : Spec (.of Ω) ⟶ A.left)
local instance baseFiberFunctor :
    FiberFunctor (FiniteEtale.fiber (xi ≫ A.hom)) :=
  FiniteEtale.fiberFunctor (X := S) (xi ≫ A.hom)
variable [IsGalois (C := FiniteEtale S) A] [ConnectedSpace A.left]
variable (B : AddCommGrpCat.{u}) [Finite B]

Lean source · statement

theorem mem_range_constantH1Pullback_iff_deckInvariant
    (hcop : (Nat.card (Multiplicative B)).Coprime
      (pointedCoverOpenSubgroup A xi).toSubgroup.index)
    (c : Sheaf.H.{u} ((constantSheaf A.left.smallEtaleTopology AddCommGrpCat.{u}).obj B) 1) :
    c ∈ Set.range (constantCohomologyPullback A.hom B 1) ↔
      ∀ σ : Aut A, constantCohomologyPullback σ.hom.left B 1 c = c

Module documentation

Descent of actual finite-coefficient H¹ along Galois covers

Declarations

baseFiberFunctor

pointedCoverOpenSubgroup

constantH1Pullback_injective_of_coprime_index

exists_constantH1Pullback_eq_of_deckInvariant

constantH1Pullback_deck_of_base

mem_range_constantH1Pullback_iff_deckInvariant