NYLL
Module

ArtinSchreier.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.ArtinSchreier
2 declarations indexed from sourceView source ↗

Module documentation

Artin–Schreier roots in a Henselian valuation ring

In characteristic p, the maximal ideal is contained in the image of x ↦ x^p - x. Consequently this additive image is open in the valued field.

Imports4
Imported by2

Declarations

theorem

exists_pow_sub_eq_of_valuation_lt_one

L25 ↗
ValuationTheory.exists_pow_sub_eq_of_valuation_lt_one
Documentation

Every element of positive valuation is an Artin–Schreier difference in a Henselian valued field of positive characteristic.

Source context 2 commands

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

namespace ValuationTheory
open Polynomial
Lean source · statement
theorem exists_pow_sub_eq_of_valuation_lt_one
    {K Γ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ)
    [HenselianRing v.valuationSubring (IsLocalRing.maximalIdeal v.valuationSubring)]
    (p : ℕ) [Fact p.Prime] [CharP K p] (a : K) (ha : v a < 1) :
    ∃ b : K, b ^ p - b = a
theorem

isOpen_artinSchreier_range

L58 ↗
ValuationTheory.isOpen_artinSchreier_range
Documentation

The additive Artin–Schreier image is open in a Henselian valued field of characteristic p.

Source context 2 commands

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

namespace ValuationTheory
open Polynomial
Lean source · statement
theorem isOpen_artinSchreier_range
    {K Γ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ] [Valued K Γ]
    [HenselianRing (Valued.v : Valuation K Γ).valuationSubring
      (IsLocalRing.maximalIdeal (Valued.v : Valuation K Γ).valuationSubring)]
    (p : ℕ) [Fact p.Prime] [CharP K p] :
    IsOpen (((frobenius K p).toAddMonoidHom - AddMonoidHom.id K).range : Set K)

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