NYLL
Module

CharacterClasses.lean

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

Module documentation

Artin–Schreier classes and all continuous cyclic characters

Additive Hilbert 90 realizes every character by a root. Changing the field element by an Artin–Schreier coboundary leaves its character unchanged.

Imports5
Imported by2

Declarations

theorem

exists_rootCharacter_eq

L26 ↗
ArtinSchreierTheory.exists_rootCharacter_eq
Documentation

Every continuous cyclic character is the difference character of a root.

Source context 3 commands

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

namespace ArtinSchreierTheory
section Surjectivity
variable (p : ℕ) [Fact p.Prime] {K Ω : Type*} [Field K] [Field Ω]
  [CharP Ω p] [Algebra K Ω] [IsGalois K Ω]
Lean source · statement
theorem exists_rootCharacter_eq (χ : Gal(Ω/K) →ₜ* Multiplicative (ZMod p)) :
    ∃ (a : K) (β : Ω) (hβ : β ^ p - β = algebraMap K Ω a),
      rootCharacter p Ω a β hβ = χ
theorem

rootCharacter_eq_of_class_eq

L65 ↗
ArtinSchreierTheory.rootCharacter_eq_of_class_eq
Documentation

Equal additive Artin–Schreier classes give equal continuous characters.

Source context 3 commands

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

namespace ArtinSchreierTheory
section Classes
variable (p : ℕ) [Fact p.Prime] {K Ω : Type*} [Field K] [Field Ω]
  [CharP K p] [CharP Ω p] [Algebra K Ω] [Algebra.IsIntegral K Ω]
Lean source · statement
theorem rootCharacter_eq_of_class_eq (a b : K) (β γ : Ω)
    (hβ : β ^ p - β = algebraMap K Ω a)
    (hγ : γ ^ p - γ = algebraMap K Ω b)
    (hab : (a : K ⧸ ((frobenius K p).toAddMonoidHom - AddMonoidHom.id K).range) =
      (b : K ⧸ ((frobenius K p).toAddMonoidHom - AddMonoidHom.id K).range)) :
    rootCharacter p Ω a β hβ = rootCharacter p Ω b γ hγ

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