Module

FiniteH1DeckKernel.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiniteH1DeckKernel

2 declarations indexed from sourceView source ↗

Module documentation

The kernel of the actual deck action on finite H¹

The subgroup laws are proved from the composition and identity laws of the actual derived-sheaf pullback. In particular triviality propagates to the cyclic subgroup generated by a deck transformation.

Imports1

Nyll.EtaleFundamentalGroups.Cohomology.FiniteH1PullbackIdentity

Imported by2

def

finiteH1DeckKernel

L27 ↗

EtaleFundamentalGroups.Cohomology.finiteH1DeckKernel

Documentation

The genuine kernel of pullback on actual derived H¹.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace EtaleFundamentalGroups.Cohomology
variable {S : Scheme} (A : FiniteEtale S) [ConnectedSpace A.left]
  {Ω : Type} [Field Ω] [IsSepClosed Ω]
  (geom : Spec (.of Ω) ⟶ A.left) (B : AddCommGrpCat.{0}) [Finite B]

Lean source · full declaration

def finiteH1DeckKernel : Subgroup (Aut A) where
  carrier := { σ | ∀ c, constantCohomologyPullback σ.hom.left B 1 c = c }
  one_mem' := by
    intro c
    exact constantFiniteH1Pullback_id geom B c
  mul_mem' := by
    intro σ τ hσ hτ c
    change constantCohomologyPullback (τ.hom.left ≫ σ.hom.left) B 1 c = c
    rw [constantFiniteH1Pullback_comp τ.hom.left σ.hom.left geom B c, hσ c, hτ c]
  inv_mem' := by
    intro σ hσ c
    have he : σ.hom.left ≫ σ.inv.left = 𝟙 A.left :=
      congrArg (fun f : A ⟶ A => f.left) σ.hom_inv_id
    have h := constantFiniteH1Pullback_comp σ.hom.left σ.inv.left geom B c
    rw [he, constantFiniteH1Pullback_id geom B c,
      hσ (constantCohomologyPullback σ.inv.left B 1 c)] at h
    exact h.symm

theorem

constantFiniteH1Pullback_eq_self_of_mem_deck_zpowers

L49 ↗

EtaleFundamentalGroups.Cohomology.constantFiniteH1Pullback_eq_self_of_mem_deck_zpowers

Documentation

All powers of a deck transformation acting trivially act trivially, for the actual finite-coefficient derived H¹ pullback.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace EtaleFundamentalGroups.Cohomology
variable {S : Scheme} (A : FiniteEtale S) [ConnectedSpace A.left]
  {Ω : Type} [Field Ω] [IsSepClosed Ω]
  (geom : Spec (.of Ω) ⟶ A.left) (B : AddCommGrpCat.{0}) [Finite B]
include geom

Lean source · statement

theorem constantFiniteH1Pullback_eq_self_of_mem_deck_zpowers
    (σ τ : Aut A) (hσ : ∀ c, constantCohomologyPullback σ.hom.left B 1 c = c)
    (hτ : τ ∈ Subgroup.zpowers σ) :
    ∀ c, constantCohomologyPullback τ.hom.left B 1 c = c

Module documentation

The kernel of the actual deck action on finite H¹

Declarations

finiteH1DeckKernel

constantFiniteH1Pullback_eq_self_of_mem_deck_zpowers