The special linear group of a module

If R is a commutative ring and V is an R-module, we define SpecialLinearGroup R V as the subtype of linear equivalences V ≃ₗ[R] V with determinant 1. When V doesn't have a finite basis, the determinant is defined to be 1 and the definition gives V ≃ₗ[R] V. The interest of this definition is that SpecialLinearGroup R V has a group structure. (Starting from linear maps wouldn't have worked.)

The file is constructed parallel to the one defining Matrix.SpecialLinearGroup.

We provide SpecialLinearGroup.toLinearEquiv: the canonical map from SpecialLinearGroup R V to V ≃ₗ[R] V, as a monoid hom.

When V is free and finite over R, we define

• SpecialLinearGroup.dualMap
• SpecialLinearGroup.baseChange

We define Matrix.SpecialLinearGroup.toLin'_equiv: the multiplicative equivalence from Matrix.SpecialLinearGroup n R to SpecialLinearGroup R (n → R) and its variant Matrix.SpecialLinearGroup.toLin_equiv, from Matrix.SpecialLinearGroup n R to SpecialLinearGroup R V, associated with a finite basis of V.

@[reducible, inline]

abbrev SpecialLinearGroup (R : Type u_1) (V : Type u_2) [CommRing R] [AddCommGroup V] [Module R V] : Type u_2

The special linear group of a module.

This is only meaningful when the module is finite and free, for otherwise, it coincides with the group of linear equivalences.

