Nyll.EtaleFundamentalGroups.Cohomology.CyclicDeckH1Reduction

Module documentation

Actual cyclic intermediate cover for a kernel element of deck H¹ action

This is a reduction by contradiction: a nonidentity kernel element would produce an actual nontrivial relative Galois cover whose whole deck group acts trivially. The intermediate scheme and all action comparisons are constructed, rather than required as hypotheses.

theorem

exists_cyclicIntermediate_of_allFiniteH1Trivial

L26 ↗

EtaleFundamentalGroups.Cohomology.exists_cyclicIntermediate_of_allFiniteH1Trivial

Documentation

A nonidentity element in the actual H¹ deck kernel yields an actual nontrivial cyclic intermediate Galois cover with wholly trivial H¹ action.

Source context 3 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
namespace EtaleFundamentalGroups.Cohomology

Lean source · statement

theorem exists_cyclicIntermediate_of_allFiniteH1Trivial
    {S : Scheme} [ConnectedSpace S] (A : FiniteEtale S) [IsGalois A]
    [ConnectedSpace A.left]
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (geom : Spec (.of Ω) ⟶ A.left)
    (σ : Aut A) (hσne : σ ≠ 1)
    (hσ : ∀ (C : AddCommGrpCat.{0}) [Finite C] c,
      constantCohomologyPullback σ.hom.left C 1 c = c) :
    ∃ (B : FiniteEtale S) (_ : ConnectedSpace B.left) (f : A ⟶ B),
      CategoryTheory.PreGaloisCategory.IsGalois (C := FiniteEtale B.left) (FiniteEtale.mk f.left) ∧
      (∃ ρ : Aut (FiniteEtale.mk f.left), ρ ≠ 1) ∧
      (∀ (C : AddCommGrpCat.{0}) [Finite C] (τ : Aut (FiniteEtale.mk f.left)) c,
        constantCohomologyPullback τ.hom.left C 1 c = c)

Module documentation

Actual cyclic intermediate cover for a kernel element of deck H¹ action

Declarations

exists_cyclicIntermediate_of_allFiniteH1Trivial