Mathlib.LinearAlgebra.GeneralLinearGroup

Module docstring

{"# 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.

Main definitions

LinearMap.GeneralLinearGroup

LinearMap.GeneralLinearGroup abbrev

Full source

/-- The group of invertible linear maps from `M` to itself -/
abbrev GeneralLinearGroup :=
  (M →ₗ[R] M)ˣ

General Linear Group of Linear Maps

Informal description

The general linear group over a ring $R$ acting on a module $M$ is the group of invertible $R$-linear maps from $M$ to itself, denoted by $\mathrm{GL}(R, M)$.

LinearMap.GeneralLinearGroup.toLinearEquiv definition

(f : GeneralLinearGroup R M) : M ≃ₗ[R] M

Full source

/-- An invertible linear map `f` determines an equivalence from `M` to itself. -/
def toLinearEquiv (f : GeneralLinearGroup R M) : M ≃ₗ[R] M :=
  { f.val with
    invFun := f.inv.toFun
    left_inv := fun m ↦ show (f.inv * f.val) m = m by rw [f.inv_val]; simp
    right_inv := fun m ↦ show (f.val * f.inv) m = m by rw [f.val_inv]; simp }

Linear equivalence from general linear group element

Informal description

Given an element $ f $ of the general linear group $\mathrm{GL}(R, M)$, this function constructs a linear equivalence $ M \simeq_{R} M $ from $ f $, where the inverse function is given by the inverse of $ f $ in the general linear group, and the left and right inverse properties are satisfied.

LinearMap.GeneralLinearGroup.ofLinearEquiv definition

(f : M ≃ₗ[R] M) : GeneralLinearGroup R M

Full source

/-- An equivalence from `M` to itself determines an invertible linear map. -/
def ofLinearEquiv (f : M ≃ₗ[R] M) : GeneralLinearGroup R M where
  val := f
  inv := (f.symm : M →ₗ[R] M)
  val_inv := LinearMap.ext fun _ ↦ f.apply_symm_apply _
  inv_val := LinearMap.ext fun _ ↦ f.symm_apply_apply _

Construction of general linear group element from linear equivalence

Informal description

Given a linear equivalence $ f : M \simeq_{R} M $, this function constructs an element of the general linear group $\mathrm{GL}(R, M)$ by packaging $ f $ and its inverse $ f^{-1} $ together with proofs that they are mutual inverses.

LinearMap.GeneralLinearGroup.generalLinearEquiv definition

: GeneralLinearGroup R M ≃* M ≃ₗ[R] M

Full source

/-- The general linear group on `R` and `M` is multiplicatively equivalent to the type of linear
equivalences between `M` and itself. -/
def generalLinearEquiv : GeneralLinearGroupGeneralLinearGroup R M ≃* M ≃ₗ[R] M where
  toFun := toLinearEquiv
  invFun := ofLinearEquiv
  left_inv f := by ext; rfl
  right_inv f := by ext; rfl
  map_mul' x y := by ext; rfl

Multiplicative equivalence between general linear group and linear equivalences

Informal description

The multiplicative equivalence between the general linear group $\mathrm{GL}(R, M)$ and the type of linear equivalences $M \simeq_{R} M$. Specifically, the function `toLinearEquiv` maps an element of $\mathrm{GL}(R, M)$ to its corresponding linear equivalence, while the function `ofLinearEquiv` constructs an element of $\mathrm{GL}(R, M)$ from a linear equivalence. This equivalence preserves the multiplicative structure, meaning that the product of two elements in $\mathrm{GL}(R, M)$ corresponds to the composition of their respective linear equivalences.

LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap theorem

(f : GeneralLinearGroup R M) : (generalLinearEquiv R M f : M →ₗ[R] M) = f

Full source

@[simp]
theorem generalLinearEquiv_to_linearMap (f : GeneralLinearGroup R M) :
    (generalLinearEquiv R M f : M →ₗ[R] M) = f := by ext; rfl

Correspondence between general linear group elements and their linear maps

Informal description

For any element $f$ in the general linear group $\mathrm{GL}(R, M)$, the underlying linear map of the corresponding linear equivalence (via `generalLinearEquiv`) is equal to $f$ itself. That is, if we consider $f$ as a linear map $M \to M$, this coincides with the linear map obtained from the linear equivalence corresponding to $f$.

LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv theorem

(f : GeneralLinearGroup R M) : (generalLinearEquiv R M f) = (f : M → M)

Full source

@[simp]
theorem coeFn_generalLinearEquiv (f : GeneralLinearGroup R M) :
    (generalLinearEquiv R M f) = (f : M → M) := rfl

Equality of General Linear Group Element and Its Linear Equivalence as Functions

Informal description

For any element $f$ in the general linear group $\mathrm{GL}(R, M)$, the linear equivalence obtained via the `generalLinearEquiv` map is equal to $f$ when both are viewed as functions from $M$ to $M$.