NYLL
Module

Depth.lean

Nyll.AlgebraicCurves.Places.Depth
24 declarations indexed from sourceView source ↗

Module documentation

Depth

Imports3
Imported by1

Declarations

def

HasValuation

L31 ↗
AlgebraicCurve.Place.HasValuation
Documentation

The condition that the residue value has the specified valuation in the residue field.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
Lean source · statement
def HasValuation (f : F) (γ : A.ValueGroup) : Prop
theorem

hasValuation_iff

L34 ↗
AlgebraicCurve.Place.hasValuation_iff
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
Lean source · statement
theorem hasValuation_iff (f : F) (γ : A.ValueGroup) :
    V.HasValuation A f γ ↔ ∃ a : L, V.HasValue f a ∧ A.valuation a = γ
def

HasDepth

L40 ↗
AlgebraicCurve.Place.HasDepth
Documentation

The condition that the residue value has valuation equal to the indicated power of the parameter.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
Lean source · statement
def HasDepth (f : F) (ϖ : L) (n : ℕ) : Prop
theorem

hasDepth_iff

L43 ↗
AlgebraicCurve.Place.hasDepth_iff
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
Lean source · statement
theorem hasDepth_iff (f : F) (ϖ : L) (n : ℕ) :
    V.HasDepth A f ϖ n ↔ ∃ a : L, V.HasValue f a ∧ A.valuation a = A.valuation ϖ ^ n
def

DepthBetween

L48 ↗
AlgebraicCurve.Place.DepthBetween
Documentation

The condition that the residue value lies strictly between the two parameter-power bounds.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
Lean source · statement
def DepthBetween (f : F) (ϖ : L) (m n : ℕ) : Prop
theorem

depthBetween_iff

L51 ↗
AlgebraicCurve.Place.depthBetween_iff
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
Lean source · statement
theorem depthBetween_iff (f : F) (ϖ : L) (m n : ℕ) :
    V.DepthBetween A f ϖ m n ↔
      ∃ a : L, V.HasValue f a ∧ A.valuation ϖ ^ n < A.valuation a ∧ A.valuation a < A.valuation ϖ ^
        m
theorem

hasValuation

L59 ↗
AlgebraicCurve.Place.HasDepth.hasValuation
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
variable {A V}
Lean source · statement
theorem HasDepth.hasValuation {f : F} {ϖ : L} {n : ℕ} (h : V.HasDepth A f ϖ n) :
    V.HasValuation A f (A.valuation ϖ ^ n)
theorem

mul

L63 ↗
AlgebraicCurve.Place.HasValuation.mul
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
variable {A V}
Lean source · statement
theorem HasValuation.mul {f g : F} {γ δ : A.ValueGroup} (hf : V.HasValuation A f γ) (hg :
  V.HasValuation A g δ) :
    V.HasValuation A (f * g) (γ * δ)
theorem

mul

L70 ↗
AlgebraicCurve.Place.HasDepth.mul
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
variable {A V}
Lean source · statement
theorem HasDepth.mul {f g : F} {ϖ : L} {m n : ℕ} (hf : V.HasDepth A f ϖ m) (hg : V.HasDepth A g ϖ
  n) :
    V.HasDepth A (f * g) ϖ (m + n)
theorem

pow

L76 ↗
AlgebraicCurve.Place.HasDepth.pow
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
variable {A V}
Lean source · statement
theorem HasDepth.pow {f : F} {ϖ : L} {n : ℕ} (hf : V.HasDepth A f ϖ n) (d : ℕ) :
    V.HasDepth A (f ^ d) ϖ (d * n)
theorem

hasValuation_algebraMap

L89 ↗
AlgebraicCurve.Place.hasValuation_algebraMap
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
variable {A V}
variable (A V)
Lean source · statement
theorem hasValuation_algebraMap (c : L) : V.HasValuation A (algebraMap L F c) (A.valuation c)
theorem

hasDepth_algebraMap_pow

L92 ↗
AlgebraicCurve.Place.hasDepth_algebraMap_pow
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
variable {A V}
variable (A V)
Lean source · statement
theorem hasDepth_algebraMap_pow (ϖ : L) (n : ℕ) : V.HasDepth A (algebraMap L F (ϖ ^ n)) ϖ n
theorem

hasDepth_one_zero

L95 ↗
AlgebraicCurve.Place.hasDepth_one_zero
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
variable {A V}
variable (A V)
Lean source · statement
theorem hasDepth_one_zero (ϖ : L) : V.HasDepth A (1 : F) ϖ 0
theorem

smul

L100 ↗
AlgebraicCurve.Place.HasValuation.smul
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
variable {A V}
variable (A V)
variable {A V}
Lean source · statement
theorem HasValuation.smul (g : SemilinearAut L F)
    (hg : ∀ a : L, A.valuation (SemilinearAut.baseAut g a) = A.valuation a)
    {f : F} {γ : A.ValueGroup} (h : V.HasValuation A f γ) :
    (g • V).HasValuation A (g • f) γ
