Module

MixedCharacteristicPrimeDetection.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.MixedCharacteristicPrimeDetection

1 declaration indexed from sourceView source ↗

Module documentation

Prime-degree detection for arbitrary mixed-characteristic discrete valuations

A prolongation is either invariant under every automorphism or is moved by one. Completion detects the first case, and simultaneous character approximation detects the second case. No completeness or Henselian hypothesis is required.

Imports3

Imported by3

theorem

prime_order_detection_of_mixedChar

L26 ↗

Yamaguchi26AbfaithfulGalois.prime_order_detection_of_mixedChar

Documentation

Prime-degree Galois extensions of a mixed-characteristic discretely valued field act nontrivially on abelianization modulo the residue prime.

Source context 3 commands

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

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

Lean source · statement

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

Module documentation

Prime-degree detection for arbitrary mixed-characteristic discrete valuations

Declarations

prime_order_detection_of_mixedChar