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.GeneralLinearGroup

Main definitions

• LinearMap.GeneralLinearGroup

@[reducible, inline]

abbrev LinearMap.GeneralLinearGroup (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Type u_2

The group of invertible linear maps from M to itself

Equations

• LinearMap.GeneralLinearGroup R M = (M →ₗ[R] M)ˣ

def LinearMap.GeneralLinearGroup.toLinearEquiv {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : GeneralLinearGroup R M) : M ≃ₗ[R] M

An invertible linear map f determines an equivalence from M to itself.

Equations

• f.toLinearEquiv = { toLinearMap := ↑f, invFun := f.inv.toFun, left_inv := ⋯, right_inv := ⋯ }

def LinearMap.GeneralLinearGroup.ofLinearEquiv {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : M ≃ₗ[R] M) : GeneralLinearGroup R M

An equivalence from M to itself determines an invertible linear map.

Equations

• LinearMap.GeneralLinearGroup.ofLinearEquiv f = { val := ↑f, inv := ↑f.symm, val_inv := ⋯, inv_val := ⋯ }

def LinearMap.GeneralLinearGroup.generalLinearEquiv (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : GeneralLinearGroup R M ≃* M ≃ₗ[R] M

The general linear group on R and M is multiplicatively equivalent to the type of linear equivalences between M and itself.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (f : GeneralLinearGroup R M) : ↑((generalLinearEquiv R M) f) = ↑f

@[simp]

theorem LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (f : GeneralLinearGroup R M) : ⇑((generalLinearEquiv R M) f) = ⇑↑f