The general linear group of linear maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
@[reducible]
def
linear_map.general_linear_group
(R : Type u_1)
(M : Type u_2)
[semiring R]
[add_comm_monoid M]
[module R M] :
Type u_2
The group of invertible linear maps from M to itself
Equations
- linear_map.general_linear_group R M = (M →ₗ[R] M)ˣ
@[protected, instance]
def
linear_map.general_linear_group.has_coe_to_fun
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M] :
has_coe_to_fun (linear_map.general_linear_group R M) (λ (_x : linear_map.general_linear_group R M), M → M)
def
linear_map.general_linear_group.to_linear_equiv
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(f : linear_map.general_linear_group R M) :
An invertible linear map f determines an equivalence from M to itself.
def
linear_map.general_linear_group.of_linear_equiv
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(f : M ≃ₗ[R] M) :
An equivalence from M to itself determines an invertible linear map.
def
linear_map.general_linear_group.general_linear_equiv
(R : Type u_1)
(M : Type u_2)
[semiring R]
[add_comm_monoid M]
[module R M] :
linear_map.general_linear_group 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
- linear_map.general_linear_group.general_linear_equiv R M = {to_fun := linear_map.general_linear_group.to_linear_equiv _inst_3, inv_fun := linear_map.general_linear_group.of_linear_equiv _inst_3, left_inv := _, right_inv := _, map_mul' := _}
@[simp]
theorem
linear_map.general_linear_group.general_linear_equiv_to_linear_map
(R : Type u_1)
(M : Type u_2)
[semiring R]
[add_comm_monoid M]
[module R M]
(f : linear_map.general_linear_group R M) :
@[simp]
theorem
linear_map.general_linear_group.coe_fn_general_linear_equiv
(R : Type u_1)
(M : Type u_2)
[semiring R]
[add_comm_monoid M]
[module R M]
(f : linear_map.general_linear_group R M) :