NYLL
Module

Basic.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.Basic
47 declarations indexed from sourceView source ↗

Module documentation

Local fields

A local-field package here is a chosen complete discretely valued field with finite residue field. The topology-first mathlib class remains available through imports; this file only adds the chosen-valuation API needed downstream.

Imports9
Imported by11

Declarations

structure

LocalField

L34 ↗
LocalFieldTheory.DiscreteValuationField.LocalField
Documentation

A local field with a chosen complete discrete valuation and finite residue field.

Source context 3 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
Lean source · full declaration
structure LocalField (K : Type u) [Field K] extends CompleteDVF.{u, v} K where
  /-- The residue field of the chosen complete discrete valuation is finite. -/
  [residueFinite : Finite toCompleteDVF.residueField]
abbrev

residueField

L45 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueField
Documentation

The residue field of a local field package.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
abbrev residueField (F : LocalField.{u, v} K) : Type u
abbrev

valuationSubring

L49 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuationSubring
Documentation

The valuation subring of a local field package.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
abbrev valuationSubring (F : LocalField.{u, v} K) : Type u
abbrev

maximalIdeal

L53 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.maximalIdeal
Documentation

The maximal ideal of the valuation subring.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
abbrev maximalIdeal (F : LocalField.{u, v} K) : Ideal F.valuationSubring
abbrev

residueMap

L57 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueMap
Documentation

The residue map of a local field package.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
abbrev residueMap (F : LocalField.{u, v} K) :
    RingHom F.valuationSubring F.residueField
theorem

valuationSubring_isDiscreteValuationRing

L62 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuationSubring_isDiscreteValuationRing
Documentation

The valuation subring of a local field package is a DVR.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuationSubring_isDiscreteValuationRing
    (F : LocalField.{u, v} K) :
    IsDiscreteValuationRing F.valuationSubring
theorem

henselianRing

L69 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.henselianRing
Documentation

The valuation subring of a local field package is Henselian.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem henselianRing (F : LocalField.{u, v} K) :
    HenselianRing F.valuationSubring F.maximalIdeal
theorem

exists_uniformizer

L74 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.exists_uniformizer
Documentation

A local field package has a uniformizer.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem exists_uniformizer (F : LocalField.{u, v} K) :
    ∃ pi : F.valuationSubring, F.toCompleteDVF.valuation.IsUniformizer (pi : K)
abbrev

residueCharacteristic

L79 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueCharacteristic
Documentation

The residue characteristic of a local field.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
abbrev residueCharacteristic (F : LocalField.{u, v} K) : ℕ
theorem

residueCharacteristic_ne_zero

L83 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueCharacteristic_ne_zero
Documentation

Establishes the inequality F.residueCharacteristic ≠ 0.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem residueCharacteristic_ne_zero (F : LocalField.{u, v} K) :
    F.residueCharacteristic ≠ 0
theorem

residueCharacteristic_prime

L88 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueCharacteristic_prime
Documentation

Proves the primality statement Nat.Prime F.residueCharacteristic.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem residueCharacteristic_prime (F : LocalField.{u, v} K) :
    Nat.Prime F.residueCharacteristic
instance

residueField_charP_residueCharacteristic

L96 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueField_charP_residueCharacteristic
Documentation

The target has the stated characteristic: CharP F.residueField F.residueCharacteristic.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
instance residueField_charP_residueCharacteristic (F : LocalField.{u, v} K) :
    CharP F.residueField F.residueCharacteristic
instance

fact_prime

L101 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueCharacteristic.fact_prime
Documentation

Registers the mathematical fact Fact F.residueCharacteristic.Prime for typeclass inference.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
instance residueCharacteristic.fact_prime (F : LocalField.{u, v} K) :
    Fact F.residueCharacteristic.Prime
theorem

residueCharacteristic_natCast_residue_eq_zero

L108 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueCharacteristic_natCast_residue_eq_zero
Documentation

The residue characteristic vanishes after reduction modulo the maximal ideal. This is the first characteristic input in the converse direction of the local-field structure theory, the local-field structure classification.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem residueCharacteristic_natCast_residue_eq_zero
    (F : LocalField.{u, v} K) :
    F.residueMap (F.residueCharacteristic : F.valuationSubring) = 0
