From 5dc2ffdddd23b51c4f5c3c602b63976000198606 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Mon, 11 May 2026 00:49:54 +0200
Subject: [PATCH 1/9] feat(AlgebraicGeometry): function fields and Faltings'
 theorem

---
 LeanEval/AlgebraicGeometry/FunctionField.lean | 146 ++++++++++++++++++
 manifests/problems.toml                       |  40 +++++
 2 files changed, 186 insertions(+)
 create mode 100644 LeanEval/AlgebraicGeometry/FunctionField.lean

diff --git a/LeanEval/AlgebraicGeometry/FunctionField.lean b/LeanEval/AlgebraicGeometry/FunctionField.lean
new file mode 100644
index 0000000..1d96bb4
--- /dev/null
+++ b/LeanEval/AlgebraicGeometry/FunctionField.lean
@@ -0,0 +1,146 @@
+import Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
+import Mathlib.NumberTheory.NumberField.Basic
+import Mathlib.RingTheory.AlgebraicIndependent.Basic
+import Mathlib.RingTheory.DiscreteValuationRing.Basic
+import Mathlib.RingTheory.Valuation.ValuationSubring
+import Mathlib.Topology.Algebra.RestrictedProduct.Basic
+import EvalTools.Markers
+
+/-!
+# Function fields of one variable
+
+This file develops the basic theory of function fields of one variable following [Stichtenoth], with
+several sorries left as LeanEval problems, and ends with a very hard sorry (Faltings' theorem).
+
+[Stichtenoth] Henning Stichtenoth, *Algebraic Function Fields and Codes*, Second Edition.
+-/
+
+section ValuationSubalgebra
+
+variable (R F : Type*) [CommSemiring R] [Field F] [Algebra R F]
+
+@[ext] structure ValuationSubalgebra extends Subalgebra R F, ValuationSubring F
+
+end ValuationSubalgebra
+
+variable (K F: Type*) [Field K] [Field F] [Algebra K F]
+
+namespace Algebra
+
+class Is1DFunctionField : Prop where
+  trdeg_eq_one : trdeg K F = 1
+  fg : (⊤ : IntermediateField K F).FG
+
+open scoped IntermediateField
+
+@[eval_problem]
+theorem Is1DFunctionField.finiteDimensional_of_transcendental [Is1DFunctionField K F]
+    (x : F) (hx : Transcendental K x) : FiniteDimensional K⟮x⟯ F := by
+  sorry
+
+variable {K F} in
+/-- The definition `Is1DFunctionField` is equivalent to [Stichtenoth, Definition 1.1.1]. -/
+@[eval_problem]
+theorem is1DFunctionField_iff_exists_transcendental_finiteDimensional :
+    Is1DFunctionField K F ↔ ∃ x : F, Transcendental K x ∧ FiniteDimensional K⟮x⟯ F := by
+  sorry
+
+namespace Is1DFunctionField
+
+/-- The type of places of a 1-dimensional function field. See [Stichtenoth,
+Definition 1.1.4 and 1.1.8]. We omit the condition `toSubalgebra ≠ ⊥` since it is automatic. -/
+@[ext] structure Place extends ValuationSubalgebra K F where
+  ne_top : toSubalgebra ≠ ⊤
+
+instance : SetLike (Place K F) F where
+  coe v := v.carrier
+  coe_injective' _ _ := Place.ext
+
+instance : SMulMemClass (Place K F) K F where
+  smul_mem {v} r _ h := v.smul_mem h r
+
+instance : SubringClass (Place K F) F where
+  mul_mem {v} := v.mul_mem
+  one_mem {v} := v.one_mem
+  add_mem {v} := v.add_mem
+  zero_mem {v} := v.zero_mem
+  neg_mem {v} := v.toValuationSubring.neg_mem _
+
+variable (v : Place K F)
+
+instance : HasMemOrInvMem v where
+  mem_or_inv_mem := v.mem_or_inv_mem'
+
+instance : Algebra v F := inferInstanceAs (Algebra v.toSubalgebra F)
+instance : IsScalarTower K v F := inferInstanceAs (IsScalarTower K v.toSubalgebra F)
+instance : IsFractionRing v F := inferInstanceAs (IsFractionRing v.toValuationSubring F)
+instance : ValuationRing v := inferInstanceAs (ValuationRing v.toValuationSubring)
+
+variable {K F} in
+/-- [Stichtenoth, Theorem 1.1.6]. -/
+@[eval_problem]
+instance Place.isDiscreteValuationRing [Is1DFunctionField K F] : IsDiscreteValuationRing v := by
+  sorry
+
+variable {F} in
+/-- [Stichtenoth, Corollary 1.3.4] (finitely many poles). -/
+@[eval_problem]
+theorem Place.finite_setOf_notMem [Is1DFunctionField K F] (x : F) :
+    Finite {v : Place K F | x ∉ v} := by
+  sorry
+
+open scoped RestrictedProduct
+
+/-- [Stichtenoth, Definition 1.5.2]. -/
+abbrev Adele : Type _ := Πʳ v : Place K F, [F, v]
+
+variable {F} in
+/-- The principal adele associated to an element in the function field. -/
+def Adele.principal [Is1DFunctionField K F] : F →+* Adele K F where
+  toFun x := ⟨fun _ ↦ x, Place.finite_setOf_notMem K x⟩
+  map_one' := rfl
+  map_mul' _ _ := rfl
+  map_zero' := rfl
+  map_add' _ _ := rfl
+
+instance [Is1DFunctionField K F] : Algebra F (Adele K F) where
+  smul x a := ⟨x • a, (.principal K x * a).2⟩
+  algebraMap := Adele.principal K
+  commutes' _ _ := mul_comm ..
+  smul_def' _ _ := rfl
+
+-- TODO: generalize this to RestrictedProduct
+instance : Algebra K (Adele K F) where
+  __ : Module K _ := inferInstance
+  algebraMap.toFun x := ⟨fun _ ↦ algebraMap K F x, .of_forall fun _ ↦ algebraMap_mem ..⟩
+  algebraMap.map_one' := by ext; exact (algebraMap K F).map_one
+  algebraMap.map_mul' _ _ := by ext; exact (algebraMap K F).map_mul ..
+  algebraMap.map_add' _ _ := by ext; exact (algebraMap K F).map_add ..
+  algebraMap.map_zero' := by ext; exact (algebraMap K F).map_zero
+  commutes' _ _ := mul_comm ..
+  smul_def' _ _ := by ext; apply smul_def
+
+instance [Is1DFunctionField K F] : IsScalarTower K F (Adele K F) :=
+  .of_algebraMap_eq fun _ ↦ rfl
+
+/-- The $K$-subspace $\mathcal{A}_F(0)$, see [Stichtenoth, Definition 1.5.3]. -/
+def integralAdele : Submodule K (Adele K F) where
+  carrier := {x | ∀ v, x v ∈ v}
+  add_mem' h₁ h₂ v := add_mem (h₁ v) (h₂ v)
+  zero_mem' _ := zero_mem _
+  smul_mem' _ _ h v := v.smul_mem (h v) _
+
+/-- The genus of a function field, [Stichtenoth, Corollary 1.5.5]. -/
+noncomputable def genus [Is1DFunctionField K F] : ℕ := Module.finrank K
+  (Adele K F ⧸ integralAdele K F ⊔ (IsScalarTower.toAlgHom K F _).toLinearMap.range)
+
+/-- Every function field of genus at least 2 (equivalently, every curve of geometric genus at least 2)
+over a number field has only finitely many rational points. -/
+@[eval_problem]
+theorem faltings [NumberField K] [Is1DFunctionField K F] (h : 2 ≤ genus K F) :
+    Finite {v : Place K F | Module.rank K (IsLocalRing.ResidueField v) = 1} := by
+  sorry
+
+end Is1DFunctionField
+
+end Algebra
diff --git a/manifests/problems.toml b/manifests/problems.toml
index d0d66c4..eee5737 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -645,3 +645,43 @@ module = "LeanEval.NumberTheory.NeukirchUchida"
 holes = ["neukirch_uchida"]
 submitter = "Junyan Xu"
 source = "Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Number Fields*, Theorem 12.2.1."
+
+[[problem]]
+id = "Is1DFunctionField.finiteDimensional_of_transcendental"
+title = "A function field is finite-dimensional over any transcendental subfield"
+test = false
+module = "LeanEval.AlgebraicGeometry.FunctionField"
+holes = ["Is1DFunctionField.finiteDimensional_of_transcendental"] 
+submitter = "Junyan Xu"
+
+[[problem]]
+id = "is1DFunctionField_iff_exists_transcendental_finiteDimensional"
+title = "A characterization of function fields of one variable"
+test = false
+module = "LeanEval.AlgebraicGeometry.FunctionField"
+holes = ["is1DFunctionField_iff_exists_transcendental_finiteDimensional"]
+submitter = "Junyan Xu"
+
+[[problem]]
+id = "Place.isDiscreteValuationRing"
+title = "Places of function fields are discrete valuation rings"
+test = false
+module = "LeanEval.AlgebraicGeometry.FunctionField"
+holes = ["Place.isDiscreteValuationRing"]
+submitter = "Junyan Xu"
+
+[[problem]]
+id = "Place.finite_setOf_notMem"
+title = "Elements in function fields have finitely many poles"
+test = false
+module = "LeanEval.AlgebraicGeometry.FunctionField"
+holes = ["Place.finite_setOf_notMem"]
+submitter = "Junyan Xu"
+
+[[problem]]
+id = "faltings"
+title = "Faltings' theorem (Mordell conjecture)"
+test = false
+module = "LeanEval.AlgebraicGeometry.FunctionField"
+holes = ["faltings"]
+submitter = "Junyan Xu"

From e1c4f5b668ab45a70709068a8c4b11c1a43cc099 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Mon, 11 May 2026 01:22:52 +0200
Subject: [PATCH 2/9] add a comment

---
 LeanEval/AlgebraicGeometry/FunctionField.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/LeanEval/AlgebraicGeometry/FunctionField.lean b/LeanEval/AlgebraicGeometry/FunctionField.lean
index 1d96bb4..13f99a6 100644
--- a/LeanEval/AlgebraicGeometry/FunctionField.lean
+++ b/LeanEval/AlgebraicGeometry/FunctionField.lean
@@ -135,7 +135,9 @@ noncomputable def genus [Is1DFunctionField K F] : ℕ := Module.finrank K
   (Adele K F ⧸ integralAdele K F ⊔ (IsScalarTower.toAlgHom K F _).toLinearMap.range)
 
 /-- Every function field of genus at least 2 (equivalently, every curve of geometric genus at least 2)
-over a number field has only finitely many rational points. -/
+over a number field has only finitely many rational points.
+Note: if K is not the full constant field of F/K then there are no rational points, because every place
+contains the full constant field. -/
 @[eval_problem]
 theorem faltings [NumberField K] [Is1DFunctionField K F] (h : 2 ≤ genus K F) :
     Finite {v : Place K F | Module.rank K (IsLocalRing.ResidueField v) = 1} := by

From a97a98ba42150a41a6970b9be4086507a1c499e8 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Mon, 11 May 2026 01:33:49 +0200
Subject: [PATCH 3/9] fix eval_problem namespaces

---
 LeanEval/AlgebraicGeometry/FunctionField.lean | 8 ++++----
 manifests/problems.toml                       | 6 +++---
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/LeanEval/AlgebraicGeometry/FunctionField.lean b/LeanEval/AlgebraicGeometry/FunctionField.lean
index 13f99a6..b7f7eb7 100644
--- a/LeanEval/AlgebraicGeometry/FunctionField.lean
+++ b/LeanEval/AlgebraicGeometry/FunctionField.lean
@@ -134,10 +134,10 @@ def integralAdele : Submodule K (Adele K F) where
 noncomputable def genus [Is1DFunctionField K F] : ℕ := Module.finrank K
   (Adele K F ⧸ integralAdele K F ⊔ (IsScalarTower.toAlgHom K F _).toLinearMap.range)
 
-/-- Every function field of genus at least 2 (equivalently, every curve of geometric genus at least 2)
-over a number field has only finitely many rational points.
-Note: if K is not the full constant field of F/K then there are no rational points, because every place
-contains the full constant field. -/
+/-- Every function field of genus at least 2 (equivalently, every curve of geometric genus
+at least 2) over a number field has only finitely many rational points.
+Note: if K is not the full constant field of F/K then there are no rational points, because
+every place contains the full constant field. -/
 @[eval_problem]
 theorem faltings [NumberField K] [Is1DFunctionField K F] (h : 2 ≤ genus K F) :
     Finite {v : Place K F | Module.rank K (IsLocalRing.ResidueField v) = 1} := by
diff --git a/manifests/problems.toml b/manifests/problems.toml
index eee5737..4e4cda2 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -651,7 +651,7 @@ id = "Is1DFunctionField.finiteDimensional_of_transcendental"
 title = "A function field is finite-dimensional over any transcendental subfield"
 test = false
 module = "LeanEval.AlgebraicGeometry.FunctionField"
-holes = ["Is1DFunctionField.finiteDimensional_of_transcendental"] 
+holes = ["Algebra.Is1DFunctionField.finiteDimensional_of_transcendental"] 
 submitter = "Junyan Xu"
 
 [[problem]]
@@ -667,7 +667,7 @@ id = "Place.isDiscreteValuationRing"
 title = "Places of function fields are discrete valuation rings"
 test = false
 module = "LeanEval.AlgebraicGeometry.FunctionField"
-holes = ["Place.isDiscreteValuationRing"]
+holes = ["Algebra.Is1DFunctionField.Place.isDiscreteValuationRing"]
 submitter = "Junyan Xu"
 
 [[problem]]
@@ -675,7 +675,7 @@ id = "Place.finite_setOf_notMem"
 title = "Elements in function fields have finitely many poles"
 test = false
 module = "LeanEval.AlgebraicGeometry.FunctionField"
-holes = ["Place.finite_setOf_notMem"]
+holes = ["Algebra.Is1DFunctionField.Place.finite_setOf_notMem"]
 submitter = "Junyan Xu"
 
 [[problem]]

From 9ba34ca34a0eae83e0e4b505db456a8a2ea26768 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Mon, 11 May 2026 10:44:53 +0200
Subject: [PATCH 4/9] replace . by _

---
 manifests/problems.toml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/manifests/problems.toml b/manifests/problems.toml
index 4e4cda2..050f0ad 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -647,7 +647,7 @@ submitter = "Junyan Xu"
 source = "Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Number Fields*, Theorem 12.2.1."
 
 [[problem]]
-id = "Is1DFunctionField.finiteDimensional_of_transcendental"
+id = "Is1DFunctionField_finiteDimensional_of_transcendental"
 title = "A function field is finite-dimensional over any transcendental subfield"
 test = false
 module = "LeanEval.AlgebraicGeometry.FunctionField"
@@ -663,7 +663,7 @@ holes = ["is1DFunctionField_iff_exists_transcendental_finiteDimensional"]
 submitter = "Junyan Xu"
 
 [[problem]]
-id = "Place.isDiscreteValuationRing"
+id = "Place_isDiscreteValuationRing"
 title = "Places of function fields are discrete valuation rings"
 test = false
 module = "LeanEval.AlgebraicGeometry.FunctionField"
@@ -671,7 +671,7 @@ holes = ["Algebra.Is1DFunctionField.Place.isDiscreteValuationRing"]
 submitter = "Junyan Xu"
 
 [[problem]]
-id = "Place.finite_setOf_notMem"
+id = "Place_finite_setOf_notMem"
 title = "Elements in function fields have finitely many poles"
 test = false
 module = "LeanEval.AlgebraicGeometry.FunctionField"

From 7654ab332c6eac425769c72ffc792b7ada276ce0 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Mon, 11 May 2026 11:29:50 +0200
Subject: [PATCH 5/9] try fix

---
 LeanEval/AlgebraicGeometry/FunctionField.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/LeanEval/AlgebraicGeometry/FunctionField.lean b/LeanEval/AlgebraicGeometry/FunctionField.lean
index b7f7eb7..c24f00d 100644
--- a/LeanEval/AlgebraicGeometry/FunctionField.lean
+++ b/LeanEval/AlgebraicGeometry/FunctionField.lean
@@ -33,11 +33,6 @@ class Is1DFunctionField : Prop where
 
 open scoped IntermediateField
 
-@[eval_problem]
-theorem Is1DFunctionField.finiteDimensional_of_transcendental [Is1DFunctionField K F]
-    (x : F) (hx : Transcendental K x) : FiniteDimensional K⟮x⟯ F := by
-  sorry
-
 variable {K F} in
 /-- The definition `Is1DFunctionField` is equivalent to [Stichtenoth, Definition 1.1.1]. -/
 @[eval_problem]
@@ -47,6 +42,11 @@ theorem is1DFunctionField_iff_exists_transcendental_finiteDimensional :
 
 namespace Is1DFunctionField
 
+@[eval_problem]
+theorem finiteDimensional_of_transcendental [Is1DFunctionField K F]
+    (x : F) (hx : Transcendental K x) : FiniteDimensional K⟮x⟯ F := by
+  sorry
+
 /-- The type of places of a 1-dimensional function field. See [Stichtenoth,
 Definition 1.1.4 and 1.1.8]. We omit the condition `toSubalgebra ≠ ⊥` since it is automatic. -/
 @[ext] structure Place extends ValuationSubalgebra K F where

From 884f16056ab9ce6ab4d7da88a1528f5405e0acb8 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Mon, 11 May 2026 13:45:41 +0200
Subject: [PATCH 6/9] try fixes

---
 LeanEval/AlgebraicGeometry/FunctionField.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/LeanEval/AlgebraicGeometry/FunctionField.lean b/LeanEval/AlgebraicGeometry/FunctionField.lean
index c24f00d..d5bef2f 100644
--- a/LeanEval/AlgebraicGeometry/FunctionField.lean
+++ b/LeanEval/AlgebraicGeometry/FunctionField.lean
@@ -76,19 +76,23 @@ instance : IsScalarTower K v F := inferInstanceAs (IsScalarTower K v.toSubalgebr
 instance : IsFractionRing v F := inferInstanceAs (IsFractionRing v.toValuationSubring F)
 instance : ValuationRing v := inferInstanceAs (ValuationRing v.toValuationSubring)
 
+namespace Place
+
 variable {K F} in
 /-- [Stichtenoth, Theorem 1.1.6]. -/
 @[eval_problem]
-instance Place.isDiscreteValuationRing [Is1DFunctionField K F] : IsDiscreteValuationRing v := by
+instance isDiscreteValuationRing [Is1DFunctionField K F] : IsDiscreteValuationRing v := by
   sorry
 
 variable {F} in
 /-- [Stichtenoth, Corollary 1.3.4] (finitely many poles). -/
 @[eval_problem]
-theorem Place.finite_setOf_notMem [Is1DFunctionField K F] (x : F) :
+theorem finite_setOf_notMem [Is1DFunctionField K F] (x : F) :
     Finite {v : Place K F | x ∉ v} := by
   sorry
 
+end Place
+
 open scoped RestrictedProduct
 
 /-- [Stichtenoth, Definition 1.5.2]. -/

From be3be79470ead7486b3cd25a165d9dfc3dd833c8 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Mon, 11 May 2026 14:32:55 +0200
Subject: [PATCH 7/9] use Set.Finite

---
 LeanEval/AlgebraicGeometry/FunctionField.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/LeanEval/AlgebraicGeometry/FunctionField.lean b/LeanEval/AlgebraicGeometry/FunctionField.lean
index d5bef2f..ff17069 100644
--- a/LeanEval/AlgebraicGeometry/FunctionField.lean
+++ b/LeanEval/AlgebraicGeometry/FunctionField.lean
@@ -87,8 +87,7 @@ instance isDiscreteValuationRing [Is1DFunctionField K F] : IsDiscreteValuationRi
 variable {F} in
 /-- [Stichtenoth, Corollary 1.3.4] (finitely many poles). -/
 @[eval_problem]
-theorem finite_setOf_notMem [Is1DFunctionField K F] (x : F) :
-    Finite {v : Place K F | x ∉ v} := by
+theorem finite_setOf_notMem [Is1DFunctionField K F] (x : F) : {v : Place K F | x ∉ v}.Finite := by
   sorry
 
 end Place
@@ -144,7 +143,7 @@ Note: if K is not the full constant field of F/K then there are no rational poin
 every place contains the full constant field. -/
 @[eval_problem]
 theorem faltings [NumberField K] [Is1DFunctionField K F] (h : 2 ≤ genus K F) :
-    Finite {v : Place K F | Module.rank K (IsLocalRing.ResidueField v) = 1} := by
+    {v : Place K F | Module.rank K (IsLocalRing.ResidueField v) = 1}.Finite := by
   sorry
 
 end Is1DFunctionField

From ed3eaf7e28f5120fb36685221ac25edf6dca3d48 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Tue, 12 May 2026 23:48:45 +0200
Subject: [PATCH 8/9] address review

---
 LeanEval/AlgebraicGeometry/FunctionField.lean | 51 +++++++------------
 manifests/problems.toml                       | 28 ++++------
 2 files changed, 29 insertions(+), 50 deletions(-)

diff --git a/LeanEval/AlgebraicGeometry/FunctionField.lean b/LeanEval/AlgebraicGeometry/FunctionField.lean
index ff17069..05d6f63 100644
--- a/LeanEval/AlgebraicGeometry/FunctionField.lean
+++ b/LeanEval/AlgebraicGeometry/FunctionField.lean
@@ -1,6 +1,6 @@
 import Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
+import Mathlib.NumberTheory.FunctionField
 import Mathlib.NumberTheory.NumberField.Basic
-import Mathlib.RingTheory.AlgebraicIndependent.Basic
 import Mathlib.RingTheory.DiscreteValuationRing.Basic
 import Mathlib.RingTheory.Valuation.ValuationSubring
 import Mathlib.Topology.Algebra.RestrictedProduct.Basic
@@ -25,27 +25,10 @@ end ValuationSubalgebra
 
 variable (K F: Type*) [Field K] [Field F] [Algebra K F]
 
-namespace Algebra
+class BundledFunctionField extends
+  Algebra (RatFunc K) F, IsScalarTower K (RatFunc K) F, FunctionField K F
 
-class Is1DFunctionField : Prop where
-  trdeg_eq_one : trdeg K F = 1
-  fg : (⊤ : IntermediateField K F).FG
-
-open scoped IntermediateField
-
-variable {K F} in
-/-- The definition `Is1DFunctionField` is equivalent to [Stichtenoth, Definition 1.1.1]. -/
-@[eval_problem]
-theorem is1DFunctionField_iff_exists_transcendental_finiteDimensional :
-    Is1DFunctionField K F ↔ ∃ x : F, Transcendental K x ∧ FiniteDimensional K⟮x⟯ F := by
-  sorry
-
-namespace Is1DFunctionField
-
-@[eval_problem]
-theorem finiteDimensional_of_transcendental [Is1DFunctionField K F]
-    (x : F) (hx : Transcendental K x) : FiniteDimensional K⟮x⟯ F := by
-  sorry
+namespace FunctionField
 
 /-- The type of places of a 1-dimensional function field. See [Stichtenoth,
 Definition 1.1.4 and 1.1.8]. We omit the condition `toSubalgebra ≠ ⊥` since it is automatic. -/
@@ -81,13 +64,14 @@ namespace Place
 variable {K F} in
 /-- [Stichtenoth, Theorem 1.1.6]. -/
 @[eval_problem]
-instance isDiscreteValuationRing [Is1DFunctionField K F] : IsDiscreteValuationRing v := by
+instance isDiscreteValuationRing [BundledFunctionField K F] : IsDiscreteValuationRing v := by
   sorry
 
 variable {F} in
 /-- [Stichtenoth, Corollary 1.3.4] (finitely many poles). -/
 @[eval_problem]
-theorem finite_setOf_notMem [Is1DFunctionField K F] (x : F) : {v : Place K F | x ∉ v}.Finite := by
+theorem finite_setOf_notMem [BundledFunctionField K F] (x : F) :
+    {v : Place K F | x ∉ v}.Finite := by
   sorry
 
 end Place
@@ -99,14 +83,14 @@ abbrev Adele : Type _ := Πʳ v : Place K F, [F, v]
 
 variable {F} in
 /-- The principal adele associated to an element in the function field. -/
-def Adele.principal [Is1DFunctionField K F] : F →+* Adele K F where
+def Adele.principal [BundledFunctionField K F] : F →+* Adele K F where
   toFun x := ⟨fun _ ↦ x, Place.finite_setOf_notMem K x⟩
   map_one' := rfl
   map_mul' _ _ := rfl
   map_zero' := rfl
   map_add' _ _ := rfl
 
-instance [Is1DFunctionField K F] : Algebra F (Adele K F) where
+instance [BundledFunctionField K F] : Algebra F (Adele K F) where
   smul x a := ⟨x • a, (.principal K x * a).2⟩
   algebraMap := Adele.principal K
   commutes' _ _ := mul_comm ..
@@ -121,9 +105,9 @@ instance : Algebra K (Adele K F) where
   algebraMap.map_add' _ _ := by ext; exact (algebraMap K F).map_add ..
   algebraMap.map_zero' := by ext; exact (algebraMap K F).map_zero
   commutes' _ _ := mul_comm ..
-  smul_def' _ _ := by ext; apply smul_def
+  smul_def' _ _ := by ext; apply Algebra.smul_def
 
-instance [Is1DFunctionField K F] : IsScalarTower K F (Adele K F) :=
+instance [BundledFunctionField K F] : IsScalarTower K F (Adele K F) :=
   .of_algebraMap_eq fun _ ↦ rfl
 
 /-- The $K$-subspace $\mathcal{A}_F(0)$, see [Stichtenoth, Definition 1.5.3]. -/
@@ -133,8 +117,13 @@ def integralAdele : Submodule K (Adele K F) where
   zero_mem' _ := zero_mem _
   smul_mem' _ _ h v := v.smul_mem (h v) _
 
+@[eval_problem]
+instance genus_finite [BundledFunctionField K F] : FiniteDimensional K
+    (Adele K F ⧸ integralAdele K F ⊔ (IsScalarTower.toAlgHom K F _).toLinearMap.range) := by
+  sorry
+
 /-- The genus of a function field, [Stichtenoth, Corollary 1.5.5]. -/
-noncomputable def genus [Is1DFunctionField K F] : ℕ := Module.finrank K
+noncomputable def genus [BundledFunctionField K F] : ℕ := Module.finrank K
   (Adele K F ⧸ integralAdele K F ⊔ (IsScalarTower.toAlgHom K F _).toLinearMap.range)
 
 /-- Every function field of genus at least 2 (equivalently, every curve of geometric genus
@@ -142,10 +131,8 @@ at least 2) over a number field has only finitely many rational points.
 Note: if K is not the full constant field of F/K then there are no rational points, because
 every place contains the full constant field. -/
 @[eval_problem]
-theorem faltings [NumberField K] [Is1DFunctionField K F] (h : 2 ≤ genus K F) :
+theorem faltings [NumberField K] [BundledFunctionField K F] (h : 2 ≤ genus K F) :
     {v : Place K F | Module.rank K (IsLocalRing.ResidueField v) = 1}.Finite := by
   sorry
 
-end Is1DFunctionField
-
-end Algebra
+end FunctionField
diff --git a/manifests/problems.toml b/manifests/problems.toml
index cde349d..5d29806 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -646,28 +646,12 @@ holes = ["neukirch_uchida"]
 submitter = "Junyan Xu"
 source = "Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Number Fields*, Theorem 12.2.1."
 
-[[problem]]
-id = "Is1DFunctionField_finiteDimensional_of_transcendental"
-title = "A function field is finite-dimensional over any transcendental subfield"
-test = false
-module = "LeanEval.AlgebraicGeometry.FunctionField"
-holes = ["Algebra.Is1DFunctionField.finiteDimensional_of_transcendental"] 
-submitter = "Junyan Xu"
-
-[[problem]]
-id = "is1DFunctionField_iff_exists_transcendental_finiteDimensional"
-title = "A characterization of function fields of one variable"
-test = false
-module = "LeanEval.AlgebraicGeometry.FunctionField"
-holes = ["is1DFunctionField_iff_exists_transcendental_finiteDimensional"]
-submitter = "Junyan Xu"
-
 [[problem]]
 id = "Place_isDiscreteValuationRing"
 title = "Places of function fields are discrete valuation rings"
 test = false
 module = "LeanEval.AlgebraicGeometry.FunctionField"
-holes = ["Algebra.Is1DFunctionField.Place.isDiscreteValuationRing"]
+holes = ["FunctionField.Place.isDiscreteValuationRing"]
 submitter = "Junyan Xu"
 
 [[problem]]
@@ -675,9 +659,17 @@ id = "Place_finite_setOf_notMem"
 title = "Elements in function fields have finitely many poles"
 test = false
 module = "LeanEval.AlgebraicGeometry.FunctionField"
-holes = ["Algebra.Is1DFunctionField.Place.finite_setOf_notMem"]
+holes = ["FunctionField.Place.finite_setOf_notMem"]
 submitter = "Junyan Xu"
 
+[[problem]]
+id = "FunctionField_genus_finite"
+title = "Genus of a function field is finite"
+test = false
+module = "LeanEval.AlgebraicGeometry.FunctionField"
+holes = ["genus_finite"]
+submitter = "Michael Stoll, Junyan Xu"
+
 [[problem]]
 id = "faltings"
 title = "Faltings' theorem (Mordell conjecture)"

From 145dbab24f030d007ae75e6b4947fa04b8fca8df Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Wed, 13 May 2026 00:07:59 +0200
Subject: [PATCH 9/9] try remove namespaces in holes

---
 manifests/problems.toml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/manifests/problems.toml b/manifests/problems.toml
index 5d29806..bfcd2ee 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -651,7 +651,7 @@ id = "Place_isDiscreteValuationRing"
 title = "Places of function fields are discrete valuation rings"
 test = false
 module = "LeanEval.AlgebraicGeometry.FunctionField"
-holes = ["FunctionField.Place.isDiscreteValuationRing"]
+holes = ["isDiscreteValuationRing"]
 submitter = "Junyan Xu"
 
 [[problem]]
@@ -659,7 +659,7 @@ id = "Place_finite_setOf_notMem"
 title = "Elements in function fields have finitely many poles"
 test = false
 module = "LeanEval.AlgebraicGeometry.FunctionField"
-holes = ["FunctionField.Place.finite_setOf_notMem"]
+holes = ["finite_setOf_notMem"]
 submitter = "Junyan Xu"
 
 [[problem]]