From 622843a310066a01e1275cc677561448376ed012 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Tue, 5 May 2026 00:22:06 +0200 Subject: [PATCH 1/4] =?UTF-8?q?feat(NumberTheory):=20Neukirch=E2=80=93Uchi?= =?UTF-8?q?da=20theorem?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanEval/NumberTheory/NeukirchUchida.lean | 26 +++++++++++++++++++++++ manifests/problems.toml | 11 +++++++++- 2 files changed, 36 insertions(+), 1 deletion(-) create mode 100644 LeanEval/NumberTheory/NeukirchUchida.lean diff --git a/LeanEval/NumberTheory/NeukirchUchida.lean b/LeanEval/NumberTheory/NeukirchUchida.lean new file mode 100644 index 0000000..463174d --- /dev/null +++ b/LeanEval/NumberTheory/NeukirchUchida.lean @@ -0,0 +1,26 @@ +import Mathlib.FieldTheory.KrullTopology +import Mathlib.NumberTheory.NumberField.Basic +import EvalTools.Markers + +/-! +# The Neukirch–Uchida theorem + +Every topological group isomorphism between absolute Galois groups of two number fields +is induced by an isomorphism between the fields. A foundational result of anabelian geometry. + +References: +https://en.wikipedia.org/wiki/Neukirch%E2%80%93Uchida_theorem +Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Number Fields*, Theorem 12.2.1. +-/ + +namespace LeanEval.NumberTheory + +@[eval_problem] +theorem neukirch_uchida {K₁ K₂ K₁' K₂' : Type*} [Field K₁] [Field K₂] [Field K₁'] [Field K₂'] + [NumberField K₁] [NumberField K₂] [Algebra K₁ K₁'] [Algebra K₂ K₂'] [IsAlgClosure K₁ K₁'] + [IsAlgClosure K₂ K₂'] (ϕ : Gal(K₁'/K₁) ≃* Gal(K₂'/K₂)) (he : IsHomeomorph ϕ) : + ∃! σ : K₁' ≃+* K₂', (algebraMap K₁ K₁').range.map σ.toRingHom = (algebraMap K₂ K₂').range ∧ + ∀ g : Gal(K₁'/K₁), g.toRingEquiv.trans σ = σ.trans (ϕ g) := by + sorry + +end LeanEval.NumberTheory diff --git a/manifests/problems.toml b/manifests/problems.toml index 5a8d975..0bc4664 100644 --- a/manifests/problems.toml +++ b/manifests/problems.toml @@ -635,4 +635,13 @@ test = false module = "LeanEval.Geometry.RadoTheorem" holes = ["rado_riemannSurface"] submitter = "Junyan Xu" -source = "John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, §1.3." \ No newline at end of file +source = "John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, §1.3." + +[[problem]] +id = "neukirch_uchida" +title = "Neukirch–Uchida theorem" +test = false +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." From 717b35a058b99dcd7aba543bffceee11c60bdc6e Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Tue, 5 May 2026 00:41:26 +0200 Subject: [PATCH 2/4] adjustments --- LeanEval/NumberTheory/NeukirchUchida.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/LeanEval/NumberTheory/NeukirchUchida.lean b/LeanEval/NumberTheory/NeukirchUchida.lean index 463174d..ddf0abc 100644 --- a/LeanEval/NumberTheory/NeukirchUchida.lean +++ b/LeanEval/NumberTheory/NeukirchUchida.lean @@ -5,8 +5,8 @@ import EvalTools.Markers /-! # The Neukirch–Uchida theorem -Every topological group isomorphism between absolute Galois groups of two number fields -is induced by an isomorphism between the fields. A foundational result of anabelian geometry. +Every topological group isomorphism between absolute Galois groups of two number fields is +induced by a unique isomorphism between the fields. A foundational result of anabelian geometry. References: https://en.wikipedia.org/wiki/Neukirch%E2%80%93Uchida_theorem @@ -17,10 +17,10 @@ namespace LeanEval.NumberTheory @[eval_problem] theorem neukirch_uchida {K₁ K₂ K₁' K₂' : Type*} [Field K₁] [Field K₂] [Field K₁'] [Field K₂'] - [NumberField K₁] [NumberField K₂] [Algebra K₁ K₁'] [Algebra K₂ K₂'] [IsAlgClosure K₁ K₁'] - [IsAlgClosure K₂ K₂'] (ϕ : Gal(K₁'/K₁) ≃* Gal(K₂'/K₂)) (he : IsHomeomorph ϕ) : + [NumberField K₁] [NumberField K₂] [Algebra K₁ K₁'] [Algebra K₂ K₂'] [IsSepClosure K₁ K₁'] + [IsSepClosure K₂ K₂'] (ϕ : Gal(K₁'/K₁) ≃* Gal(K₂'/K₂)) (he : IsHomeomorph ϕ) : ∃! σ : K₁' ≃+* K₂', (algebraMap K₁ K₁').range.map σ.toRingHom = (algebraMap K₂ K₂').range ∧ - ∀ g : Gal(K₁'/K₁), g.toRingEquiv.trans σ = σ.trans (ϕ g) := by + ∀ g : Gal(K₁'/K₁), ϕ g = σ.symm.trans (g.toRingEquiv.trans σ) := by sorry end LeanEval.NumberTheory From bf0ef7fe5d923ae5ca5f3f252028ea5a7d9300c8 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Tue, 5 May 2026 00:54:18 +0200 Subject: [PATCH 3/4] =?UTF-8?q?swap=20=CF=83=20with=20=CF=83.symm=20(revie?= =?UTF-8?q?w=20by=20@adamtopaz)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanEval/NumberTheory/NeukirchUchida.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanEval/NumberTheory/NeukirchUchida.lean b/LeanEval/NumberTheory/NeukirchUchida.lean index ddf0abc..474dbdc 100644 --- a/LeanEval/NumberTheory/NeukirchUchida.lean +++ b/LeanEval/NumberTheory/NeukirchUchida.lean @@ -19,8 +19,8 @@ namespace LeanEval.NumberTheory theorem neukirch_uchida {K₁ K₂ K₁' K₂' : Type*} [Field K₁] [Field K₂] [Field K₁'] [Field K₂'] [NumberField K₁] [NumberField K₂] [Algebra K₁ K₁'] [Algebra K₂ K₂'] [IsSepClosure K₁ K₁'] [IsSepClosure K₂ K₂'] (ϕ : Gal(K₁'/K₁) ≃* Gal(K₂'/K₂)) (he : IsHomeomorph ϕ) : - ∃! σ : K₁' ≃+* K₂', (algebraMap K₁ K₁').range.map σ.toRingHom = (algebraMap K₂ K₂').range ∧ - ∀ g : Gal(K₁'/K₁), ϕ g = σ.symm.trans (g.toRingEquiv.trans σ) := by + ∃! σ : K₂' ≃+* K₁', (algebraMap K₂ K₂').range.map σ.toRingHom = (algebraMap K₁ K₁').range ∧ + ∀ g : Gal(K₁'/K₁), ϕ g = σ.trans (g.toRingEquiv.trans σ.symm) := by sorry end LeanEval.NumberTheory From 7924a4dabe7bbc337d85ed4ee8e285641c151821 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Tue, 5 May 2026 01:31:54 +0200 Subject: [PATCH 4/4] fix natural language statement --- LeanEval/NumberTheory/NeukirchUchida.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/LeanEval/NumberTheory/NeukirchUchida.lean b/LeanEval/NumberTheory/NeukirchUchida.lean index 474dbdc..b432a82 100644 --- a/LeanEval/NumberTheory/NeukirchUchida.lean +++ b/LeanEval/NumberTheory/NeukirchUchida.lean @@ -5,8 +5,9 @@ import EvalTools.Markers /-! # The Neukirch–Uchida theorem -Every topological group isomorphism between absolute Galois groups of two number fields is -induced by a unique isomorphism between the fields. A foundational result of anabelian geometry. +Every topological group isomorphism between absolute Galois groups of two number fields is induced +by a unique isomorphism between their separable closures that sends one field to the other. +A foundational result of anabelian geometry. References: https://en.wikipedia.org/wiki/Neukirch%E2%80%93Uchida_theorem