Module

Basic.lean

Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Basic

36 declarations indexed from sourceView source ↗

Module documentation

Prime divisors of function fields

This file introduces the model-independent form of a prime divisor used in Fried--Jarden, Chapter 6. The underlying discrete K-valuation of F is represented by a valuation subring of F which

is a discrete valuation ring, and
contains the image of the constant field K.

The discrete-valuation-ring condition forces the valuation subring to be proper, so nontriviality is derived rather than stored as redundant data. An FJ prime divisor additionally has residue field finite over K; this condition is part of FunctionFieldPrimeDivisor, so its degree is a genuine positive finite extension degree.

For a K-subalgebra A of F, being finite at the prime divisor means that every element of A belongs to the valuation subring. In that case the center on A is the contraction of the valuation ring's maximal ideal. This center is prime; no maximality assertion is made without additional finiteness or integrality hypotheses on the model.

Imports3

Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.RingTheory.Valuation.ValuationSubring

Imported by6

structure

DiscreteKValuation

L53 ↗

FieldArithmetic.Chapter06.DiscreteKValuation

Documentation

A model-independent discrete K-valuation of F.

The valuation subring property says that its fraction field is the ambient field F. Discreteness is recorded by the DVR instance, while algebraMap_mem says that the valuation is trivial on the constant field in the valuation-ring sense.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]

Lean source · full declaration

structure DiscreteKValuation where
  /-- The valuation subring of the ambient function field. -/
  valuationSubring : ValuationSubring F
  /-- The valuation subring is a discrete valuation ring. -/
  isDiscreteValuationRing :
    IsDiscreteValuationRing valuationSubring
  /-- Every constant lies in the valuation subring. -/
  algebraMap_mem : ∀ x : K, algebraMap K F x ∈ valuationSubring

instance

(anonymous instance)

L66 ↗

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace DiscreteKValuation
variable {K F}

Lean source · statement

instance (v : DiscreteKValuation K F) :
    IsDiscreteValuationRing v.valuationSubring

def

constantRingHom

L71 ↗

FieldArithmetic.Chapter06.DiscreteKValuation.constantRingHom

Documentation

The constant-field embedding into the valuation ring.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace DiscreteKValuation
variable {K F}

Lean source · full declaration

def constantRingHom (v : DiscreteKValuation K F) :
    K →+* v.valuationSubring where
  toFun x := ⟨algebraMap K F x, v.algebraMap_mem x⟩
  map_zero' := Subtype.ext (map_zero (algebraMap K F))
  map_one' := Subtype.ext (map_one (algebraMap K F))
  map_add' x y := Subtype.ext (map_add (algebraMap K F) x y)
  map_mul' x y := Subtype.ext (map_mul (algebraMap K F) x y)

instance

(anonymous instance)

L79 ↗

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace DiscreteKValuation
variable {K F}

Lean source · statement

instance (v : DiscreteKValuation K F) :
    Algebra K v.valuationSubring

theorem

coe_algebraMap

L84 ↗

FieldArithmetic.Chapter06.DiscreteKValuation.coe_algebraMap

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace DiscreteKValuation
variable {K F}

Lean source · statement

theorem coe_algebraMap
    (v : DiscreteKValuation K F) (x : K) :
    ((algebraMap K v.valuationSubring x : v.valuationSubring) : F) =
      algebraMap K F x

instance

(anonymous instance)

L90 ↗

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace DiscreteKValuation
variable {K F}

Lean source · statement

instance (v : DiscreteKValuation K F) :
    IsScalarTower K v.valuationSubring F

theorem

valuationSubring_ne_top

L98 ↗

FieldArithmetic.Chapter06.DiscreteKValuation.valuationSubring_ne_top

Documentation

The valuation subring of a prime divisor is proper. This follows from its DVR structure and is therefore not an extra field of FunctionFieldPrimeDivisor.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace DiscreteKValuation
variable {K F}

Lean source · statement

theorem valuationSubring_ne_top
    (v : DiscreteKValuation K F) :
    v.valuationSubring ≠ ⊤

abbrev

ResidueField

L107 ↗

FieldArithmetic.Chapter06.DiscreteKValuation.ResidueField

Documentation

The residue field of a prime divisor.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace DiscreteKValuation
variable {K F}

Lean source · statement

abbrev ResidueField (v : DiscreteKValuation K F)

theorem

residueField_algebraMap_injective

L111 ↗

FieldArithmetic.Chapter06.DiscreteKValuation.residueField_algebraMap_injective

Documentation

The constants embed into the residue field of a discrete K-valuation.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace DiscreteKValuation
variable {K F}

Lean source · statement

theorem residueField_algebraMap_injective
    (v : DiscreteKValuation K F) :
    Function.Injective (algebraMap K v.ResidueField)

def

HasFiniteResidueDegree

L122 ↗

FieldArithmetic.Chapter06.HasFiniteResidueDegree

Documentation

The residue-finiteness condition which distinguishes FJ prime divisors from arbitrary discrete K-valuations.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]

