Skip to content

chore(FunctionField): rename vars when constant field is not nec. finite #37894

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
xgenereux wants to merge 4 commits into
base: master
Choose a base branch
from
+103 −103
Open

chore(FunctionField): rename vars when constant field is not nec. finite #37894

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
b5398d9
rename vars
xgenereux Apr 10, 2026
17d95a2
adjust doc
xgenereux Apr 10, 2026
792ff0b
rename Fqt to Ft
xgenereux Apr 10, 2026
c5d865f
suggested changes
xgenereux Apr 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
206 changes: 103 additions & 103 deletions Mathlib/NumberTheory/FunctionField.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,19 +18,19 @@ This file defines a function field and the ring of integers corresponding to it.

## Main definitions

- `FunctionField Fq F` states that `F` is a function field over the (finite) field `Fq`,
i.e. it is a finite extension of the field of rational functions in one variable over `Fq`.
- `FunctionField F K` states that `K` is a function field over the field `F`,
i.e. it is a finite extension of the field of rational functions in one variable over `F`.
- `FunctionField.ringOfIntegers` defines the ring of integers corresponding to a function field
as the integral closure of `Fq[X]` in the function field.
- `FunctionField.inftyValuation` : The place at infinity on `Fq(t)` is the nonarchimedean
valuation on `Fq(t)` with uniformizer `1/t`.
- `FunctionField.FqtInfty` : The completion `Fq((t⁻¹))` of `Fq(t)` with respect to the
as the integral closure of `F[X]` in the function field.
- `FunctionField.inftyValuation` : The place at infinity on `F(t)` is the nonarchimedean
valuation on `F(t)` with uniformizer `1/t`.
- `FunctionField.FqtInfty` : The completion `F((t⁻¹))` of `F(t)` with respect to the
valuation at infinity.

## Implementation notes
The definitions that involve a field of fractions choose a canonical field of fractions,
but are independent of that choice. We also omit assumptions like `Finite Fq` or
`IsScalarTower Fq[X] (FractionRing Fq[X]) F` in definitions,
but are independent of that choice. We also omit assumptions like
`IsScalarTower F[X] (FractionRing F[X]) K` in definitions,
adding them back in lemmas when they are needed.

## References
Expand All @@ -49,189 +49,189 @@ noncomputable section

open scoped nonZeroDivisors Polynomial WithZero

variable (Fq F : Type*) [Field Fq] [Field F]
variable (F K : Type*) [Field F] [Field K]

/-- `F` is a function field over the finite field `Fq` if it is a finite
extension of the field of rational functions in one variable over `Fq`.
/-- `K` is a function field over the field `F` if it is a finite
extension of the field of rational functions in one variable over `F`.

Note that `F` can be a function field over multiple, non-isomorphic, `Fq`.
Note that `K` can be a function field over multiple, non-isomorphic, `F`.
-/
abbrev FunctionField [Algebra (RatFunc Fq) F] : Prop :=
FiniteDimensional (RatFunc Fq) F

/-- `F` is a function field over `Fq` iff it is a finite extension of `Fq(t)`. -/
theorem functionField_iff (Fqt : Type*) [Field Fqt] [Algebra Fq[X] Fqt]
[IsFractionRing Fq[X] Fqt] [Algebra (RatFunc Fq) F] [Algebra Fqt F] [Algebra Fq[X] F]
[IsScalarTower Fq[X] Fqt F] [IsScalarTower Fq[X] (RatFunc Fq) F] :
FunctionField Fq F ↔ FiniteDimensional Fqt F := by
let e := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
have : ∀ (c) (x : F), e c • x = c • x := by
abbrev FunctionField [Algebra (RatFunc F) K] : Prop :=
FiniteDimensional (RatFunc F) K

