Module

CompletePrimeOrderDetection.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.CompletePrimeOrderDetection

1 declaration indexed from sourceView source ↗

Module documentation

Kummer theory and discretely valued fields

The stronger abelian-quotient form of current Proposition 3.5. The action is formed on the actual quotient G_Lᵃᵇ/p.

The prime-to-p branch uses faithful mod-p H¹ and its character-dual action on the actual abelianization quotient.

Imports7

Imported by3

theorem

prime_order_detection

L35 ↗

Yamaguchi26AbfaithfulGalois.prime_order_detection

Documentation

Complete-field detection: a prime-degree Galois extension of a complete mixed-characteristic DVF acts nontrivially on G_Lᵃᵇ/p, including the dyadic case.

Source context 4 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ValuationTheory.DiscreteValuationField ProCGroups.Abelian
open ProCGroups.FiniteStepSolvableQuotients
universe u v

Lean source · statement

theorem prime_order_detection
    {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), τ ≠ 1 ∧
      ∃ z : abelianModPower Gal(AlgebraicClosure L/L) p,
        relativeGaloisAbelianModPowerTransform K L p τ z ≠ z

Module documentation

Kummer theory and discretely valued fields

Declarations

prime_order_detection