theorem

residueCharacteristic_natCast_mem_maximalIdeal

L120 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueCharacteristic_natCast_mem_maximalIdeal
Documentation

The residue characteristic belongs to the maximal ideal of the valuation ring.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem residueCharacteristic_natCast_mem_maximalIdeal
    (F : LocalField.{u, v} K) :
    (F.residueCharacteristic : F.valuationSubring) ∈ F.maximalIdeal
theorem

valuation_residueCharacteristic_natCast_lt_one

L128 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_residueCharacteristic_natCast_lt_one
Documentation

Valuatively, the residue characteristic lies in the open unit ball.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_residueCharacteristic_natCast_lt_one
    (F : LocalField.{u, v} K) :
    F.toCompleteDVF.valuation
      ((F.residueCharacteristic : F.valuationSubring) : K) < 1
theorem

valuation_natCast_residueCharacteristic_lt_one

L137 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_natCast_residueCharacteristic_lt_one
Documentation

Field-level form of the previous valuation estimate.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_natCast_residueCharacteristic_lt_one
    (F : LocalField.{u, v} K) :
    F.toCompleteDVF.valuation (F.residueCharacteristic : K) < 1
theorem

natCast_residueCharacteristic_ne_zero_of_charZero

L150 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.natCast_residueCharacteristic_ne_zero_of_charZero
Documentation

In mixed characteristic, the residue characteristic is a nonzero element of the field even though it reduces to zero.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem natCast_residueCharacteristic_ne_zero_of_charZero
    (F : LocalField.{u, v} K) [CharZero K] :
    (F.residueCharacteristic : K) ≠ 0
theorem

intCast_mem_maximalIdeal_iff_residueCharacteristic_dvd

L157 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.intCast_mem_maximalIdeal_iff_residueCharacteristic_dvd
Documentation

For an arbitrary integer, membership in the maximal ideal is exactly divisibility by the residue characteristic.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem intCast_mem_maximalIdeal_iff_residueCharacteristic_dvd
    (F : LocalField.{u, v} K) (z : ℤ) :
    (z : F.valuationSubring) ∈ F.maximalIdeal ↔
      (F.residueCharacteristic : ℤ) ∣ z
theorem

natCast_mem_maximalIdeal_iff_residueCharacteristic_dvd

L169 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.natCast_mem_maximalIdeal_iff_residueCharacteristic_dvd
Documentation

Natural-number version of intCast_mem_maximalIdeal_iff_residueCharacteristic_dvd.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem natCast_mem_maximalIdeal_iff_residueCharacteristic_dvd
    (F : LocalField.{u, v} K) (n : ℕ) :
    (n : F.valuationSubring) ∈ F.maximalIdeal ↔
      F.residueCharacteristic ∣ n
theorem

valuationSubring_intCast_lt_one_iff_residueCharacteristic_dvd

L178 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuationSubring_intCast_lt_one_iff_residueCharacteristic_dvd
Documentation

Integer-valued maximal-ideal membership as a valuation inequality.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuationSubring_intCast_lt_one_iff_residueCharacteristic_dvd
    (F : LocalField.{u, v} K) (z : ℤ) :
    F.toCompleteDVF.valuation ((z : F.valuationSubring) : K) < 1 ↔
      (F.residueCharacteristic : ℤ) ∣ z
theorem

valuationSubring_natCast_lt_one_iff_residueCharacteristic_dvd

L187 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuationSubring_natCast_lt_one_iff_residueCharacteristic_dvd
Documentation

Natural-number-valued maximal-ideal membership as a valuation inequality.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuationSubring_natCast_lt_one_iff_residueCharacteristic_dvd
    (F : LocalField.{u, v} K) (n : ℕ) :
    F.toCompleteDVF.valuation ((n : F.valuationSubring) : K) < 1 ↔
      F.residueCharacteristic ∣ n
theorem

isUnit_intCast_iff_not_residueCharacteristic_dvd

L197 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.isUnit_intCast_iff_not_residueCharacteristic_dvd
Documentation