/-- `K` is a function field over `F` iff it is a finite extension of `F(t)`. -/
theorem functionField_iff (Ft : Type*) [Field Ft] [Algebra F[X] Ft]
[IsFractionRing F[X] Ft] [Algebra (RatFunc F) K] [Algebra Ft K] [Algebra F[X] K]
[IsScalarTower F[X] Ft K] [IsScalarTower F[X] (RatFunc F) K] :
FunctionField F K ↔ FiniteDimensional Ft K := by
let e := IsLocalization.algEquiv F[X]⁰ (RatFunc F) Ft
have : ∀ (c) (x : K), e c • x = c • x := by
intro c x
rw [Algebra.smul_def, Algebra.smul_def]
congr
refine congr_fun (f := fun c => algebraMap Fqt F (e c)) ?_ c
refine IsLocalization.ext (nonZeroDivisors Fq[X]) _ _ ?_ ?_ ?_ ?_ ?_ <;> intros <;>
refine congr_fun (f := fun c => algebraMap Ft K (e c)) ?_ c
refine IsLocalization.ext (nonZeroDivisors F[X]) _ _ ?_ ?_ ?_ ?_ ?_ <;> intros <;>
simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
constructor <;> intro h
· let b := Module.finBasis (RatFunc Fq) F
· let b := Module.finBasis (RatFunc F) K
exact (b.mapCoeffs e this).finiteDimensional_of_finite
· let b := Module.finBasis Fqt F
· let b := Module.finBasis Ft K
refine (b.mapCoeffs e.symm ?_).finiteDimensional_of_finite
intro c x; convert (this (e.symm c) x).symm; simp only [e.apply_symm_apply]

namespace FunctionField

theorem algebraMap_injective [Algebra Fq[X] F] [Algebra (RatFunc Fq) F]
[IsScalarTower Fq[X] (RatFunc Fq) F] : Function.Injective (⇑(algebraMap Fq[X] F)) := by
rw [IsScalarTower.algebraMap_eq Fq[X] (RatFunc Fq) F]
exact (algebraMap (RatFunc Fq) F).injective.comp (IsFractionRing.injective Fq[X] (RatFunc Fq))
theorem algebraMap_injective [Algebra F[X] K] [Algebra (RatFunc F) K]
[IsScalarTower F[X] (RatFunc F) K] : Function.Injective (⇑(algebraMap F[X] K)) := by
rw [IsScalarTower.algebraMap_eq F[X] (RatFunc F) K]
exact (algebraMap (RatFunc F) K).injective.comp (IsFractionRing.injective F[X] (RatFunc F))

/-- The function field analogue of `NumberField.ringOfIntegers`:
`FunctionField.ringOfIntegers Fq Fqt F` is the integral closure of `Fq[t]` in `F`.
`FunctionField.ringOfIntegers F K` is the integral closure of `F[X]` in `K`.

We don't actually assume `F` is a function field over `Fq` in the definition,
We don't actually assume `K` is a function field over `F` in the definition,
only when proving its properties.
-/
def ringOfIntegers [Algebra Fq[X] F] :=
integralClosure Fq[X] F
def ringOfIntegers [Algebra F[X] K] :=
integralClosure F[X] K

namespace ringOfIntegers

variable [Algebra Fq[X] F]
variable [Algebra F[X] K]

instance : IsDomain (ringOfIntegers Fq F) :=
(ringOfIntegers Fq F).isDomain
instance : IsDomain (ringOfIntegers F K) :=
(ringOfIntegers F K).isDomain

instance : IsIntegralClosure (ringOfIntegers Fq F) Fq[X] F :=
instance : IsIntegralClosure (ringOfIntegers F K) F[X] K :=
integralClosure.isIntegralClosure _ _

variable [Algebra (RatFunc Fq) F] [IsScalarTower Fq[X] (RatFunc Fq) F]
variable [Algebra (RatFunc F) K] [IsScalarTower F[X] (RatFunc F) K]

theorem algebraMap_injective : Function.Injective (⇑(algebraMap Fq[X] (ringOfIntegers Fq F))) := by
have hinj : Function.Injective (⇑(algebraMap Fq[X] F)) := by
rw [IsScalarTower.algebraMap_eq Fq[X] (RatFunc Fq) F]
exact (algebraMap (RatFunc Fq) F).injective.comp (IsFractionRing.injective Fq[X] (RatFunc Fq))
rw [injective_iff_map_eq_zero (algebraMap Fq[X] (↥(ringOfIntegers Fq F)))]
theorem algebraMap_injective : Function.Injective (⇑(algebraMap F[X] (ringOfIntegers F K))) := by
have hinj : Function.Injective (⇑(algebraMap F[X] K)) := by
rw [IsScalarTower.algebraMap_eq F[X] (RatFunc F) K]
exact (algebraMap (RatFunc F) K).injective.comp (IsFractionRing.injective F[X] (RatFunc F))
rw [injective_iff_map_eq_zero (algebraMap F[X] (↥(ringOfIntegers F K)))]
intro p hp
rw [← Subtype.coe_inj, Subalgebra.coe_zero] at hp
rw [injective_iff_map_eq_zero (algebraMap Fq[X] F)] at hinj
rw [injective_iff_map_eq_zero (algebraMap F[X] K)] at hinj
exact hinj p hp

