Module

PrimeDegreeCohomology.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.PrimeDegreeCohomology

1 declaration indexed from sourceView source ↗

Module documentation

Prime-degree cohomology detection without a roots-of-unity hypothesis

This is stronger than Lemma 3.2 of Yamaguchi, arXiv:2610.05634v1: it requires neither μ_p ⊆ K nor completeness.

Imports2

Imported by1

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.All

theorem

prime_degree_cohomology_of_mixedChar

L21 ↗

Yamaguchi26AbfaithfulGalois.prime_degree_cohomology_of_mixedChar

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ValuationTheory.DiscreteValuationField
universe u v

Lean source · statement

theorem prime_degree_cohomology_of_mixedChar
    {K L : Type u} [Field K] [Field L] [Algebra K L] [IsGalois K L]
    [CharZero K] (base : DVF.{u, v} K)
    (p r : ℕ) [Fact p.Prime] [Fact r.Prime] [CharP base.residueField p]
    (hdegree : Module.finrank K L = r) :
    ∃ τ : Gal(L/K), relativeGaloisH1Action (n := p) K L τ ≠ 1

Module documentation

Prime-degree cohomology detection without a roots-of-unity hypothesis

Declarations

prime_degree_cohomology_of_mixedChar