Lean source · statement

def HasFiniteResidueDegree (v : DiscreteKValuation K F) : Prop

structure

FunctionFieldPrimeDivisor

L129 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor

Documentation

A prime divisor of F / K in the sense of Fried--Jarden: a nontrivial discrete K-valuation whose residue field is finite over K.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]

Lean source · full declaration

structure FunctionFieldPrimeDivisor extends DiscreteKValuation K F where
  /-- The residue field of the underlying discrete valuation is finite over K. -/
  residueFinite : HasFiniteResidueDegree K F toDiscreteKValuation

abbrev

ResidueField

L138 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.ResidueField

Documentation

The residue field of a prime divisor.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

abbrev ResidueField (v : FunctionFieldPrimeDivisor K F)

instance

(anonymous instance)

L142 ↗

Documentation

The residue field is finite-dimensional over the constant field.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

instance (v : FunctionFieldPrimeDivisor K F) :
    FiniteDimensional K v.ResidueField

def

degree

L150 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.degree

Documentation

The degree of a prime divisor is the finite vector-space dimension of its residue field over the constant field.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

def degree (v : FunctionFieldPrimeDivisor K F) : ℕ

theorem

one_le_degree

L154 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.one_le_degree

Documentation

The residue degree of a prime divisor is positive.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem one_le_degree (v : FunctionFieldPrimeDivisor K F) :
    1 ≤ v.degree

theorem

residueField_algebraMap_injective

L160 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.residueField_algebraMap_injective

Documentation

The constants embed into the residue field of a prime divisor.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem residueField_algebraMap_injective
    (v : FunctionFieldPrimeDivisor K F) :
    Function.Injective (algebraMap K v.ResidueField)

theorem

valuationSubring_ne_top

L166 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.valuationSubring_ne_top

Documentation

The valuation subring of a prime divisor is proper.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem valuationSubring_ne_top
    (v : FunctionFieldPrimeDivisor K F) :
    v.valuationSubring ≠ ⊤

def

FiniteAlong

L178 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.FiniteAlong

Documentation

The prime divisor is finite along a model map ι : A →ₐ[K] F when the image of every element of A belongs to its valuation ring.

No injectivity condition is needed: this formulation applies directly to coordinate-ring maps into a function field.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

def FiniteAlong
    {A : Type w} [CommRing A] [Algebra K A]
    (v : FunctionFieldPrimeDivisor K F) (ι : A →ₐ[K] F) : Prop

def

finiteAlongRingHom

L184 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.finiteAlongRingHom

Documentation

A model map factored through the valuation ring at a finite prime divisor.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · full declaration

def finiteAlongRingHom
    {A : Type w} [CommRing A] [Algebra K A]
    (v : FunctionFieldPrimeDivisor K F) (ι : A →ₐ[K] F)
    (h : v.FiniteAlong ι) :
    A →+* v.valuationSubring where
  toFun a := ⟨ι a, h a⟩
  map_zero' := Subtype.ext (by simp)
  map_one' := Subtype.ext (by simp)
  map_add' x y := Subtype.ext (by simp)
  map_mul' x y := Subtype.ext (by simp)

def

finiteAlongAlgHom

L196 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.finiteAlongAlgHom

Documentation

The finite-along factorization respects the K-algebra structures.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

def finiteAlongAlgHom
    {A : Type w} [CommRing A] [Algebra K A]
    (v : FunctionFieldPrimeDivisor K F) (ι : A →ₐ[K] F)
    (h : v.FiniteAlong ι) :
    A →ₐ[K] v.valuationSubring

def

centerAlong

L210 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.centerAlong

Documentation

The center along a model map is the contraction of the valuation ring's maximal ideal.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

def centerAlong
    {A : Type w} [CommRing A] [Algebra K A]
    (v : FunctionFieldPrimeDivisor K F) (ι : A →ₐ[K] F)
    (h : v.FiniteAlong ι) : Ideal A

theorem

mem_centerAlong_iff

L218 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.mem_centerAlong_iff

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem mem_centerAlong_iff
    {A : Type w} [CommRing A] [Algebra K A]
    (v : FunctionFieldPrimeDivisor K F) (ι : A →ₐ[K] F)
    (h : v.FiniteAlong ι) (a : A) :
    a ∈ v.centerAlong ι h ↔
      v.finiteAlongRingHom ι h a ∈ maximalIdeal v.valuationSubring

theorem

mem_centerAlong_iff_mem_nonunits

L227 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.mem_centerAlong_iff_mem_nonunits

Documentation

Ambient-field characterization of membership in a center along a map.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem mem_centerAlong_iff_mem_nonunits
    {A : Type w} [CommRing A] [Algebra K A]
    (v : FunctionFieldPrimeDivisor K F) (ι : A →ₐ[K] F)
    (h : v.FiniteAlong ι) (a : A) :
    a ∈ v.centerAlong ι h ↔ ι a ∈ v.valuationSubring.nonunits

theorem

mem_centerAlong_iff_residue_eq_zero