theorem not_isField : ¬IsField (ringOfIntegers Fq F) := by
simpa [← (IsIntegralClosure.isIntegral_algebra Fq[X] F).isField_iff_isField
(algebraMap_injective Fq F)] using
Polynomial.not_isField Fq
theorem not_isField : ¬IsField (ringOfIntegers F K) := by
simpa [← (IsIntegralClosure.isIntegral_algebra F[X] K).isField_iff_isField
(algebraMap_injective F K)] using
Polynomial.not_isField F

variable [FunctionField Fq F]
variable [FunctionField F K]

instance : IsFractionRing (ringOfIntegers Fq F) F :=
integralClosure.isFractionRing_of_finite_extension (RatFunc Fq) F
instance : IsFractionRing (ringOfIntegers F K) K :=
integralClosure.isFractionRing_of_finite_extension (RatFunc F) K

instance : IsIntegrallyClosed (ringOfIntegers Fq F) :=
integralClosure.isIntegrallyClosedOfFiniteExtension (RatFunc Fq)
instance : IsIntegrallyClosed (ringOfIntegers F K) :=
integralClosure.isIntegrallyClosedOfFiniteExtension (RatFunc F)

instance [Algebra.IsSeparable (RatFunc Fq) F] : IsNoetherian Fq[X] (ringOfIntegers Fq F) :=
IsIntegralClosure.isNoetherian _ (RatFunc Fq) F _
instance [Algebra.IsSeparable (RatFunc F) K] : IsNoetherian F[X] (ringOfIntegers F K) :=
IsIntegralClosure.isNoetherian _ (RatFunc F) K _

instance [Algebra.IsSeparable (RatFunc Fq) F] : IsDedekindDomain (ringOfIntegers Fq F) :=
IsIntegralClosure.isDedekindDomain Fq[X] (RatFunc Fq) F _
instance [Algebra.IsSeparable (RatFunc F) K] : IsDedekindDomain (ringOfIntegers F K) :=
IsIntegralClosure.isDedekindDomain F[X] (RatFunc F) K _

end ringOfIntegers

/-! ### The place at infinity on Fq(t) -/
/-! ### The place at infinity on F(t) -/


section InftyValuation

open Multiplicative WithZero

variable [DecidableEq (RatFunc Fq)]
variable [DecidableEq (RatFunc F)]

/-- The valuation at infinity is the nonarchimedean valuation on `Fq(t)` with uniformizer `1/t`.
Explicitly, if `f/g ∈ Fq(t)` is a nonzero quotient of polynomials, its valuation at infinity is
/-- The valuation at infinity is the nonarchimedean valuation on `F(t)` with uniformizer `1/t`.
Explicitly, if `f/g ∈ F(t)` is a nonzero quotient of polynomials, its valuation at infinity is
`exp (degree(f) - degree(g))`. -/
def inftyValuationDef (r : RatFunc Fq) : ℤᵐ⁰ :=
def inftyValuationDef (r : RatFunc F) : ℤᵐ⁰ :=
if r = 0 then 0 else exp r.intDegree

theorem InftyValuation.map_zero' : inftyValuationDef Fq 0 = 0 :=
theorem InftyValuation.map_zero' : inftyValuationDef F 0 = 0 :=
if_pos rfl

theorem InftyValuation.map_one' : inftyValuationDef Fq 1 = 1 :=
theorem InftyValuation.map_one' : inftyValuationDef F 1 = 1 :=
(if_neg one_ne_zero).trans <| by simp

theorem InftyValuation.map_mul' (x y : RatFunc Fq) :
inftyValuationDef Fq (x * y) = inftyValuationDef Fq x * inftyValuationDef Fq y := by
theorem InftyValuation.map_mul' (x y : RatFunc F) :
inftyValuationDef F (x * y) = inftyValuationDef F x * inftyValuationDef F y := by
rw [inftyValuationDef, inftyValuationDef, inftyValuationDef]
by_cases hx : x = 0
· rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]
· by_cases hy : y = 0
· rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]
· simp_all [RatFunc.intDegree_mul]

