NYLL
Module

PositiveCharacteristicOrientation.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.PositiveCharacteristicOrientation
2 declarations indexed from sourceView source ↗

Module documentation

Infinite orientations from Artin–Schreier obstructions

Imports5
Imported by3

Declarations

theorem

exists_infinite_formalHilbert90_orientation_of_character

L19 ↗
Yamaguchi26AbfaithfulGalois.exists_infinite_formalHilbert90_orientation_of_character
Documentation

A nontrivial mod-p character lifts to an infinite principal-unit orientation.

Source context 2 commands

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

namespace Yamaguchi26AbfaithfulGalois
universe u
Lean source · statement
theorem exists_infinite_formalHilbert90_orientation_of_character
    (p : ℕ) [Fact p.Prime] (K : Type u) [Field K] [CharP K p]
    (χ : Gal(AlgebraicClosure K/K) →ₜ* Multiplicative (ZMod p))
    (hχ : ∃ σ : Gal(AlgebraicClosure K/K), χ σ ≠ 1) :
    ∃ θ : Orientation p Gal(AlgebraicClosure K/K),
      FormalHilbert90 θ ∧ Set.Infinite (Set.range θ)
theorem

exists_infinite_formalHilbert90_orientation_of_artinSchreier

L41 ↗
Yamaguchi26AbfaithfulGalois.exists_infinite_formalHilbert90_orientation_of_artinSchreier
Documentation

A nonsurjective Artin–Schreier map supplies an infinite orientation with formal Hilbert 90 on the actual absolute Galois group, including imperfect fields.

Source context 2 commands

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

namespace Yamaguchi26AbfaithfulGalois
universe u
Lean source · statement
theorem exists_infinite_formalHilbert90_orientation_of_artinSchreier
    (p : ℕ) [Fact p.Prime] (K : Type u) [Field K] [CharP K p]
    (hAS : ∃ a : K, ∀ x : K, x ^ p - x ≠ a) :
    ∃ θ : Orientation p Gal(AlgebraicClosure K/K),
      FormalHilbert90 θ ∧ Set.Infinite (Set.range θ)

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