NYLL
Module

ValuationCharacters.lean

Nyll.GaloisCohomology.ArtinSchreier.ValuationCharacters
2 declarations indexed from sourceView source ↗

Module documentation

Nontrivial prime cyclic characters from discrete valuations

Imports4
Imported by2

Declarations

theorem

exists_nontrivial_absolute_character_of_DVF

L21 ↗
ArtinSchreierTheory.exists_nontrivial_absolute_character_of_DVF
Documentation

A discrete valuation in characteristic p produces a nontrivial continuous prime cyclic character on the actual absolute Galois group.

Source context 4 commands

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

namespace ArtinSchreierTheory
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem exists_nontrivial_absolute_character_of_DVF
    (D : DVF.{u, v} K) (p : ℕ) [Fact p.Prime] [CharP K p] :
    ∃ χ : Gal(AlgebraicClosure K/K) →ₜ* Multiplicative (ZMod p),
      ∃ σ : Gal(AlgebraicClosure K/K), χ σ ≠ 1
theorem

exists_nontrivial_completion_character_of_DVF

L37 ↗
ArtinSchreierTheory.exists_nontrivial_completion_character_of_DVF
Documentation

The valued completion of a discrete valuation in characteristic p has a nontrivial continuous prime cyclic character.

Source context 4 commands

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

namespace ArtinSchreierTheory
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem exists_nontrivial_completion_character_of_DVF
    (D : DVF.{u, v} K) (p : ℕ) [Fact p.Prime] [CharP K p] :
    ∃ χ : Gal(AlgebraicClosure D.valuation.Completion/D.valuation.Completion) →ₜ*
      Multiplicative (ZMod p),
      ∃ σ : Gal(AlgebraicClosure D.valuation.Completion/D.valuation.Completion), χ σ ≠ 1

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