NYLL
Module

DeckH1Centralizer.lean

Nyll.EtaleFundamentalGroups.Cohomology.DeckH1Centralizer
2 declarations indexed from sourceView source ↗

Module documentation

Centralizers act trivially on actual finite-coefficient H¹

For a geometric deck transformation selected by ambient monodromy, an element centralizing the covering subgroup acts trivially on the actual derived H¹. This comparison does not assume H¹ faithfulness. The geometric proof that a nonidentity deck transformation must act nontrivially remains a separate step.

Imports6
Imported by3

Declarations

theorem

constantH1Pullback_deck_eq_self_of_centralizes

L42 ↗
EtaleFundamentalGroups.Cohomology.constantH1Pullback_deck_eq_self_of_centralizes
Documentation

Actual derived H¹ pullback by the geometric deck transformation is the identity when its ambient lift centralizes the actual 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
namespace EtaleFundamentalGroups.Cohomology
variable {S : Scheme.{u}} [ConnectedSpace S] (A : FiniteEtale S)
variable [ConnectedSpace A.left]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω]
variable (xi : Spec (.of Ω) ⟶ A.left)
variable (σ : Aut A) (g : Aut (FiniteEtale.fiber (xi ≫ A.hom)))
variable (h : (FiniteEtale.fiber (xi ≫ A.hom)).map σ.hom
    (FiniteEtale.liftedFiberPoint A xi) = g • FiniteEtale.liftedFiberPoint A xi)
include h in
Lean source · statement
theorem constantH1Pullback_deck_eq_self_of_centralizes
    (hc : ∀ a : Aut (FiniteEtale.fiber xi),
      Commute g (FiniteEtale.fundamentalGroupHom A.hom xi a))
    (B : AddCommGrpCat.{u}) [Finite B]
    (c : Sheaf.H.{u} ((constantSheaf A.left.smallEtaleTopology AddCommGrpCat.{u}).obj B) 1) :
    constantCohomologyPullback σ.hom.left B 1 c = c
theorem

fundamentalGroup_eq_one_of_finiteH1_deck_faithful

L69 ↗
EtaleFundamentalGroups.Cohomology.fundamentalGroup_eq_one_of_finiteH1_deck_faithful
Documentation

Geometric faithfulness of the joint deck action on finite-coefficient derived H¹ kills every central element of the actual fundamental group. The geometric faithfulness premise is supplied separately for each curve; the fiber and conjugation comparisons in this proof are the actual ones.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Cohomology
Lean source · statement
theorem fundamentalGroup_eq_one_of_finiteH1_deck_faithful
    {X : Scheme.{u}} [ConnectedSpace X]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (geom : Spec (.of Ω) ⟶ X)
    (hfaithful : ∀ (A : FiniteEtale X) [CategoryTheory.PreGaloisCategory.IsGalois A]
      (_xi : Spec (.of Ω) ⟶ A.left) (σ : Aut A),
      (∀ (C : AddCommGrpCat.{u}) [Finite C]
        (c : Sheaf.H.{u}
          ((constantSheaf A.left.smallEtaleTopology AddCommGrpCat.{u}).obj C) 1),
        constantCohomologyPullback σ.hom.left C 1 c = c) → σ = 1)
    (g : Aut (FiniteEtale.fiber geom)) (hc : ∀ a, Commute g a) :
    g = 1

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