NYLL
Module

CompletionAbelianModPower.lean

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

Module documentation

Injectivity on mod-prime abelianizations of valued completions

When the prime is different from the field characteristic, extension of completion characters separates every class in the local abelian quotient.

Imports4
Imported by2

Declarations

theorem

completion_abelianModPowerMap_injective

L27 ↗
KummerTheory.completion_abelianModPowerMap_injective
Documentation

The completion embedding induces an injection on absolute Galois abelianizations modulo a prime different from the field characteristic.

Source context 4 commands

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

namespace KummerTheory
open ValuationTheory.DiscreteValuationField ProCGroups.Abelian
open Field.absoluteGaloisGroup
universe u v
Lean source · statement
theorem completion_abelianModPowerMap_injective
    {K : Type u} [Field K] (D : DVF.{u, v} K) (q : ℕ)
    [Fact q.Prime] [NeZero (q : K)] :
    Function.Injective (abelianModPowerMap q
      (map (algebraMap K D.valuation.Completion)))

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