An integer prime to the residue characteristic is a unit in the valuation ring.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem isUnit_intCast_iff_not_residueCharacteristic_dvd
    (F : LocalField.{u, v} K) (z : ℤ) :
    IsUnit (z : F.valuationSubring) ↔
      ¬ (F.residueCharacteristic : ℤ) ∣ z
theorem

isUnit_natCast_iff_not_residueCharacteristic_dvd

L210 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.isUnit_natCast_iff_not_residueCharacteristic_dvd
Documentation

A natural number prime to the residue characteristic is a unit in the valuation ring.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem isUnit_natCast_iff_not_residueCharacteristic_dvd
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUnit (n : F.valuationSubring) ↔
      ¬ F.residueCharacteristic ∣ n
theorem

valuationSubring_intCast_eq_one_of_not_residueCharacteristic_dvd

L219 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuationSubring_intCast_eq_one_of_not_residueCharacteristic_dvd
Documentation

An integer prime to the residue characteristic has valuation one.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuationSubring_intCast_eq_one_of_not_residueCharacteristic_dvd
    (F : LocalField.{u, v} K) {z : ℤ}
    (hz : ¬ (F.residueCharacteristic : ℤ) ∣ z) :
    F.toCompleteDVF.valuation ((z : F.valuationSubring) : K) = 1
theorem

valuationSubring_natCast_eq_one_of_not_residueCharacteristic_dvd

L236 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuationSubring_natCast_eq_one_of_not_residueCharacteristic_dvd
Documentation

A natural number prime to the residue characteristic has valuation one.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuationSubring_natCast_eq_one_of_not_residueCharacteristic_dvd
    (F : LocalField.{u, v} K) {n : ℕ}
    (hn : ¬ F.residueCharacteristic ∣ n) :
    F.toCompleteDVF.valuation ((n : F.valuationSubring) : K) = 1
theorem

valuation_intCast_lt_one_iff_residueCharacteristic_dvd

L253 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_intCast_lt_one_iff_residueCharacteristic_dvd
Documentation

Field-level integer valuation criterion for the residue characteristic.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_intCast_lt_one_iff_residueCharacteristic_dvd
    (F : LocalField.{u, v} K) (z : ℤ) :
    F.toCompleteDVF.valuation (z : K) < 1 ↔
      (F.residueCharacteristic : ℤ) ∣ z
theorem

valuation_natCast_lt_one_iff_residueCharacteristic_dvd

L265 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_natCast_lt_one_iff_residueCharacteristic_dvd
Documentation

Field-level natural-number valuation criterion for the residue characteristic.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_natCast_lt_one_iff_residueCharacteristic_dvd
    (F : LocalField.{u, v} K) (n : ℕ) :
    F.toCompleteDVF.valuation (n : K) < 1 ↔
      F.residueCharacteristic ∣ n
theorem

valuation_intCast_eq_one_of_not_residueCharacteristic_dvd

L277 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_intCast_eq_one_of_not_residueCharacteristic_dvd
Documentation

Field-level integer valuation-one criterion away from the residue characteristic.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_intCast_eq_one_of_not_residueCharacteristic_dvd
    (F : LocalField.{u, v} K) {z : ℤ}
    (hz : ¬ (F.residueCharacteristic : ℤ) ∣ z) :
    F.toCompleteDVF.valuation (z : K) = 1
theorem

valuation_natCast_eq_one_of_not_residueCharacteristic_dvd

L289 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_natCast_eq_one_of_not_residueCharacteristic_dvd
Documentation

Field-level natural-number valuation-one criterion away from the residue characteristic.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_natCast_eq_one_of_not_residueCharacteristic_dvd
    (F : LocalField.{u, v} K) {n : ℕ}
    (hn : ¬ F.residueCharacteristic ∣ n) :
    F.toCompleteDVF.valuation (n : K) = 1
theorem

valuation_intCast_le_one

L301 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_intCast_le_one
Documentation

Every integer lies in the valuation subring. This is the denominator control input for the mixed-characteristic branch of the local-field structure classification.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_intCast_le_one (F : LocalField.{u, v} K) (z : ℤ) :
    F.toCompleteDVF.valuation (z : K) ≤ 1