theorem InftyValuation.map_add_le_max' (x y : RatFunc Fq) :
inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y) := by
theorem InftyValuation.map_add_le_max' (x y : RatFunc F) :
inftyValuationDef F (x + y) ≤ max (inftyValuationDef F x) (inftyValuationDef F y) := by
by_cases hx : x = 0
· rw [hx, zero_add]
conv_rhs => rw [inftyValuationDef, if_pos (Eq.refl _)]
rw [max_eq_right (WithZero.zero_le (inftyValuationDef Fq y))]
rw [max_eq_right (WithZero.zero_le (inftyValuationDef F y))]
· by_cases hy : y = 0
· rw [hy, add_zero]
conv_rhs => rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
rw [max_eq_right (WithZero.zero_le (inftyValuationDef Fq x))]
rw [max_eq_right (WithZero.zero_le (inftyValuationDef F x))]
· by_cases hxy : x + y = 0
· rw [inftyValuationDef, if_pos hxy]; exact zero_le'
· rw [inftyValuationDef, inftyValuationDef, inftyValuationDef, if_neg hx, if_neg hy,
if_neg hxy]
simpa using RatFunc.intDegree_add_le hy hxy

@[simp]
theorem inftyValuation_of_nonzero {x : RatFunc Fq} (hx : x ≠ 0) :
inftyValuationDef Fq x = exp x.intDegree := by
theorem inftyValuation_of_nonzero {x : RatFunc F} (hx : x ≠ 0) :
inftyValuationDef F x = exp x.intDegree := by
rw [inftyValuationDef, if_neg hx]

/-- The valuation at infinity on `Fq(t)`. -/
def inftyValuation : Valuation (RatFunc Fq) ℤᵐ⁰ where
toFun := inftyValuationDef Fq
map_zero' := InftyValuation.map_zero' Fq
map_one' := InftyValuation.map_one' Fq
map_mul' := InftyValuation.map_mul' Fq
map_add_le_max' := InftyValuation.map_add_le_max' Fq
/-- The valuation at infinity on `F(t)`. -/
def inftyValuation : Valuation (RatFunc F) ℤᵐ⁰ where
toFun := inftyValuationDef F
map_zero' := InftyValuation.map_zero' F
map_one' := InftyValuation.map_one' F
map_mul' := InftyValuation.map_mul' F
map_add_le_max' := InftyValuation.map_add_le_max' F

theorem inftyValuation_apply {x : RatFunc Fq} : inftyValuation Fq x = inftyValuationDef Fq x :=
theorem inftyValuation_apply {x : RatFunc F} : inftyValuation F x = inftyValuationDef F x :=
rfl

@[simp]
theorem inftyValuation.C {k : Fq} (hk : k ≠ 0) :
inftyValuation Fq (RatFunc.C k) = 1 := by
theorem inftyValuation.C {k : F} (hk : k ≠ 0) :
inftyValuation F (RatFunc.C k) = 1 := by
simp [inftyValuation_apply, hk]

@[simp]
theorem inftyValuation.X : inftyValuation Fq RatFunc.X = exp 1 := by
theorem inftyValuation.X : inftyValuation F RatFunc.X = exp 1 := by
simp [inftyValuation_apply, inftyValuationDef, if_neg RatFunc.X_ne_zero, RatFunc.intDegree_X]

lemma inftyValuation.X_zpow (m : ℤ) : inftyValuation Fq (RatFunc.X ^ m) = exp m := by simp
lemma inftyValuation.X_zpow (m : ℤ) : inftyValuation F (RatFunc.X ^ m) = exp m := by simp

theorem inftyValuation.X_inv : inftyValuation Fq (1 / RatFunc.X) = exp (-1) := by
theorem inftyValuation.X_inv : inftyValuation F (1 / RatFunc.X) = exp (-1) := by
rw [one_div, ← zpow_neg_one, inftyValuation.X_zpow]

-- Dropped attribute `@[simp]` due to issue described here:
-- https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60synthInstance.2EmaxHeartbeats.60.20error.20but.20only.20in.20.60simpNF.60
theorem inftyValuation.polynomial {p : Fq[X]} (hp : p ≠ 0) :
inftyValuationDef Fq (algebraMap Fq[X] (RatFunc Fq) p) = exp (p.natDegree : ℤ) := by
theorem inftyValuation.polynomial {p : F[X]} (hp : p ≠ 0) :
inftyValuationDef F (algebraMap F[X] (RatFunc F) p) = exp (p.natDegree : ℤ) := by
rw [inftyValuationDef, if_neg (by simpa), RatFunc.intDegree_polynomial]