theorem

smul

L107 ↗
AlgebraicCurve.Place.HasDepth.smul
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
variable {A V}
variable (A V)
variable {A V}
Lean source · statement
theorem HasDepth.smul (g : SemilinearAut L F)
    (hg : ∀ a : L, A.valuation (SemilinearAut.baseAut g a) = A.valuation a)
    {f : F} {ϖ : L} {n : ℕ} (h : V.HasDepth A f ϖ n) :
    (g • V).HasDepth A (g • f) ϖ n
theorem

smul

L113 ↗
AlgebraicCurve.Place.DepthBetween.smul
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
variable {A V}
variable (A V)
variable {A V}
Lean source · statement
theorem DepthBetween.smul (g : SemilinearAut L F)
    (hg : ∀ a : L, A.valuation (SemilinearAut.baseAut g a) = A.valuation a)
    {f : F} {ϖ : L} {m n : ℕ} (h : V.DepthBetween A f ϖ m n) :
    (g • V).DepthBetween A (g • f) ϖ m n
theorem

eq_valuation_evalAt

L124 ↗
AlgebraicCurve.Place.HasValuation.eq_valuation_evalAt
Source context 9 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
variable {A V}
variable (A V)
variable {A V}
variable (A V)
Lean source · statement
theorem HasValuation.eq_valuation_evalAt {f : F} {γ : A.ValueGroup} (hV : V.IsRational) (h :
  V.HasValuation A f γ) :
    γ = A.valuation (V.evalAt f)
theorem

hasValuation_iff_valuation_evalAt

L132 ↗
AlgebraicCurve.Place.hasValuation_iff_valuation_evalAt
Source context 9 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
variable {A V}
variable (A V)
variable {A V}
variable (A V)
Lean source · statement
theorem hasValuation_iff_valuation_evalAt (hV : V.IsRational) (f : F) (γ : A.ValueGroup) :
    V.HasValuation A f γ ↔ ∃ _ : f ∈ V.toValuationSubring, A.valuation (V.evalAt f) = γ
theorem

hasDepth_iff_valuation_evalAt

L143 ↗
AlgebraicCurve.Place.hasDepth_iff_valuation_evalAt
Source context 9 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Place
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable (A : ValuationSubring L) (V : Place L F)
variable {A V}
variable (A V)
variable {A V}
variable (A V)
Lean source · statement
theorem hasDepth_iff_valuation_evalAt (hV : V.IsRational) (f : F) (ϖ : L) (n : ℕ) :
    V.HasDepth A f ϖ n ↔ ∃ _ : f ∈ V.toValuationSubring, A.valuation (V.evalAt f) = A.valuation ϖ ^
      n
def

IsAtDepth

L157 ↗
ValuationSubring.IsAtDepth
Documentation

The condition that the valuation of the element equals the indicated parameter power.

Source context 3 commands

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

noncomputable section
namespace ValuationSubring
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
Lean source · statement
def IsAtDepth (O : ValuationSubring F) (f : F) (ϖ : L) (n : ℕ) : Prop
theorem

isAtDepth_iff

L160 ↗
ValuationSubring.isAtDepth_iff
Source context 3 commands

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

noncomputable section
namespace ValuationSubring
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
Lean source · statement
theorem isAtDepth_iff (O : ValuationSubring F) (f : F) (ϖ : L) (n : ℕ) :
    O.IsAtDepth f ϖ n ↔ O.valuation f = O.valuation (algebraMap L F ϖ) ^ n
theorem

mul

L166 ↗
ValuationSubring.IsAtDepth.mul
Source context 4 commands

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

noncomputable section
namespace ValuationSubring
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable {O : ValuationSubring F}
Lean source · statement
theorem IsAtDepth.mul {f g : F} {ϖ : L} {m n : ℕ} (hf : O.IsAtDepth f ϖ m) (hg : O.IsAtDepth g ϖ n)
  :
    O.IsAtDepth (f * g) ϖ (m + n)
theorem

isAtDepth_algebraMap_pow

L173 ↗
ValuationSubring.isAtDepth_algebraMap_pow
Source context 5 commands

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

noncomputable section
namespace ValuationSubring
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable {O : ValuationSubring F}
variable (O) in
Lean source · statement
theorem isAtDepth_algebraMap_pow (ϖ : L) (n : ℕ) : O.IsAtDepth (algebraMap L F (ϖ ^ n)) ϖ n
theorem

isAtDepth_zero_of_isUnit

L177 ↗
ValuationSubring.isAtDepth_zero_of_isUnit
Source context 5 commands

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

noncomputable section
namespace ValuationSubring
variable {L F : Type*} [Field L] [Field F] [Algebra L F]
variable {O : ValuationSubring F}
variable (O) in
Lean source · statement
theorem isAtDepth_zero_of_isUnit {f : O} (hf : IsUnit f) (ϖ : L) : O.IsAtDepth (f : F) ϖ 0

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