ArtinSchreierTheory.exists_character_moved_by_map_of_pow_sub_ne
A nonzero difference of Artin--Schreier classes detects the actual absolute Galois map associated to the field automorphism.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ArtinSchreierTheory
open Field.absoluteGaloisGroup ValuationTheory.Completion
variable (p : ℕ) [Fact p.Prime] {K : Type*} [Field K] [CharP K p]Lean source · statement
theorem exists_character_moved_by_map_of_pow_sub_ne
(τ : K ≃+* K) (a : K) (ha : ∀ y : K, y ^ p - y ≠ τ a - a) :
∃ χ : Gal(AlgebraicClosure K/K) →ₜ* Multiplicative (ZMod p),
∃ σ : Gal(AlgebraicClosure K/K),
χ (map τ.toRingHom σ) ≠ χ σ