theorem

valuation_natCast_le_one

L316 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_natCast_le_one
Documentation

Every natural number lies in the valuation subring.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_natCast_le_one (F : LocalField.{u, v} K) (n : ℕ) :
    F.toCompleteDVF.valuation (n : K) ≤ 1
theorem

valuation_ratCast_eq_intCast_of_not_residueCharacteristic_dvd_den

L322 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_ratCast_eq_intCast_of_not_residueCharacteristic_dvd_den
Documentation

If the denominator of a rational number is prime to the residue characteristic, then its valuation is the valuation of its numerator.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_ratCast_eq_intCast_of_not_residueCharacteristic_dvd_den
    (F : LocalField.{u, v} K) (q : ℚ)
    (hden : ¬ F.residueCharacteristic ∣ q.den) :
    F.toCompleteDVF.valuation (q : K) =
      F.toCompleteDVF.valuation (q.num : K)
theorem

valuation_ratCast_le_one_of_not_residueCharacteristic_dvd_den

L342 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_ratCast_le_one_of_not_residueCharacteristic_dvd_den
Documentation

A rational number with denominator prime to the residue characteristic lies in the valuation subring. This is the local ℤ_(p) input for the converse classification in the local-field structure theory, the local-field structure classification.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_ratCast_le_one_of_not_residueCharacteristic_dvd_den
    (F : LocalField.{u, v} K) (q : ℚ)
    (hden : ¬ F.residueCharacteristic ∣ q.den) :
    F.toCompleteDVF.valuation (q : K) ≤ 1
theorem

ratCast_mem_valuationSubring_of_not_residueCharacteristic_dvd_den

L351 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.ratCast_mem_valuationSubring_of_not_residueCharacteristic_dvd_den
Documentation

Valuation-subring membership form of valuation_ratCast_le_one_of_not_residueCharacteristic_dvd_den.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem ratCast_mem_valuationSubring_of_not_residueCharacteristic_dvd_den
    (F : LocalField.{u, v} K) (q : ℚ)
    (hden : ¬ F.residueCharacteristic ∣ q.den) :
    (q : K) ∈ F.toCompleteDVF.valuation.valuationSubring
theorem

not_residueCharacteristic_dvd_rat_num_of_dvd_den

L360 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.not_residueCharacteristic_dvd_rat_num_of_dvd_den
Documentation

In a reduced rational number, if the denominator is divisible by the residue characteristic then the numerator is not.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem not_residueCharacteristic_dvd_rat_num_of_dvd_den
    (F : LocalField.{u, v} K) (q : ℚ)
    (hden : F.residueCharacteristic ∣ q.den) :
    ¬ (F.residueCharacteristic : ℤ) ∣ q.num
theorem

valuation_ratCast_le_one_iff_not_residueCharacteristic_dvd_den

L374 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_ratCast_le_one_iff_not_residueCharacteristic_dvd_den
Documentation

For mixed-characteristic local fields, the rational numbers lying in the valuation subring are exactly those whose denominator is prime to the residue characteristic.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_ratCast_le_one_iff_not_residueCharacteristic_dvd_den
    (F : LocalField.{u, v} K) [CharZero K] (q : ℚ) :
    F.toCompleteDVF.valuation (q : K) ≤ 1 ↔
      ¬ F.residueCharacteristic ∣ q.den
theorem

ratCast_mem_valuationSubring_iff_not_residueCharacteristic_dvd_den

L413 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.ratCast_mem_valuationSubring_iff_not_residueCharacteristic_dvd_den
Documentation

Valuation-subring membership version of valuation_ratCast_le_one_iff_not_residueCharacteristic_dvd_den.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem ratCast_mem_valuationSubring_iff_not_residueCharacteristic_dvd_den
    (F : LocalField.{u, v} K) [CharZero K] (q : ℚ) :
    (q : K) ∈ F.toCompleteDVF.valuation.valuationSubring ↔
      ¬ F.residueCharacteristic ∣ q.den
theorem

valuation_ratCast_le_one_iff_padicValuation_le_one

L422 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_ratCast_le_one_iff_padicValuation_le_one
Documentation

