Module

H1Surjectivity.lean

Nyll.EtaleFundamentalGroups.Cohomology.H1Surjectivity

1 declaration indexed from sourceView source ↗

Module documentation

Every finite continuous character is an actual étale H¹ class

A character gives a finite triangular representation on A × End(A). Its descended short exact sequence is pulled back along the constant map ℤ → End(A) sending 1 to the identity. Evaluation in the actual middle stalk recovers the original character. Only connectedness and a geometric point of the scheme are required.

Imports5

Imported by2

theorem

h1Character_surjective

L34 ↗

EtaleFundamentalGroups.Cohomology.h1Character_surjective

Documentation

For finite constant abelian coefficients, every continuous character of the actual étale fundamental group comes from the existing derived H¹.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped FintypeCatDiscrete
universe u
namespace EtaleFundamentalGroups.Cohomology

Lean source · statement

theorem h1Character_surjective {X : Scheme.{u}} [ConnectedSpace X]
    (A : AddCommGrpCat.{u}) [Finite A]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X) :
    Function.Surjective (h1Character A ξ)

Module documentation

Every finite continuous character is an actual étale H¹ class

Declarations

h1Character_surjective