NYLL
Module

H1FiniteEtaleEffacement.lean

Nyll.EtaleFundamentalGroups.Cohomology.H1FiniteEtaleEffacement
4 declarations indexed from sourceView source ↗

Module documentation

Killing actual finite-coefficient H¹ on a finite étale cover

The open kernel of the actual cohomology character is realized by an actual connected finite étale cover. Geometric naturality proves that the original derived cohomology class pulls back to zero.

This supplies the degree-one step of Mochizuki, "The Local Pro-p Anabelian Geometry of Curves", Lemma 0.4, pp. 14–15: https://www.kurims.kyoto-u.ac.jp/~motizuki/The%20Local%20Pro-p%20Anabelian%20Geometry%20of%20Curves.pdf

The result here allows any finite abelian constant coefficients and asserts finite étale effacement, with geometric fiber degree dividing the order of the coefficient group. The higher-degree K(pi,1) comparison is not asserted.

Imports9
Imported by1

Declarations

theorem

exists_galois_finiteEtale_cover_killing_h1

L44 ↗
EtaleFundamentalGroups.Cohomology.exists_galois_finiteEtale_cover_killing_h1
Documentation

Every actual finite constant-coefficient H¹ class becomes zero on an actual connected finite étale Galois cover, with degree dividing the order of the coefficient group and a lift of the original base point.

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 exists_galois_finiteEtale_cover_killing_h1
    {X : Scheme.{u}} [ConnectedSpace X]
    (C : AddCommGrpCat.{u}) [Finite C]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ X)
    (a : Sheaf.H.{u} ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj C) 1) :
    ∃ (V : FiniteEtale X) (_ : IsGalois V)
      (xiV : Spec (.of Ω) ⟶ V.left),
      xiV ≫ V.hom = xi ∧
        Nat.card ((FiniteEtale.fiber xi).obj V) ∣ Nat.card C ∧
        (Nat.card ((FiniteEtale.fiber xi).obj V) = 1 ↔ a = 0) ∧
        constantCohomologyPullback (X := V.left) (Y := X) V.hom C 1 a = 0
theorem

exists_connected_finiteEtale_cover_killing_h1

L98 ↗
EtaleFundamentalGroups.Cohomology.exists_connected_finiteEtale_cover_killing_h1
Documentation

The connected-cover form of finite constant-coefficient H¹ effacement.

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 exists_connected_finiteEtale_cover_killing_h1
    {X : Scheme.{u}} [ConnectedSpace X]
    (C : AddCommGrpCat.{u}) [Finite C]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ X)
    (a : Sheaf.H.{u} ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj C) 1) :
    ∃ (V : FiniteEtale X) (_ : ConnectedSpace V.left)
      (xiV : Spec (.of Ω) ⟶ V.left),
      xiV ≫ V.hom = xi ∧
        constantCohomologyPullback (X := V.left) (Y := X) V.hom C 1 a = 0
theorem

exists_primePower_galois_finiteEtale_cover_killing_h1

L115 ↗
EtaleFundamentalGroups.Cohomology.exists_primePower_galois_finiteEtale_cover_killing_h1
Documentation

For a finite p-primary coefficient group, the killing cover has p-power geometric degree, bounded by the order of the coefficient group.

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 exists_primePower_galois_finiteEtale_cover_killing_h1
    {X : Scheme.{u}} [ConnectedSpace X]
    (C : AddCommGrpCat.{u}) [Finite C]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ X)
    (p n : ℕ) (hp : p.Prime) (hC : Nat.card C = p ^ n)
    (a : Sheaf.H.{u} ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj C) 1) :
    ∃ (V : FiniteEtale X) (_ : IsGalois V)
      (xiV : Spec (.of Ω) ⟶ V.left) (m : ℕ),
      xiV ≫ V.hom = xi ∧ m ≤ n ∧
        Nat.card ((FiniteEtale.fiber xi).obj V) = p ^ m ∧
        constantCohomologyPullback (X := V.left) (Y := X) V.hom C 1 a = 0
theorem

exists_primeDegree_galois_finiteEtale_cover_killing_h1

L136 ↗
EtaleFundamentalGroups.Cohomology.exists_primeDegree_galois_finiteEtale_cover_killing_h1
Documentation

A nonzero H¹ class with coefficients of prime order is killed by a connected Galois cover of exactly that prime degree.

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 exists_primeDegree_galois_finiteEtale_cover_killing_h1
    {X : Scheme.{u}} [ConnectedSpace X]
    (C : AddCommGrpCat.{u}) [Finite C]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ X)
    (p : ℕ) (hp : p.Prime) (hC : Nat.card C = p)
    (a : Sheaf.H.{u} ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj C) 1)
    (ha : a ≠ 0) :
    ∃ (V : FiniteEtale X) (_ : IsGalois V)
      (xiV : Spec (.of Ω) ⟶ V.left),
      xiV ≫ V.hom = xi ∧
        Nat.card ((FiniteEtale.fiber xi).obj V) = p ∧
        constantCohomologyPullback (X := V.left) (Y := X) V.hom C 1 a = 0

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