feat(LinearAlgebra/Matrix): define projective special linear group (l…

…eanprover-community#7791)




Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Mathlib.lean

@@ -2553,6 +2553,7 @@ import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
 import Mathlib.LinearAlgebra.Matrix.Orthogonal
 import Mathlib.LinearAlgebra.Matrix.Polynomial
 import Mathlib.LinearAlgebra.Matrix.PosDef
+import Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup
 import Mathlib.LinearAlgebra.Matrix.Reindex
 import Mathlib.LinearAlgebra.Matrix.SchurComplement
 import Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Mathlib/LinearAlgebra/Matrix/ProjectiveSpecialLinearGroup.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2023 Wen Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wen Yang
+-/
+import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
+
+/-!
+# Projective Special Linear Group
+
+## Notation
+
+In the `MatrixGroups` locale:
+
+* `PSL(n, R)` is a shorthand for `Matrix.ProjectiveSpecialLinearGroup (Fin n) R`
+-/
+
+namespace Matrix
+
+universe u v
+
+open Matrix LinearMap
+
+open scoped MatrixGroups
+
+variable (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R]
+
+/-- A projective special linear group is the quotient of a special linear group by its center.-/
+abbrev ProjectiveSpecialLinearGroup : Type _ :=
+    SpecialLinearGroup n R ⧸ Subgroup.center (SpecialLinearGroup n R)
+
+/-- `PSL(n, R)` is the projective special linear group `SL(n, R)/Z(SL(n, R))`.-/
+scoped[MatrixGroups] notation "PSL(" n ", " R ")" => Matrix.ProjectiveSpecialLinearGroup (Fin n) R