L238 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.mem_centerAlong_iff_residue_eq_zero

Documentation

A model element is in the center along ι exactly when its residue is zero.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem mem_centerAlong_iff_residue_eq_zero
    {A : Type w} [CommRing A] [Algebra K A]
    (v : FunctionFieldPrimeDivisor K F) (ι : A →ₐ[K] F)
    (h : v.FiniteAlong ι) (a : A) :
    a ∈ v.centerAlong ι h ↔
      residue v.valuationSubring (v.finiteAlongRingHom ι h a) = 0

theorem

centerAlong_isPrime

L247 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.centerAlong_isPrime

Documentation

The center along any finite model map is a prime ideal.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem centerAlong_isPrime
    {A : Type w} [CommRing A] [Algebra K A]
    (v : FunctionFieldPrimeDivisor K F) (ι : A →ₐ[K] F)
    (h : v.FiniteAlong ι) :
    (v.centerAlong ι h).IsPrime

def

FiniteOn

L261 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.FiniteOn

Documentation

The prime divisor is finite on a K-model A when every function in A is contained in its valuation ring. This is FiniteAlong for the inclusion A.val : A →ₐ[K] F.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

def FiniteOn
    (v : FunctionFieldPrimeDivisor K F) (A : Subalgebra K F) : Prop

theorem

finiteOn_iff_finiteAlong_val

L266 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.finiteOn_iff_finiteAlong_val

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem finiteOn_iff_finiteAlong_val
    (v : FunctionFieldPrimeDivisor K F) (A : Subalgebra K F) :
    v.FiniteOn A ↔ v.FiniteAlong A.val

theorem

finiteOn_iff_toSubring_le

L271 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.finiteOn_iff_toSubring_le

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem finiteOn_iff_toSubring_le
    (v : FunctionFieldPrimeDivisor K F) (A : Subalgebra K F) :
    v.FiniteOn A ↔ A.toSubring ≤ v.valuationSubring.toSubring

def

finiteOnRingHom

L281 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.finiteOnRingHom

Documentation

Inclusion of a model into the valuation ring at a finite prime divisor.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

def finiteOnRingHom
    (v : FunctionFieldPrimeDivisor K F) (A : Subalgebra K F)
    (h : v.FiniteOn A) :
    A →+* v.valuationSubring

def

finiteOnAlgHom

L288 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.finiteOnAlgHom

Documentation

The finite-on inclusion respects the K-algebra structures.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

def finiteOnAlgHom
    (v : FunctionFieldPrimeDivisor K F) (A : Subalgebra K F)
    (h : v.FiniteOn A) :
  A →ₐ[K] v.valuationSubring

theorem

finiteOnRingHom_injective

L294 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.finiteOnRingHom_injective

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem finiteOnRingHom_injective
    (v : FunctionFieldPrimeDivisor K F) (A : Subalgebra K F)
    (h : v.FiniteOn A) :
    Function.Injective (v.finiteOnRingHom A h)

def

center

L306 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.center

Documentation

The center of a prime divisor on a model is the contraction of the maximal ideal of its valuation ring.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

def center
    (v : FunctionFieldPrimeDivisor K F) (A : Subalgebra K F)
    (h : v.FiniteOn A) : Ideal A

theorem

mem_center_iff

L312 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.mem_center_iff

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem mem_center_iff
    (v : FunctionFieldPrimeDivisor K F) (A : Subalgebra K F)
    (h : v.FiniteOn A) (x : A) :
    x ∈ v.center A h ↔
      v.finiteOnRingHom A h x ∈ maximalIdeal v.valuationSubring

theorem

mem_center_iff_mem_nonunits

L323 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.mem_center_iff_mem_nonunits

Documentation

Ambient-field characterization of the center: a model element is centered at v exactly when it is a nonunit of the valuation ring.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem mem_center_iff_mem_nonunits
    (v : FunctionFieldPrimeDivisor K F) (A : Subalgebra K F)
    (h : v.FiniteOn A) (x : A) :
    x ∈ v.center A h ↔ (x : F) ∈ v.valuationSubring.nonunits

theorem

mem_center_iff_residue_eq_zero

L330 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.mem_center_iff_residue_eq_zero

Documentation

A model element is in the center exactly when its residue is zero.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem mem_center_iff_residue_eq_zero
    (v : FunctionFieldPrimeDivisor K F) (A : Subalgebra K F)
    (h : v.FiniteOn A) (x : A) :
    x ∈ v.center A h ↔
      residue v.valuationSubring (v.finiteOnRingHom A h x) = 0

theorem

center_isPrime

L338 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.center_isPrime

Documentation

The center of a finite prime divisor on a model is a prime ideal.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe u v w
variable (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
namespace FunctionFieldPrimeDivisor
variable {K F}

Lean source · statement

theorem center_isPrime
    (v : FunctionFieldPrimeDivisor K F) (A : Subalgebra K F)
    (h : v.FiniteOn A) :
    (v.center A h).IsPrime

Module documentation

Prime divisors of function fields

Declarations