The restriction of the local-field valuation to ℚ has the same valuation subring as the p-adic valuation, where p is the residue characteristic.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_ratCast_le_one_iff_padicValuation_le_one
    (F : LocalField.{u, v} K) [CharZero K] (q : ℚ) :
    F.toCompleteDVF.valuation (q : K) ≤ 1 ↔
      Rat.padicValuation F.residueCharacteristic q ≤ 1
theorem

ratCast_mem_valuationSubring_iff_padicValuation_le_one

L432 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.ratCast_mem_valuationSubring_iff_padicValuation_le_one
Documentation

Valuation-subring membership version of valuation_ratCast_le_one_iff_padicValuation_le_one.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem ratCast_mem_valuationSubring_iff_padicValuation_le_one
    (F : LocalField.{u, v} K) [CharZero K] (q : ℚ) :
    (q : K) ∈ F.toCompleteDVF.valuation.valuationSubring ↔
      Rat.padicValuation F.residueCharacteristic q ≤ 1
theorem

ratCast_preimage_valuationSubring_eq_padicValuationSubring

L441 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.ratCast_preimage_valuationSubring_eq_padicValuationSubring
Documentation

The valuation subring pulled back from K along the rational embedding is the usual p-adic valuation subring of ℚ.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem ratCast_preimage_valuationSubring_eq_padicValuationSubring
    (F : LocalField.{u, v} K) [CharZero K] :
    F.toCompleteDVF.valuation.valuationSubring.comap (Rat.castHom K) =
      (Rat.padicValuation F.residueCharacteristic).valuationSubring
theorem

ratCast_valuation_isEquiv_padicValuation

L451 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.ratCast_valuation_isEquiv_padicValuation
Documentation

The valuation on K, restricted along ℚ → K, is equivalent to the p-adic valuation on ℚ.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem ratCast_valuation_isEquiv_padicValuation
    (F : LocalField.{u, v} K) [CharZero K] :
    (F.toCompleteDVF.valuation.comap (Rat.castHom K)).IsEquiv
      (Rat.padicValuation F.residueCharacteristic)
theorem

residueField_charP_of_charP

L465 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueField_charP_of_charP
Documentation

In positive equal characteristic, the residue field has the same characteristic as the local field.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem residueField_charP_of_charP
    (F : LocalField.{u, v} K) (p : ℕ) [CharP K p] (hp : p ≠ 0) :
    CharP F.residueField p
theorem

residueCharacteristic_eq_of_charP

L472 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueCharacteristic_eq_of_charP
Documentation

In positive equal characteristic, the residue characteristic is the characteristic of the local field.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem residueCharacteristic_eq_of_charP
    (F : LocalField.{u, v} K) (p : ℕ) [CharP K p] (hp : p ≠ 0) :
    F.residueCharacteristic = p
theorem

residueExtension_isAlgebraic_of_finite

L481 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueExtension_isAlgebraic_of_finite
Documentation

Any finite residue-field algebra over a local field residue field is algebraic.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem residueExtension_isAlgebraic_of_finite
    (F : LocalField.{u, v} K) {k : Type w} [Field k]
    [Algebra F.residueField k] [Finite k] :
    Algebra.IsAlgebraic F.residueField k
theorem

residueExtension_isSeparable_of_finite

L491 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueExtension_isSeparable_of_finite
Documentation

Any finite residue-field algebra over a local field residue field is separable.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem residueExtension_isSeparable_of_finite
    (F : LocalField.{u, v} K) {k : Type w} [Field k]
    [Algebra F.residueField k] [Finite k] :
    Algebra.IsSeparable F.residueField k
theorem

residueExtension_isSeparable

L502 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.residueExtension_isSeparable
Documentation

The residue-field algebra between two local-field packages is separable.

Source context 6 commands

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

universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
attribute [instance] LocalField.residueFinite
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem residueExtension_isSeparable
    (F : LocalField.{u, v} K) {L : Type w} [Field L]
    (E : LocalField.{w, x} L) [Algebra F.residueField E.residueField] :
    Algebra.IsSeparable F.residueField E.residueField

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