Module

GenericH1Characters.lean

Nyll.EtaleFundamentalGroups.Cohomology.GenericH1Characters

2 declarations indexed from sourceView source ↗

Module documentation

Actual geometric H¹ and unramified generic characters

The generic absolute Galois map identifies the characters of a normal integral scheme with the characters that kill its actual normalization inertia groups. The inertia groups are those of the literal integral closures on affine charts.

Imports3

Nyll.EtaleFundamentalGroups.Cohomology.FiniteH1Comparison
Nyll.EtaleFundamentalGroups.Inertia.GenericKernelNormalGeneration
Mathlib.Topology.Algebra.Group.Subgroup

Imported by1

Nyll.EtaleFundamentalGroups.Cohomology.All

theorem

exists_genericCharacter_iff_kills_inertia

L33 ↗

EtaleFundamentalGroups.Cohomology.exists_genericCharacter_iff_kills_inertia

Documentation

Actual generic characters descend precisely when they annihilate all normalization inertia, including the topological closure of their normal span.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale CategoryTheory
open EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups.Cohomology
universe u v
variable (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
variable {B : Type v} [CommGroup B] [TopologicalSpace B] [T2Space B]

Lean source · statement

theorem exists_genericCharacter_iff_kills_inertia
    (χ : Gal(SeparableClosure X.functionField/X.functionField) →ₜ* B) :
    (∃ ψ : π₁ᵉᵗ(X.genericExtensionMorphism (AlgebraicClosure X.functionField)) →ₜ* B,
      ψ.comp (genericAbsoluteGaloisHom X) = χ) ↔
    ∀ σ ∈ affineNormalizationInertiaGenerators X, χ σ = 1

theorem

genericCharacter_comp_injective

L77 ↗

EtaleFundamentalGroups.Cohomology.genericCharacter_comp_injective

Documentation

Two characters of the actual fundamental group agree if their generic absolute Galois characters agree.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry AlgebraicGeometry.FiniteEtale CategoryTheory
open EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups.Cohomology
universe u v
variable (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
variable {B : Type v} [CommGroup B] [TopologicalSpace B] [T2Space B]
omit [T2Space B] in

Lean source · full declaration

theorem genericCharacter_comp_injective :
    Function.Injective (fun ψ :
      π₁ᵉᵗ(X.genericExtensionMorphism (AlgebraicClosure X.functionField)) →ₜ* B =>
        ψ.comp (genericAbsoluteGaloisHom X)) := by
  intro ψ τ h
  apply ContinuousMonoidHom.ext
  intro g
  obtain ⟨σ, rfl⟩ := genericAbsoluteGaloisHom_surjective X g
  exact congrArg (fun f => f σ) h

Module documentation

Actual geometric H¹ and unramified generic characters

Declarations

exists_genericCharacter_iff_kills_inertia

genericCharacter_comp_injective