feat(LinearAlgebra/SpecialLinearGroup): special linear group of a module (#30987)

Define the special linear group of a module.

Relate it with `Matrix.SpecialLinearGroup`.

Several additional constructions.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: AntoineChambert-Loir

Mathlib.lean

@@ -4552,6 +4552,7 @@ import Mathlib.LinearAlgebra.SesquilinearForm.Basic
 import Mathlib.LinearAlgebra.SesquilinearForm.Star
 import Mathlib.LinearAlgebra.Span.Basic
 import Mathlib.LinearAlgebra.Span.Defs
+import Mathlib.LinearAlgebra.SpecialLinearGroup
 import Mathlib.LinearAlgebra.StdBasis
 import Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
 import Mathlib.LinearAlgebra.SymmetricAlgebra.Basis

Mathlib/LinearAlgebra/Charpoly/BaseChange.lean

@@ -6,14 +6,17 @@ Authors: Andrew Yang
 import Mathlib.LinearAlgebra.Charpoly.ToMatrix
 import Mathlib.LinearAlgebra.Determinant
 import Mathlib.RingTheory.TensorProduct.Finite
+import Mathlib.LinearAlgebra.TensorProduct.Tower
 
 
 /-! # The characteristic polynomial of base change -/
 
-@[simp]
-lemma LinearMap.charpoly_baseChange {R M} [CommRing R] [AddCommGroup M] [Module R M]
+variable {R M} [CommRing R] [AddCommGroup M] [Module R M]
     [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M)
-    (A) [CommRing A] [Algebra R A] :
+    (A) [CommRing A] [Algebra R A]
+
+@[simp]
+lemma LinearMap.charpoly_baseChange :
     (f.baseChange A).charpoly = f.charpoly.map (algebraMap R A) := by
   nontriviality A
   have := (algebraMap R A).domain_nontrivial
@@ -25,20 +28,23 @@ lemma LinearMap.charpoly_baseChange {R M} [CommRing R] [AddCommGroup M] [Module
   ext i j
   simp [LinearMap.toMatrix_apply, ← Algebra.algebraMap_eq_smul_one]
 
-lemma LinearMap.det_eq_sign_charpoly_coeff {R M} [CommRing R] [AddCommGroup M] [Module R M]
-    [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) :
+lemma LinearMap.det_eq_sign_charpoly_coeff :
     LinearMap.det f = (-1) ^ Module.finrank R M * f.charpoly.coeff 0 := by
   nontriviality R
   rw [← LinearMap.det_toMatrix (Module.Free.chooseBasis R M), Matrix.det_eq_sign_charpoly_coeff,
     ← Module.finrank_eq_card_chooseBasisIndex, charpoly_def]
 
-lemma LinearMap.det_baseChange {R M} [CommRing R] [AddCommGroup M] [Module R M]
-    [Module.Free R M] [Module.Finite R M]
-    {A} [CommRing A] [Algebra R A] (f : M →ₗ[R] M) :
+variable {A} in
+lemma LinearMap.det_baseChange :
     LinearMap.det (f.baseChange A) = algebraMap R A (LinearMap.det f) := by
   nontriviality A
   have := (algebraMap R A).domain_nontrivial
   rw [LinearMap.det_eq_sign_charpoly_coeff, LinearMap.det_eq_sign_charpoly_coeff]
   simp
 
+lemma LinearEquiv.det_baseChange (f : M ≃ₗ[R] M) :
+    LinearEquiv.det (f.baseChange R A _ _) = (LinearEquiv.det f).map (algebraMap R A) := by
+  ext
+  simp [LinearMap.det_baseChange]
+
 /-! Also see `LinearMap.trace_baseChange` in `Mathlib/LinearAlgebra/Trace` -/

Mathlib/LinearAlgebra/Determinant.lean

@@ -7,10 +7,12 @@ import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 import Mathlib.LinearAlgebra.GeneralLinearGroup
 import Mathlib.LinearAlgebra.Matrix.Reindex
 import Mathlib.Tactic.FieldSimp
+import Mathlib.LinearAlgebra.Dual.Basis
+import Mathlib.LinearAlgebra.Matrix.Dual
 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
 import Mathlib.LinearAlgebra.Matrix.Basis
 import Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
-
+import Mathlib.RingTheory.Finiteness.Cardinality
 /-!
 # Determinant of families of vectors
 
@@ -486,6 +488,35 @@ theorem LinearEquiv.coe_ofIsUnitDet {f : M →ₗ[R] M'} {v : Basis ι R M} {v'
   ext x
   rfl
 
+/-- Builds a linear equivalence from an endomorphism whose determinant is a unit. -/
+noncomputable def LinearMap.equivOfIsUnitDet
+    [Module.Free R M] [Module.Finite R M]
+    {f : M →ₗ[R] M} (h : IsUnit f.det) :
+    M ≃ₗ[R] M := by
+  by_cases hR : Nontrivial R
+  · let ⟨ι, b⟩ := (Module.Free.exists_basis R M).some
+    have : Finite ι := Module.Finite.finite_basis b
+    have : Fintype ι := Fintype.ofFinite ι
+    have : DecidableEq ι := Classical.typeDecidableEq ι
+    exact LinearEquiv.ofIsUnitDet (by rwa [det_toMatrix b])
+  · exact 1
+
+@[simp]
+theorem LinearMap.equivOfIsUnitDet_apply
+    [Module.Free R M] [Module.Finite R M]
+    {f : M →ₗ[R] M} (h : IsUnit f.det) (x : M) :
+    (LinearMap.equivOfIsUnitDet h) x = f x := by
+  nontriviality M
+  simp [equivOfIsUnitDet, dif_pos (Module.nontrivial R M)]
+
+@[simp]
+theorem LinearMap.coe_equivOfIsUnitDet
+    [Module.Free R M] [Module.Finite R M]
+    {f : M →ₗ[R] M} (h : IsUnit f.det) :
+    (LinearMap.equivOfIsUnitDet h : M →ₗ[R] M) = f := by
+  ext
+  apply LinearMap.equivOfIsUnitDet_apply
+
 /-- Builds a linear equivalence from a linear map on a finite-dimensional vector space whose
 determinant is nonzero. -/
 abbrev LinearMap.equivOfDetNeZero {𝕜 : Type*} [Field 𝕜] {M : Type*} [AddCommGroup M] [Module 𝕜 M]
@@ -705,3 +736,17 @@ theorem det_isUnitSMul {w : ι → R} (hw : ∀ i, IsUnit (w i)) :
   e.det_unitsSMul_self _
 
 end Module.Basis
+
+section Dual
+
+/-- The determinant of the transpose of an endomorphism coincides with its determinant. -/
+theorem _root_.LinearMap.det_dualMap
+    [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) :
+    f.dualMap.det = f.det := by
+  set b := Module.Free.chooseBasis R M
+  have : Fintype (Module.Free.ChooseBasisIndex R M) :=
+    Module.Free.ChooseBasisIndex.fintype R M
+  rw [← LinearMap.det_toMatrix b, ← LinearMap.det_toMatrix b.dualBasis]
+  simp [LinearMap.dualMap_def, LinearMap.toMatrix_transpose]
+
+end Dual

Mathlib/LinearAlgebra/Dimension/Free.lean

@@ -242,6 +242,24 @@ noncomputable def basisUnique (ι : Type*) [Unique ι]
     Module.finite_of_finrank_pos (_root_.zero_lt_one.trans_le h.symm.le)
   (finBasisOfFinrankEq R M h).reindex (Equiv.ofUnique _ _)
 
+/-- If a finite module of `finrank 1` has a basis, then this basis has a unique element. -/
+theorem Basis.nonempty_unique_index_of_finrank_eq_one
+    {ι : Type*} (b : Module.Basis ι R M) (d1 : Module.finrank R M = 1) :
+    Nonempty (Unique ι) := by
+  -- why isn't this an instance?
+  have : Nontrivial R := nontrivial_of_invariantBasisNumber R
+  haveI : Module.Finite R M :=
+    Module.finite_of_finrank_pos (Nat.lt_of_sub_eq_succ d1)
+  have : Finite ι := Module.Finite.finite_basis b
+  have : Fintype ι := Fintype.ofFinite ι
+  rwa [Module.finrank_eq_card_basis b, Fintype.card_eq_one_iff_nonempty_unique] at d1
+
+theorem nonempty_linearEquiv_of_finrank_eq_one (d1 : Module.finrank R M = 1) :
+    Nonempty (R ≃ₗ[R] M) := by
+  let ⟨ι, b⟩ := (Module.Free.exists_basis R M).some
+  have : Unique ι := (b.nonempty_unique_index_of_finrank_eq_one d1).some
+  exact ⟨((b.equivFun).trans (LinearEquiv.funUnique ι R R)).symm⟩
+
 @[simp]
 theorem basisUnique_repr_eq_zero_iff {ι : Type*} [Unique ι]
     {h : finrank R M = 1} {v : M} {i : ι} :
@@ -250,6 +268,38 @@ theorem basisUnique_repr_eq_zero_iff {ι : Type*} [Unique ι]
     (basisUnique ι h).repr.map_eq_zero_iff.mp (Finsupp.ext fun j => Subsingleton.elim i j ▸ hv),
     fun hv => by rw [hv, LinearEquiv.map_zero, Finsupp.zero_apply]⟩
 
+variable {R : Type*} [CommSemiring R] [StrongRankCondition R]
+    {M : Type*} [AddCommMonoid M] [Module R M] [Module.Free R M]
+
+theorem _root_.LinearMap.existsUnique_eq_smul_id_of_finrank_eq_one
+    (d1 : Module.finrank R M = 1) (u : M →ₗ[R] M) :
+    ∃! c : R, u = c • LinearMap.id := by
+  let e := (nonempty_linearEquiv_of_finrank_eq_one d1).some
+  set c := e.symm (u (e 1)) with hc
+  suffices u = c • LinearMap.id by
+    use c
+    simp only [this, true_and]
+    intro d hcd
+    rw [LinearMap.ext_iff] at hcd
+    simpa using (LinearEquiv.congr_arg (e := e.symm) (hcd (e 1))).symm
+  ext x
+  have (x : M) : x = (e.symm x) • (e 1) := by simp [← LinearEquiv.map_smul]
+  rw [this x]
+  simp only [hc, map_smul, LinearMap.smul_apply, LinearMap.id_coe, id_eq]
+  rw [← this]
+
+/-- Endomorphisms of a free module of rank one are homotheties. -/
+@[simps apply]
+noncomputable def _root_.LinearEquiv.smul_id_of_finrank_eq_one (d1 : Module.finrank R M = 1) :
+    R ≃ₗ[R] (M →ₗ[R] M) where
+  toFun := fun c ↦ c • LinearMap.id
+  map_add' c d := by ext; simp [add_smul]
+  map_smul' c d := by ext; simp [mul_smul]
+  invFun u := (u.existsUnique_eq_smul_id_of_finrank_eq_one d1).choose
+  left_inv c := by
+    simp [← (LinearMap.existsUnique_eq_smul_id_of_finrank_eq_one d1 _).choose_spec.2 c]
+  right_inv u := ((u.existsUnique_eq_smul_id_of_finrank_eq_one d1).choose_spec.1).symm
+
 end Module
 
 namespace Algebra

Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

@@ -170,7 +170,8 @@ theorem Module.rank_le_one_iff_top_isPrincipal [Module.Free K V] :
   rw [← Submodule.rank_le_one_iff_isPrincipal, rank_top]
 
 /-- A module has dimension 1 iff there is some `v : V` so `{v}` is a basis.
--/
+
+See also `Module.Basis.nonempty_unique_index_of_finrank_eq_one` -/
 theorem finrank_eq_one_iff [Module.Free K V] (ι : Type*) [Unique ι] :
     finrank K V = 1 ↔ Nonempty (Basis ι K V) := by
   constructor

Mathlib/LinearAlgebra/GeneralLinearGroup.lean

@@ -43,6 +43,14 @@ def toLinearEquiv (f : GeneralLinearGroup R M) : M ≃ₗ[R] M :=
 @[simp] lemma coe_toLinearEquiv (f : GeneralLinearGroup R M) :
     f.toLinearEquiv = (f : M → M) := rfl
 
+theorem toLinearEquiv_mul (f g : GeneralLinearGroup R M) :
+    (f * g).toLinearEquiv = f.toLinearEquiv * g.toLinearEquiv := by
+  rfl
+
+theorem toLinearEquiv_inv (f : GeneralLinearGroup R M) :
+    (f⁻¹).toLinearEquiv = (f.toLinearEquiv)⁻¹ := by
+  rfl
+
 /-- An equivalence from `M` to itself determines an invertible linear map. -/
 def ofLinearEquiv (f : M ≃ₗ[R] M) : GeneralLinearGroup R M where
   val := f
@@ -53,6 +61,14 @@ def ofLinearEquiv (f : M ≃ₗ[R] M) : GeneralLinearGroup R M where
 @[simp] lemma coe_ofLinearEquiv (f : M ≃ₗ[R] M) :
     ofLinearEquiv f = (f : M → M) := rfl
 
+theorem ofLinearEquiv_mul (f g : M ≃ₗ[R] M) :
+    ofLinearEquiv (f * g) = ofLinearEquiv f * ofLinearEquiv g := by
+  rfl
+
+theorem ofLinearEquiv_inv (f : M ≃ₗ[R] M) :
+    ofLinearEquiv (f⁻¹) = (ofLinearEquiv f)⁻¹ := by
+  rfl
+
 variable (R M) in
 /-- The general linear group on `R` and `M` is multiplicatively equivalent to the type of linear
 equivalences between `M` and itself. -/

Mathlib/LinearAlgebra/Matrix/Dual.lean

@@ -21,7 +21,7 @@ open Matrix Module
 
 section Transpose
 
-variable {K V₁ V₂ ι₁ ι₂ : Type*} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂]
+variable {K V₁ V₂ ι₁ ι₂ : Type*} [CommSemiring K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂]
   [Module K V₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] {B₁ : Basis ι₁ K V₁}
   {B₂ : Basis ι₂ K V₂}
 

Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

@@ -74,6 +74,18 @@ lemma det_ne_zero [Nontrivial R] (g : GL n R) : g.val.det ≠ 0 :=
 def toLin : GL n R ≃* LinearMap.GeneralLinearGroup R (n → R) :=
   Units.mapEquiv toLinAlgEquiv'.toMulEquiv
 
+/-- The isomorphism from `GL n R` to the general linear group of a module
+associated with a basis. -/
+noncomputable def toLin'
+    {V : Type*} [AddCommGroup V] [Module R V] (b : Module.Basis n R V) :
+    GL n R ≃* LinearMap.GeneralLinearGroup R V :=
+  toLin.trans <| LinearMap.GeneralLinearGroup.congrLinearEquiv b.equivFun.symm
+
+lemma toLin'_apply {V : Type*} [AddCommGroup V] [Module R V]
+    (b : Module.Basis n R V) (M : GL n R) (v : V) :
+    (toLin' b M).toLinearEquiv v = Fintype.linearCombination R ⇑b (↑M *ᵥ (b.repr v)) := by
+  simp [toLin', toLin, Fintype.linearCombination_apply, MulEquiv.trans_apply]
+
 /-- Given a matrix with invertible determinant, we get an element of `GL n R`. -/
 @[simps! val]
 def mk' (A : Matrix n n R) (_ : Invertible (Matrix.det A)) : GL n R :=