instance : Valuation.IsNontrivial (inftyValuation Fq) := ⟨RatFunc.X, by simp⟩
instance : Valuation.IsNontrivial (inftyValuation F) := ⟨RatFunc.X, by simp⟩

instance : Valuation.IsTrivialOn Fq (inftyValuation Fq) :=
instance : Valuation.IsTrivialOn F (inftyValuation F) :=
⟨fun _ hx ↦ by simp [inftyValuation.C _ hx]⟩

/-- The valued field `Fq(t)` with the valuation at infinity. -/
/-- The valued field `F(t)` with the valuation at infinity. -/
@[implicit_reducible]
def inftyValuedFqt : Valued (RatFunc Fq) ℤᵐ⁰ :=
Valued.mk' <| inftyValuation Fq
def inftyValuedFqt : Valued (RatFunc F) ℤᵐ⁰ :=
Valued.mk' <| inftyValuation F

theorem inftyValuedFqt.def {x : RatFunc Fq} :
(inftyValuedFqt Fq).v x = inftyValuationDef Fq x :=
theorem inftyValuedFqt.def {x : RatFunc F} :
(inftyValuedFqt F).v x = inftyValuationDef F x :=
rfl

namespace FqtInfty
Expand All @@ -242,20 +242,20 @@ attribute [-instance] RatFunc.valuedRatFunc

/- Locally add the uniform space structure coming from the valuation at infinity. This instance
is scoped in the `FqtInfty` namescape in case it is needed in the future. -/
/-- The uniform space structure on `RatFunc Fq` coming from the valuation at infinity. -/
scoped instance : UniformSpace (RatFunc Fq) := (inftyValuedFqt Fq).toUniformSpace
/-- The uniform space structure on `RatFunc F` coming from the valuation at infinity. -/
scoped instance : UniformSpace (RatFunc F) := (inftyValuedFqt F).toUniformSpace

/-- The completion `Fq((t⁻¹))` of `Fq(t)` with respect to the valuation at infinity. -/
def _root_.FunctionField.FqtInfty := UniformSpace.Completion (RatFunc Fq)
deriving Field, Algebra (RatFunc Fq), Coe (RatFunc Fq), Inhabited
/-- The completion `F((t⁻¹))` of `F(t)` with respect to the valuation at infinity. -/
def _root_.FunctionField.FqtInfty := UniformSpace.Completion (RatFunc F)
Copy link
Copy Markdown
Contributor

@MichaelStollBayreuth MichaelStollBayreuth Apr 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similarly here. InftyCompletionRatFunc?

Copy link
Copy Markdown
Collaborator Author

@xgenereux xgenereux Apr 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But then this shouldn't be in this file right? I feel like the InftyValuation should be in the RatFunc folder no?

Copy link
Copy Markdown
Contributor

@MichaelStollBayreuth MichaelStollBayreuth Apr 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess so. (And at some point, it would make sense to move the current content of this file out of NumberTheory into FieldTheory. I think this place should be for material that is specifically about function fields over finite fields. But don't feel obliged to do that now, too!)

Copy link
Copy Markdown
Collaborator Author

@xgenereux xgenereux Apr 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would you like me to do this move in this PR or in another?
I am asking because all of these lemmas will have to change name (out of the FunctionField namespace) and will need to be deprecated.

deriving Field, Algebra (RatFunc F), Coe (RatFunc F), Inhabited

end FqtInfty

/-- The valuation at infinity on `k(t)` extends to a valuation on `FqtInfty`. -/
instance valuedFqtInfty : Valued (FqtInfty Fq) ℤᵐ⁰ := (inftyValuedFqt Fq).valuedCompletion
instance valuedFqtInfty : Valued (FqtInfty F) ℤᵐ⁰ := (inftyValuedFqt F).valuedCompletion

theorem valuedFqtInfty.def {x : FqtInfty Fq} :
Valued.v x = (inftyValuedFqt Fq).extensionValuation x := rfl
theorem valuedFqtInfty.def {x : FqtInfty F} :
Valued.v x = (inftyValuedFqt F).extensionValuation x := rfl

end InftyValuation

Expand Down
Loading