From 324931503dfe0b5ae263930543f90aee616ae273 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 15 Jul 2026 09:34:10 +0200 Subject: [PATCH 1/7] feat(Geometry): Mostow rigidity, algebraic form --- LeanEval/Geometry/MostowRigidity.lean | 130 ++++++++++++++++++++++++ manifests/problems/mostow_rigidity.toml | 7 ++ 2 files changed, 137 insertions(+) create mode 100644 LeanEval/Geometry/MostowRigidity.lean create mode 100644 manifests/problems/mostow_rigidity.toml diff --git a/LeanEval/Geometry/MostowRigidity.lean b/LeanEval/Geometry/MostowRigidity.lean new file mode 100644 index 00000000..3425f137 --- /dev/null +++ b/LeanEval/Geometry/MostowRigidity.lean @@ -0,0 +1,130 @@ +import Mathlib.Algebra.Star.Unitary +import Mathlib.Data.Real.Star +import Mathlib.LinearAlgebra.Matrix.ConjTranspose +import Mathlib.MeasureTheory.Group.FundamentalDomain +import Mathlib.MeasureTheory.Measure.Haar.Basic +import Mathlib.Topology.Instances.Matrix +import Mathlib.Topology.MetricSpace.Pseudo.Defs +import EvalTools.Markers + +/-! +# Mostow rigidity + +A common form of Mostow's rigidity theorem says that two complete, finite-volume hyperbolic +manifolds of dimension at least three must be isometric if they have isomorphic fundamental +groups. Since the group of isometries of the hyperbolic space ℍⁿ is isomorphic to the +projective orthogonal group PO(n,1), this can be shown to be equivalent to the following +algebraic statement: two lattices (subgroups of finite covolume) in PO(n,1) with n ≥ 3 are +isomorphic iff they are conjugate in PO(n,1). In this file we define the group PO(n,1) and +state this algebraic form of Mostow rigidity. In fact, the isomorphism should agree with +conju + +References: +https://en.wikipedia.org/wiki/Mostow_rigidity_theorem#Algebraic_form +Riccardo Benedetti, Carlo Petronio. *Lectures on Hyperbolic Geometry*, Chapter C +(proof of geometric form in compact case in 50 pages). +-/ + +namespace LeanEval.Geometry + +universe u + +variable (p q : Type u) (α : Type*) + +def MatrixSum : Type _ := Matrix (p ⊕ q) (p ⊕ q) α + +variable [Fintype p] [Fintype q] [DecidableEq p] [DecidableEq q] [Ring α] + +instance : Ring (MatrixSum p q α) := inferInstanceAs (Ring (Matrix ..)) + +variable {p q α} in +def MatrixSum.ofMatrix : Matrix (p ⊕ q) (p ⊕ q) α ≃+* MatrixSum p q α := .refl _ + +variable {p q α} in +def pmOneMat : Matrix (p ⊕ q) (p ⊕ q) α := .fromBlocks 1 0 0 (-1) + +theorem pmOneMat_mul_pmOneMat : pmOneMat * pmOneMat = (1 : Matrix (p ⊕ q) _ α) := by + simp [pmOneMat, Matrix.fromBlocks_multiply] + +open MatrixSum Matrix + +section Star + +variable [StarRing α] + +omit [Fintype p] [Fintype q] in +@[simp] theorem conjTranspose_pmOneMat : (pmOneMat : Matrix (p ⊕ q) _ α)ᴴ = pmOneMat := by + simp_rw [pmOneMat, conjTranspose, fromBlocks_transpose, fromBlocks_map] + simp [Matrix.map_neg] + +instance : StarRing (MatrixSum p q α) where + star A := .ofMatrix (pmOneMat * (ofMatrix.symm A).conjTranspose * pmOneMat) + star_involutive A := by + simp [← mul_assoc pmOneMat, mul_assoc (ofMatrix.symm A), pmOneMat_mul_pmOneMat] + star_mul A B := by + conv_lhs => rw [map_mul _ A, conjTranspose_mul, ← mul_one _ᴴ, ← pmOneMat_mul_pmOneMat] + simp [mul_assoc] + star_add A B := by simp [add_mul, mul_add] + +end Star + +section Topology + +variable [TopologicalSpace α] + +instance : TopologicalSpace (MatrixSum p q α) := inferInstanceAs (TopologicalSpace (Matrix ..)) + +instance [T1Space α] : T1Space (MatrixSum p q α) := inferInstanceAs (T1Space (_ → _)) + +instance [LocallyCompactSpace α] : LocallyCompactSpace (MatrixSum p q α) := + inferInstanceAs (LocallyCompactSpace (_ → _)) + +@[fun_prop] theorem MatrixSum.continuous_ofMatrix : Continuous (@ofMatrix p q α _ _ _ _ _) := + continuous_id + +@[fun_prop] theorem MatrixSum.continuous_ofMatrix_symm : Continuous (@ofMatrix p q α ..).symm := + continuous_id + +variable [IsTopologicalRing α] + +instance [Star α] [ContinuousStar α] : IsTopologicalRing (MatrixSum p q α) := + inferInstanceAs (IsTopologicalRing (Matrix ..)) + +variable [StarRing α] [ContinuousStar α] + +instance : ContinuousStar (MatrixSum p q α) where + continuous_star := by rw [star]; fun_prop + +theorem MatrixSum.isClosed_unitary [T1Space α] : + IsClosed (SetLike.coe <| unitary (MatrixSum p q α)) := + .inter (isClosed_singleton.preimage <| by fun_prop) (isClosed_singleton.preimage <| by fun_prop) + +instance [T1Space α] [LocallyCompactSpace α] : + LocallyCompactSpace (unitary (MatrixSum p q α)) := + (MatrixSum.isClosed_unitary ..).isClosedEmbedding_subtypeVal.locallyCompactSpace + +instance : IsTopologicalGroup (unitary (MatrixSum p q α)) where + continuous_inv := by simp_rw [Inv.inv, star]; fun_prop + +end Topology + +variable (p q : ℕ) + +/-- `PO p q` is the projective indefinite orthogonal group PO(p,q) over the reals. -/ +abbrev PO : Type _ := unitary (MatrixSum (Fin p) (Fin q) ℝ) ⧸ Subgroup.center _ + +instance : MeasurableSpace (PO p q) := borel _ +instance : BorelSpace (PO p q) := ⟨rfl⟩ + +open MeasureTheory + +noncomputable instance : MeasureSpace (PO p q) := ⟨.haar⟩ + +@[eval_problem] +theorem mostow_rigidity (n : ℕ) (hn : 3 ≤ n) (Γ Λ : Subgroup (PO n 1)) + (disc_Γ : IsDiscrete (SetLike.coe Γ)) (covol_Γ : covolume Γ (PO n 1) ≠ ⊤) + (disc_Λ : IsDiscrete (SetLike.coe Λ)) (covol_Λ : covolume Λ (PO n 1) ≠ ⊤) + (f : Γ ≃* Λ) : ∃ g : PO n 1, Γ.map (MulAut.conj g) = Λ := by + sorry + +end LeanEval.Geometry diff --git a/manifests/problems/mostow_rigidity.toml b/manifests/problems/mostow_rigidity.toml new file mode 100644 index 00000000..46ef0ace --- /dev/null +++ b/manifests/problems/mostow_rigidity.toml @@ -0,0 +1,7 @@ +id = "mostow_rigidity" +title = "Mostow rigidity" +test = false +module = "LeanEval.Geometry.MostowRigidity" +holes = ["mostow_rigidity"] +submitter = "Junyan Xu" +source = "https://en.wikipedia.org/wiki/Mostow_rigidity_theorem#Algebraic_form" \ No newline at end of file From 3d56f7b6b4cc8b4937184d8d3264811cedb7012a Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 15 Jul 2026 14:35:48 +0200 Subject: [PATCH 2/7] fix? --- LeanEval/Geometry/MostowRigidity.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/LeanEval/Geometry/MostowRigidity.lean b/LeanEval/Geometry/MostowRigidity.lean index 3425f137..1a3c3cb9 100644 --- a/LeanEval/Geometry/MostowRigidity.lean +++ b/LeanEval/Geometry/MostowRigidity.lean @@ -111,7 +111,8 @@ end Topology variable (p q : ℕ) /-- `PO p q` is the projective indefinite orthogonal group PO(p,q) over the reals. -/ -abbrev PO : Type _ := unitary (MatrixSum (Fin p) (Fin q) ℝ) ⧸ Subgroup.center _ +@[reducible] +def PO : Type _ := unitary (MatrixSum (Fin p) (Fin q) ℝ) ⧸ Subgroup.center _ instance : MeasurableSpace (PO p q) := borel _ instance : BorelSpace (PO p q) := ⟨rfl⟩ From 2406b4cb2ada628136102d27990cdfcc73f04216 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 15 Jul 2026 19:00:43 +0200 Subject: [PATCH 3/7] fix? --- LeanEval/Geometry/MostowRigidity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanEval/Geometry/MostowRigidity.lean b/LeanEval/Geometry/MostowRigidity.lean index 1a3c3cb9..d60c8783 100644 --- a/LeanEval/Geometry/MostowRigidity.lean +++ b/LeanEval/Geometry/MostowRigidity.lean @@ -112,7 +112,7 @@ variable (p q : ℕ) /-- `PO p q` is the projective indefinite orthogonal group PO(p,q) over the reals. -/ @[reducible] -def PO : Type _ := unitary (MatrixSum (Fin p) (Fin q) ℝ) ⧸ Subgroup.center _ +def PO := unitary (MatrixSum (Fin p) (Fin q) ℝ) ⧸ Subgroup.center _ instance : MeasurableSpace (PO p q) := borel _ instance : BorelSpace (PO p q) := ⟨rfl⟩ From 7c5e5a7452dfbcc08bf311a61b28b9275156faae Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 15 Jul 2026 23:03:48 +0200 Subject: [PATCH 4/7] verified fix --- LeanEval/Geometry/MostowRigidity.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/LeanEval/Geometry/MostowRigidity.lean b/LeanEval/Geometry/MostowRigidity.lean index d60c8783..f6753ad2 100644 --- a/LeanEval/Geometry/MostowRigidity.lean +++ b/LeanEval/Geometry/MostowRigidity.lean @@ -121,6 +121,12 @@ open MeasureTheory noncomputable instance : MeasureSpace (PO p q) := ⟨.haar⟩ +end LeanEval.Geometry + +namespace LeanEval.Geometry + +open MeasureTheory + @[eval_problem] theorem mostow_rigidity (n : ℕ) (hn : 3 ≤ n) (Γ Λ : Subgroup (PO n 1)) (disc_Γ : IsDiscrete (SetLike.coe Γ)) (covol_Γ : covolume Γ (PO n 1) ≠ ⊤) From 14fe7212da584d516b4922c62e3525c27b7a4e82 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 15 Jul 2026 23:22:46 +0200 Subject: [PATCH 5/7] add compact version --- LeanEval/Geometry/MostowRigidity.lean | 11 +++++++++-- manifests/problems/mostow_rigidity_compact.toml | 8 ++++++++ 2 files changed, 17 insertions(+), 2 deletions(-) create mode 100644 manifests/problems/mostow_rigidity_compact.toml diff --git a/LeanEval/Geometry/MostowRigidity.lean b/LeanEval/Geometry/MostowRigidity.lean index f6753ad2..a6a2668a 100644 --- a/LeanEval/Geometry/MostowRigidity.lean +++ b/LeanEval/Geometry/MostowRigidity.lean @@ -16,8 +16,8 @@ groups. Since the group of isometries of the hyperbolic space ℍⁿ is isomorph projective orthogonal group PO(n,1), this can be shown to be equivalent to the following algebraic statement: two lattices (subgroups of finite covolume) in PO(n,1) with n ≥ 3 are isomorphic iff they are conjugate in PO(n,1). In this file we define the group PO(n,1) and -state this algebraic form of Mostow rigidity. In fact, the isomorphism should agree with -conju +state this algebraic form of Mostow rigidity. We also state the version for cocompact +lattices, since the proof might be easier. References: https://en.wikipedia.org/wiki/Mostow_rigidity_theorem#Algebraic_form @@ -127,6 +127,13 @@ namespace LeanEval.Geometry open MeasureTheory +@[eval_problem] +theorem mostow_rigidity_compact (n : ℕ) (hn : 3 ≤ n) (Γ Λ : Subgroup (PO n 1)) + (disc_Γ : IsDiscrete (SetLike.coe Γ)) [CompactSpace (PO n 1 ⧸ Γ)] + (disc_Λ : IsDiscrete (SetLike.coe Λ)) [CompactSpace (PO n 1 ⧸ Λ)] + (f : Γ ≃* Λ) : ∃ g : PO n 1, Γ.map (MulAut.conj g) = Λ := by + sorry + @[eval_problem] theorem mostow_rigidity (n : ℕ) (hn : 3 ≤ n) (Γ Λ : Subgroup (PO n 1)) (disc_Γ : IsDiscrete (SetLike.coe Γ)) (covol_Γ : covolume Γ (PO n 1) ≠ ⊤) diff --git a/manifests/problems/mostow_rigidity_compact.toml b/manifests/problems/mostow_rigidity_compact.toml new file mode 100644 index 00000000..71cc00f8 --- /dev/null +++ b/manifests/problems/mostow_rigidity_compact.toml @@ -0,0 +1,8 @@ +id = "mostow_rigidity_compact" +title = "Mostow rigidity (compact case)" +test = false +module = "LeanEval.Geometry.MostowRigidity" +holes = ["mostow_rigidity_compact"] +submitter = "Junyan Xu" +notes = "A proof is presented in Riccardo Benedetti, Carlo Petronio. *Lectures on Hyperbolic Geometry*, Chapter C." +source = "https://en.wikipedia.org/wiki/Mostow_rigidity_theorem#Algebraic_form" \ No newline at end of file From 5d501987dc054cfbcdbc35795091ee97def0236a Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Fri, 31 Jul 2026 23:08:18 +0800 Subject: [PATCH 6/7] remove cocompact version --- LeanEval/Geometry/MostowRigidity.lean | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/LeanEval/Geometry/MostowRigidity.lean b/LeanEval/Geometry/MostowRigidity.lean index a6a2668a..67fa0724 100644 --- a/LeanEval/Geometry/MostowRigidity.lean +++ b/LeanEval/Geometry/MostowRigidity.lean @@ -16,8 +16,7 @@ groups. Since the group of isometries of the hyperbolic space ℍⁿ is isomorph projective orthogonal group PO(n,1), this can be shown to be equivalent to the following algebraic statement: two lattices (subgroups of finite covolume) in PO(n,1) with n ≥ 3 are isomorphic iff they are conjugate in PO(n,1). In this file we define the group PO(n,1) and -state this algebraic form of Mostow rigidity. We also state the version for cocompact -lattices, since the proof might be easier. +state this algebraic form of Mostow rigidity. References: https://en.wikipedia.org/wiki/Mostow_rigidity_theorem#Algebraic_form @@ -127,13 +126,6 @@ namespace LeanEval.Geometry open MeasureTheory -@[eval_problem] -theorem mostow_rigidity_compact (n : ℕ) (hn : 3 ≤ n) (Γ Λ : Subgroup (PO n 1)) - (disc_Γ : IsDiscrete (SetLike.coe Γ)) [CompactSpace (PO n 1 ⧸ Γ)] - (disc_Λ : IsDiscrete (SetLike.coe Λ)) [CompactSpace (PO n 1 ⧸ Λ)] - (f : Γ ≃* Λ) : ∃ g : PO n 1, Γ.map (MulAut.conj g) = Λ := by - sorry - @[eval_problem] theorem mostow_rigidity (n : ℕ) (hn : 3 ≤ n) (Γ Λ : Subgroup (PO n 1)) (disc_Γ : IsDiscrete (SetLike.coe Γ)) (covol_Γ : covolume Γ (PO n 1) ≠ ⊤) From 696d2d33566c1255d301fc21524180fed8007c4d Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Fri, 31 Jul 2026 23:15:56 +0800 Subject: [PATCH 7/7] remove mostow_rigidity_compact.toml --- manifests/problems/mostow_rigidity_compact.toml | 8 -------- 1 file changed, 8 deletions(-) delete mode 100644 manifests/problems/mostow_rigidity_compact.toml diff --git a/manifests/problems/mostow_rigidity_compact.toml b/manifests/problems/mostow_rigidity_compact.toml deleted file mode 100644 index 71cc00f8..00000000 --- a/manifests/problems/mostow_rigidity_compact.toml +++ /dev/null @@ -1,8 +0,0 @@ -id = "mostow_rigidity_compact" -title = "Mostow rigidity (compact case)" -test = false -module = "LeanEval.Geometry.MostowRigidity" -holes = ["mostow_rigidity_compact"] -submitter = "Junyan Xu" -notes = "A proof is presented in Riccardo Benedetti, Carlo Petronio. *Lectures on Hyperbolic Geometry*, Chapter C." -source = "https://en.wikipedia.org/wiki/Mostow_rigidity_theorem#Algebraic_form" \ No newline at end of file