lean-eval generated Mostow rigidity (compact version) dependency file

ChallengeDeps.lean

import Mathlib

/-!
# 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. 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
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 ..))

/-- `PO p q` is the projective indefinite orthogonal group PO(p,q) over the reals. -/
@[reducible]
def PO := unitary (MatrixSum (Fin p) (Fin q) ℝ) ⧸ Subgroup.center _



end LeanEval.Geometry