From b5398d91e0c2f43311c1393ce9efdef9fff5f690 Mon Sep 17 00:00:00 2001 From: Xavier Genereux Date: Fri, 10 Apr 2026 10:52:09 -0400 Subject: [PATCH 1/4] rename vars --- Mathlib/NumberTheory/FunctionField.lean | 206 ++++++++++++------------ 1 file changed, 103 insertions(+), 103 deletions(-) diff --git a/Mathlib/NumberTheory/FunctionField.lean b/Mathlib/NumberTheory/FunctionField.lean index af71fedeb637ca..b99d4c55c88dd4 100644 --- a/Mathlib/NumberTheory/FunctionField.lean +++ b/Mathlib/NumberTheory/FunctionField.lean @@ -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 (finite) 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 `Finite F` or +`IsScalarTower F[X] (FractionRing F[X]) K` in definitions, adding them back in lemmas when they are needed. ## References @@ -49,118 +49,118 @@ 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 finite 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 (Fqt : Type*) [Field Fqt] [Algebra F[X] Fqt] + [IsFractionRing F[X] Fqt] [Algebra (RatFunc F) K] [Algebra Fqt K] [Algebra F[X] K] + [IsScalarTower F[X] Fqt K] [IsScalarTower F[X] (RatFunc F) K] : + FunctionField F K ↔ FiniteDimensional Fqt K := by + let e := IsLocalization.algEquiv F[X]⁰ (RatFunc F) Fqt + 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 Fqt 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 Fqt 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 Fqt K` is the integral closure of `F[t]` 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] @@ -168,16 +168,16 @@ theorem InftyValuation.map_mul' (x y : RatFunc Fq) : · 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, @@ -185,53 +185,53 @@ theorem InftyValuation.map_add_le_max' (x y : RatFunc Fq) : 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 @@ -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) +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 From 17d95a22f32754f24e6ab4daabc96355929330e7 Mon Sep 17 00:00:00 2001 From: Xavier Genereux Date: Fri, 10 Apr 2026 10:52:28 -0400 Subject: [PATCH 2/4] adjust doc --- Mathlib/NumberTheory/FunctionField.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/NumberTheory/FunctionField.lean b/Mathlib/NumberTheory/FunctionField.lean index b99d4c55c88dd4..4711c82692d4fb 100644 --- a/Mathlib/NumberTheory/FunctionField.lean +++ b/Mathlib/NumberTheory/FunctionField.lean @@ -18,7 +18,7 @@ This file defines a function field and the ring of integers corresponding to it. ## Main definitions -- `FunctionField F K` states that `K` is a function field over the (finite) field `F`, +- `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 `F[X]` in the function field. @@ -51,7 +51,7 @@ open scoped nonZeroDivisors Polynomial WithZero variable (F K : Type*) [Field F] [Field K] -/-- `K` is a function field over the finite field `F` if it is a finite +/-- `K` is a function field over the (usually finite) field `F` if it is a finite extension of the field of rational functions in one variable over `F`. Note that `K` can be a function field over multiple, non-isomorphic, `F`. From 792ff0bccfc3d35f10f331d98834d309aef5b327 Mon Sep 17 00:00:00 2001 From: Xavier Genereux Date: Fri, 10 Apr 2026 10:59:15 -0400 Subject: [PATCH 3/4] rename Fqt to Ft --- Mathlib/NumberTheory/FunctionField.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Mathlib/NumberTheory/FunctionField.lean b/Mathlib/NumberTheory/FunctionField.lean index 4711c82692d4fb..e370d9acafee2c 100644 --- a/Mathlib/NumberTheory/FunctionField.lean +++ b/Mathlib/NumberTheory/FunctionField.lean @@ -60,22 +60,22 @@ 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 (Fqt : Type*) [Field Fqt] [Algebra F[X] Fqt] - [IsFractionRing F[X] Fqt] [Algebra (RatFunc F) K] [Algebra Fqt K] [Algebra F[X] K] - [IsScalarTower F[X] Fqt K] [IsScalarTower F[X] (RatFunc F) K] : - FunctionField F K ↔ FiniteDimensional Fqt K := by - let e := IsLocalization.algEquiv F[X]⁰ (RatFunc F) Fqt +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 K (e c)) ?_ c + 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 F) K exact (b.mapCoeffs e this).finiteDimensional_of_finite - · let b := Module.finBasis Fqt K + · 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] @@ -87,7 +87,7 @@ theorem algebraMap_injective [Algebra F[X] K] [Algebra (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 F Fqt K` is the integral closure of `F[t]` in `K`. +`FunctionField.ringOfIntegers F Ft K` is the integral closure of `F[t]` in `K`. We don't actually assume `K` is a function field over `F` in the definition, only when proving its properties. From c5d865f07b22ea4059d9ac16e170e90578cb08f7 Mon Sep 17 00:00:00 2001 From: Xavier Genereux Date: Fri, 10 Apr 2026 15:24:54 -0400 Subject: [PATCH 4/4] suggested changes --- Mathlib/NumberTheory/FunctionField.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/NumberTheory/FunctionField.lean b/Mathlib/NumberTheory/FunctionField.lean index e370d9acafee2c..703e4230930203 100644 --- a/Mathlib/NumberTheory/FunctionField.lean +++ b/Mathlib/NumberTheory/FunctionField.lean @@ -29,7 +29,7 @@ This file defines a function field and the ring of integers corresponding to it. ## 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 F` or +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. @@ -51,7 +51,7 @@ open scoped nonZeroDivisors Polynomial WithZero variable (F K : Type*) [Field F] [Field K] -/-- `K` is a function field over the (usually finite) field `F` if it is a finite +/-- `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 `K` can be a function field over multiple, non-isomorphic, `F`. @@ -87,7 +87,7 @@ theorem algebraMap_injective [Algebra F[X] K] [Algebra (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 F Ft K` is the integral closure of `F[t]` in `K`. +`FunctionField.ringOfIntegers F K` is the integral closure of `F[X]` in `K`. We don't actually assume `K` is a function field over `F` in the definition, only when proving its properties.