NYLL
Module

MixedCharacteristicCharacters.lean

Nyll.GaloisCohomology.Kummer.Concrete.MixedCharacteristicCharacters
1 declaration indexed from sourceView source ↗

Module documentation

Prime cyclic characters of mixed-characteristic discretely valued fields

Finiteness of primary roots in every finite extension forces the cyclotomic character to have infinite image. Its image therefore has a cyclic quotient of order equal to the residue characteristic.

Imports5
Imported by2

Declarations

theorem

exists_surjective_prime_character_of_mixedChar

L28 ↗
KummerTheory.exists_surjective_prime_character_of_mixedChar
Documentation

Every mixed-characteristic discretely valued field has a continuous cyclic quotient of residue-prime order.

Source context 3 commands

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

namespace KummerTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type*} [Field K] [CharZero K]
Lean source · statement
theorem exists_surjective_prime_character_of_mixedChar
    (base : DVF K) (p : ℕ) [Fact p.Prime] [CharP base.residueField p] :
    ∃ ψ : Gal(AlgebraicClosure K/K) →ₜ* Multiplicative (ZMod p),
      Function.Surjective ψ

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.