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 #
@[reducible]
def
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
Instances For
def
LinearMap.GeneralLinearGroup.toLinearEquiv
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(f : LinearMap.GeneralLinearGroup R M)
:
An invertible linear map f
determines an equivalence from M
to itself.
Instances For
def
LinearMap.GeneralLinearGroup.ofLinearEquiv
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(f : M ≃ₗ[R] M)
:
An equivalence from M
to itself determines an invertible linear map.
Instances For
def
LinearMap.GeneralLinearGroup.generalLinearEquiv
(R : Type u_1)
(M : Type u_2)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
LinearMap.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.
Instances For
@[simp]
theorem
LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap
(R : Type u_1)
(M : Type u_2)
[Semiring R]
[AddCommMonoid M]
[Module R M]
(f : LinearMap.GeneralLinearGroup R M)
:
↑(↑(LinearMap.GeneralLinearGroup.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 : LinearMap.GeneralLinearGroup R M)
:
↑(↑(LinearMap.GeneralLinearGroup.generalLinearEquiv R M) f) = ↑↑f