Module

Theorem3Dot5CompletePrimeDegree.lean

Nyll.Yamaguchi26AbfaithfulGalois.Theorem3Dot5CompletePrimeDegree

1 declaration indexed from sourceView source ↗

Module documentation

Proposition 3.5: nontrivial mod-p cohomology action

Source: Yamaguchi, arXiv:2610.05634v1, Proposition 3.5.

Imports2

Imported by1

Nyll.Yamaguchi26AbfaithfulGalois.All

theorem

complete_prime_degree_cohomology_3_5

L19 ↗

Yamaguchi26AbfaithfulGalois.complete_prime_degree_cohomology_3_5

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 complete_prime_degree_cohomology_3_5
    {K L : Type u} [Field K] [Field L] [Algebra K L] [IsGalois K L]
    [CharZero K] (base : CompleteDVF.{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

Proposition 3.5: nontrivial mod-p cohomology action

Declarations

complete_prime_degree_cohomology_3_5