theorem SpecialLinearGroup.det_eq_one {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (u : SpecialLinearGroup R V) : LinearMap.det ↑↑u = 1

@[implicit_reducible]

instance SpecialLinearGroup.instCoeFunForall {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : CoeFun (SpecialLinearGroup R V) fun (x : SpecialLinearGroup R V) => V → V

The coercion from SpecialLinearGroup R V to the function type V → V

theorem SpecialLinearGroup.ext_iff {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (u v : SpecialLinearGroup R V) : u = v ↔ ∀ (x : V), (fun (x : V) => ↑u x) x = (fun (x : V) => ↑v x) x

theorem SpecialLinearGroup.ext {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (u v : SpecialLinearGroup R V) : (∀ (x : V), (fun (x : V) => ↑u x) x = (fun (x : V) => ↑v x) x) → u = v

theorem SpecialLinearGroup.subsingleton_of_finrank_eq_one {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] (d1 : Module.finrank R V = 1) : Subsingleton (SpecialLinearGroup R V)

If a free module has Module.finrank equal to 1, then its special linear group is trivial.

@[implicit_reducible]

instance SpecialLinearGroup.instInv {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : Inv (SpecialLinearGroup R V)

@[implicit_reducible]

instance SpecialLinearGroup.instMul {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : Mul (SpecialLinearGroup R V)

@[implicit_reducible]

instance SpecialLinearGroup.instDiv {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : Div (SpecialLinearGroup R V)

@[implicit_reducible]

instance SpecialLinearGroup.instOne {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : One (SpecialLinearGroup R V)

@[implicit_reducible]

instance SpecialLinearGroup.instPowNat {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : Pow (SpecialLinearGroup R V) ℕ

@[implicit_reducible]

instance SpecialLinearGroup.instPowInt {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : Pow (SpecialLinearGroup R V) ℤ

@[implicit_reducible]

instance SpecialLinearGroup.instInhabited {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : Inhabited (SpecialLinearGroup R V)

def SpecialLinearGroup.dualMap {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (A : SpecialLinearGroup R V) : SpecialLinearGroup R (Module.Dual R V)

The transpose of an element in SpecialLinearGroup R V.

def SpecialLinearGroup.«term_ᵀ» : Lean.TrailingParserDescr

The transpose of an element in SpecialLinearGroup R V.

theorem SpecialLinearGroup.coe_mk {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : V ≃ₗ[R] V) (h : LinearEquiv.det A = 1) : ↑⟨A, h⟩ = A

@[simp]

theorem SpecialLinearGroup.coe_mul {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A B : SpecialLinearGroup R V) : ↑(A * B) = ↑A * ↑B

@[simp]

theorem SpecialLinearGroup.coe_div {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A B : SpecialLinearGroup R V) : ↑(A / B) = ↑A / ↑B

@[simp]

theorem SpecialLinearGroup.coe_inv {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : SpecialLinearGroup R V) : ↑A⁻¹ = (↑A)⁻¹

@[simp]

theorem SpecialLinearGroup.coe_one {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : ↑1 = 1

@[simp]

theorem SpecialLinearGroup.det_coe {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : SpecialLinearGroup R V) : LinearEquiv.det ↑A = 1

@[simp]

theorem SpecialLinearGroup.coe_pow {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : SpecialLinearGroup R V) (m : ℕ) : ↑(A ^ m) = ↑A ^ m

@[simp]

theorem SpecialLinearGroup.coe_zpow {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : SpecialLinearGroup R V) (m : ℤ) : ↑(A ^ m) = ↑A ^ m

@[simp]

theorem SpecialLinearGroup.coe_dualMap {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : SpecialLinearGroup R V) [Module.Free R V] [Module.Finite R V] : ↑A.dualMap = (↑A).dualMap

@[implicit_reducible]

instance SpecialLinearGroup.instGroup {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : Group (SpecialLinearGroup R V)

The special linear group of a module is a group.

def SpecialLinearGroup.toLinearEquiv {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : SpecialLinearGroup R V →* V ≃ₗ[R] V

A version of Matrix.toLin' A that produces linear equivalences.

@[simp]

theorem SpecialLinearGroup.toLinearEquiv_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : SpecialLinearGroup R V) (v : V) : (toLinearEquiv A) v = (fun (x : V) => ↑A x) v

@[simp]

theorem SpecialLinearGroup.toLinearEquiv_to_linearMap {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : SpecialLinearGroup R V) : ↑(toLinearEquiv A) = ↑↑A

@[simp]

theorem SpecialLinearGroup.toLinearEquiv_symm_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : SpecialLinearGroup R V) (v : V) : (toLinearEquiv A).symm v = (fun (x : V) => ↑A⁻¹ x) v

@[simp]

theorem SpecialLinearGroup.toLinearEquiv_symm_to_linearMap {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : SpecialLinearGroup R V) : ↑(toLinearEquiv A).symm = ↑↑A⁻¹

theorem SpecialLinearGroup.toLinearEquiv_injective {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : Function.Injective ⇑toLinearEquiv

def SpecialLinearGroup.toGeneralLinearGroup {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : SpecialLinearGroup R V →* LinearMap.GeneralLinearGroup R V

The canonical group morphism from the special linear group to the general linear group.

theorem SpecialLinearGroup.toGeneralLinearGroup_toLinearEquiv_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (u : SpecialLinearGroup R V) : (toGeneralLinearGroup u).toLinearEquiv = toLinearEquiv u

theorem SpecialLinearGroup.coe_toGeneralLinearGroup_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (u : SpecialLinearGroup R V) : ↑(toGeneralLinearGroup u) = ↑(toLinearEquiv u)

theorem SpecialLinearGroup.toGeneralLinearGroup_injective {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : Function.Injective ⇑toGeneralLinearGroup

theorem SpecialLinearGroup.mem_range_toGeneralLinearGroup_iff {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {u : LinearMap.GeneralLinearGroup R V} : u ∈ Set.range ⇑toGeneralLinearGroup ↔ LinearEquiv.det u.toLinearEquiv = 1

def SpecialLinearGroup.baseChange {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {S : Type u_3} [CommRing S] [Algebra R S] [Module.Free R V] [Module.Finite R V] : SpecialLinearGroup R V →* SpecialLinearGroup S (TensorProduct R S V)

By base change, an R-algebra S induces a group homomorphism from SpecialLinearGroup R V to SpecialLinearGroup S (S ⊗[R] V).

@[simp]

theorem SpecialLinearGroup.baseChange_apply_coe {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {S : Type u_3} [CommRing S] [Algebra R S] [Module.Free R V] [Module.Finite R V] (g : SpecialLinearGroup R V) : ↑(baseChange g) = LinearEquiv.baseChange R S V V ↑g

def SpecialLinearGroup.congr_linearEquiv {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {W : Type u_3} [AddCommGroup W] [Module R W] (e : V ≃ₗ[R] W) : SpecialLinearGroup R V ≃* SpecialLinearGroup R W

The isomorphism between special linear groups of isomorphic modules.

@[simp]

theorem SpecialLinearGroup.congr_linearEquiv_coe_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {W : Type u_3} [AddCommGroup W] [Module R W] (e : V ≃ₗ[R] W) (f : SpecialLinearGroup R V) : ↑((congr_linearEquiv e) f) = e.symm ≪≫ₗ ↑f ≪≫ₗ e

@[simp]

theorem SpecialLinearGroup.congr_linearEquiv_apply_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {W : Type u_3} [AddCommGroup W] [Module R W] (e : V ≃ₗ[R] W) (f : SpecialLinearGroup R V) (x : W) : (fun (x : W) => ↑((congr_linearEquiv e) f) x) x = e ((fun (x : V) => ↑f x) (e.symm x))

theorem SpecialLinearGroup.congr_linearEquiv_symm {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {W : Type u_3} [AddCommGroup W] [Module R W] (e : V ≃ₗ[R] W) : (congr_linearEquiv e).symm = congr_linearEquiv e.symm

theorem SpecialLinearGroup.congr_linearEquiv_trans {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {W : Type u_3} {X : Type u_4} [AddCommGroup W] [Module R W] [AddCommGroup X] [Module R X] (e : V ≃ₗ[R] W) (f : W ≃ₗ[R] X) : (congr_linearEquiv e).trans (congr_linearEquiv f) = congr_linearEquiv (e ≪≫ₗ f)

theorem SpecialLinearGroup.congr_linearEquiv_refl {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : congr_linearEquiv (LinearEquiv.refl R V) = MulEquiv.refl (SpecialLinearGroup R V)

def Matrix.SpecialLinearGroup.toLin'_equiv {R : Type u_1} [CommRing R] {n : Type u_3} [Fintype n] [DecidableEq n] : SpecialLinearGroup n R ≃* _root_.SpecialLinearGroup R (n → R)

The canonical isomorphism from SL(n, R) to the special linear group of the module n → R.

noncomputable def Matrix.SpecialLinearGroup.toLin_equiv {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {n : Type u_3} [Fintype n] [DecidableEq n] (b : Module.Basis n R V) : SpecialLinearGroup n R ≃* _root_.SpecialLinearGroup R V

The isomorphism from Matrix.SpecialLinearGroup n R to the special linear group of a module associated with a basis of that module.

theorem Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {n : Type u_3} [Fintype n] [DecidableEq n] (b : Module.Basis n R V) (g : SpecialLinearGroup n R) : ↑↑((toLin_equiv b) g) = (toLin b b) ↑g

theorem Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {n : Type u_3} [Fintype n] [DecidableEq n] (b : Module.Basis n R V) (g : _root_.SpecialLinearGroup R V) : ↑((toLin_equiv b).symm g) = (LinearMap.toMatrix b b) ↑↑g

theorem SpecialLinearGroup.center_eq_bot_of_finrank_le_one {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (h : Module.finrank R V ≤ 1) : Subgroup.center (SpecialLinearGroup R V) = ⊥

theorem SpecialLinearGroup.mem_center_iff {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] {g : SpecialLinearGroup R V} : g ∈ Subgroup.center (SpecialLinearGroup R V) ↔ ∃ (r : R), r ^ Module.finrank R V = 1 ∧ ↑↑g = r • LinearMap.id

theorem SpecialLinearGroup.mem_center_iff_spec {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] {g : SpecialLinearGroup R V} (hg : g ∈ Subgroup.center (SpecialLinearGroup R V)) (x : V) : ↑↑g x = ⋯.choose • x

noncomputable def SpecialLinearGroup.centerEquivRootsOfUnity_invFun {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)) : ↥(Subgroup.center (SpecialLinearGroup R V))

The inverse map for the equivalence SpecialLinearGroup.centerEquivRootsOfUnity.

noncomputable def SpecialLinearGroup.centerEquivRootsOfUnity {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] : ↥(Subgroup.center (SpecialLinearGroup R V)) ≃* ↥(rootsOfUnity (max (Module.finrank R V) 1) R)

The isomorphism between the roots of unity and the center of the special linear group.

theorem SpecialLinearGroup.centerEquivRootsOfUnity_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (g : ↥(Subgroup.center (SpecialLinearGroup R V))) : ↑↑↑g = centerEquivRootsOfUnity g • LinearMap.id

theorem SpecialLinearGroup.centerEquivRootsOfUnity_apply_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (g : ↥(Subgroup.center (SpecialLinearGroup R V))) (x : V) : centerEquivRootsOfUnity g • x = (fun (x : V) => ↑↑g x) x

theorem rootsOfUnity.eq_one {R : Type u_1} [CommRing R] {n : ℕ} {r : ↥(rootsOfUnity n R)} (hn : n = 1) : ↑r = 1

theorem SpecialLinearGroup.centerEquivRootsOfUnity_apply_of_finrank_le_one {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (d1 : Module.finrank R V ≤ 1) (g : ↥(Subgroup.center (SpecialLinearGroup R V))) : centerEquivRootsOfUnity g = 1

theorem SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)) : ↑↑↑(centerEquivRootsOfUnity.symm r) = r • LinearMap.id

theorem SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq {R : Type u_4} [CommRing R] {V : Type u_5} [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] {ι : Type u_6} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R V) (g : ↥(Subgroup.center (Matrix.SpecialLinearGroup ι R))) : ↑(((Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)).trans centerEquivRootsOfUnity) g) = ↑(Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity g)