refactor(linear_algebra/basic): extract content about linear_map.general_linear_group (#18345)

eric-wieser · eric-wieser · commit 2705404e701a · 2023-02-02T17:00:14.000Z
diff --git a/src/linear_algebra/affine_space/affine_equiv.lean b/src/linear_algebra/affine_space/affine_equiv.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
 import linear_algebra.affine_space.affine_map
+import linear_algebra.general_linear_group
 import algebra.invertible
 
 /-!
diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean
@@ -25,7 +25,6 @@ Many of the relevant definitions, including `module`, `submodule`, and `linear_m
 * Many constructors for (semi)linear maps
 * The kernel `ker` and range `range` of a linear map are submodules of the domain and codomain
   respectively.
-* The general linear group is defined to be the group of invertible linear maps from `M` to itself.
 
 See `linear_algebra.span` for the span of a set (as a submodule),
 and `linear_algebra.quotient` for quotients by submodules.
@@ -2161,55 +2160,3 @@ rfl
 end linear_equiv
 
 end fun_left
-
-namespace linear_map
-
-variables [semiring R] [add_comm_monoid M] [module R M]
-variables (R M)
-
-/-- The group of invertible linear maps from `M` to itself -/
-@[reducible] def general_linear_group := (M →ₗ[R] M)ˣ
-
-namespace general_linear_group
-variables {R M}
-
-instance : has_coe_to_fun (general_linear_group R M) (λ _, M → M) := by apply_instance
-
-/-- An invertible linear map `f` determines an equivalence from `M` to itself. -/
-def to_linear_equiv (f : general_linear_group R M) : (M ≃ₗ[R] M) :=
-{ inv_fun := f.inv.to_fun,
-  left_inv := λ m, show (f.inv * f.val) m = m,
-    by erw f.inv_val; simp,
-  right_inv := λ m, show (f.val * f.inv) m = m,
-    by erw f.val_inv; simp,
-  ..f.val }
-
-/-- An equivalence from `M` to itself determines an invertible linear map. -/
-def of_linear_equiv (f : (M ≃ₗ[R] M)) : general_linear_group R M :=
-{ val := f,
-  inv := (f.symm : M →ₗ[R] M),
-  val_inv := linear_map.ext $ λ _, f.apply_symm_apply _,
-  inv_val := linear_map.ext $ λ _, f.symm_apply_apply _ }
-
-variables (R M)
-
-/-- The general linear group on `R` and `M` is multiplicatively equivalent to the type of linear
-equivalences between `M` and itself. -/
-def general_linear_equiv : general_linear_group R M ≃* (M ≃ₗ[R] M) :=
-{ to_fun := to_linear_equiv,
-  inv_fun := of_linear_equiv,
-  left_inv := λ f, by { ext, refl },
-  right_inv := λ f, by { ext, refl },
-  map_mul' := λ x y, by {ext, refl} }
-
-@[simp] lemma general_linear_equiv_to_linear_map (f : general_linear_group R M) :
-  (general_linear_equiv R M f : M →ₗ[R] M) = f :=
-by {ext, refl}
-
-@[simp] lemma coe_fn_general_linear_equiv (f : general_linear_group R M) :
-  ⇑(general_linear_equiv R M f) = (f : M → M) :=
-rfl
-
-end general_linear_group
-
-end linear_map
diff --git a/src/linear_algebra/determinant.lean b/src/linear_algebra/determinant.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
 -/
+import linear_algebra.general_linear_group
 import linear_algebra.matrix.reindex
 import tactic.field_simp
 import linear_algebra.matrix.nonsingular_inverse
diff --git a/src/linear_algebra/eigenspace.lean b/src/linear_algebra/eigenspace.lean
@@ -7,6 +7,7 @@ Authors: Alexander Bentkamp
 import algebra.algebra.spectrum
 import order.hom.basic
 import linear_algebra.free_module.finite.basic
+import linear_algebra.general_linear_group
 
 /-!
 # Eigenvectors and eigenvalues
diff --git a/src/linear_algebra/general_linear_group.lean b/src/linear_algebra/general_linear_group.lean
@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2019 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+import algebra.module.equiv
+
+/-!
+# The general linear group of linear maps
+
+The general linear group is defined to be the group of invertible linear maps from `M` to itself.
+
+See also `matrix.general_linear_group`
+
+## Main definitions
+
+* `linear_map.general_linear_group`
+
+-/
+
+variables (R M : Type*)
+
+namespace linear_map
+
+variables [semiring R] [add_comm_monoid M] [module R M]
+variables (R M)
+
+/-- The group of invertible linear maps from `M` to itself -/
+@[reducible] def general_linear_group := (M →ₗ[R] M)ˣ
+
+namespace general_linear_group
+variables {R M}
+
+instance : has_coe_to_fun (general_linear_group R M) (λ _, M → M) := by apply_instance
+
+/-- An invertible linear map `f` determines an equivalence from `M` to itself. -/
+def to_linear_equiv (f : general_linear_group R M) : (M ≃ₗ[R] M) :=
+{ inv_fun := f.inv.to_fun,
+  left_inv := λ m, show (f.inv * f.val) m = m,
+    by erw f.inv_val; simp,
+  right_inv := λ m, show (f.val * f.inv) m = m,
+    by erw f.val_inv; simp,
+  ..f.val }
+
+/-- An equivalence from `M` to itself determines an invertible linear map. -/
+def of_linear_equiv (f : (M ≃ₗ[R] M)) : general_linear_group R M :=
+{ val := f,
+  inv := (f.symm : M →ₗ[R] M),
+  val_inv := linear_map.ext $ λ _, f.apply_symm_apply _,
+  inv_val := linear_map.ext $ λ _, f.symm_apply_apply _ }
+
+variables (R M)
+
+/-- The general linear group on `R` and `M` is multiplicatively equivalent to the type of linear
+equivalences between `M` and itself. -/
+def general_linear_equiv : general_linear_group R M ≃* (M ≃ₗ[R] M) :=
+{ to_fun := to_linear_equiv,
+  inv_fun := of_linear_equiv,
+  left_inv := λ f, by { ext, refl },
+  right_inv := λ f, by { ext, refl },
+  map_mul' := λ x y, by {ext, refl} }
+
+@[simp] lemma general_linear_equiv_to_linear_map (f : general_linear_group R M) :
+  (general_linear_equiv R M f : M →ₗ[R] M) = f :=
+by {ext, refl}
+
+@[simp] lemma coe_fn_general_linear_equiv (f : general_linear_group R M) :
+  ⇑(general_linear_equiv R M f) = (f : M → M) :=
+rfl
+
+end general_linear_group
+
+end linear_map
diff --git a/src/linear_algebra/matrix/general_linear_group.lean b/src/linear_algebra/matrix/general_linear_group.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Chris Birkbeck. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Birkbeck
 -/
+import linear_algebra.general_linear_group
 import linear_algebra.matrix.nonsingular_inverse
 import linear_algebra.matrix.special_linear_group
 
diff --git a/src/linear_algebra/matrix/special_linear_group.lean b/src/linear_algebra/matrix/special_linear_group.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
+import linear_algebra.general_linear_group
 import linear_algebra.matrix.adjugate
 import linear_algebra.matrix.to_lin
 
diff --git a/src/linear_algebra/unitary_group.lean b/src/linear_algebra/unitary_group.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Shing Tak Lam. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shing Tak Lam
 -/
+import linear_algebra.general_linear_group
 import linear_algebra.matrix.to_lin
 import linear_algebra.matrix.nonsingular_inverse
 import algebra.star.unitary
diff --git a/src/number_theory/modular.lean b/src/number_theory/modular.lean
@@ -6,6 +6,7 @@ Authors: Alex Kontorovich, Heather Macbeth, Marc Masdeu
 
 import analysis.complex.upper_half_plane.basic
 import analysis.normed_space.finite_dimension
+import linear_algebra.general_linear_group
 import linear_algebra.matrix.general_linear_group
 
 /-!
