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 := ⋯ }

@[simp]

theorem LinearMap.GeneralLinearGroup.coe_toLinearEquiv {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : GeneralLinearGroup R M) : ⇑f.toLinearEquiv = ⇑↑f

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 := ⋯ }

@[simp]

theorem LinearMap.GeneralLinearGroup.coe_ofLinearEquiv {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : M ≃ₗ[R] M) : ⇑↑(ofLinearEquiv f) = ⇑f

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

def LinearMap.GeneralLinearGroup.congrLinearEquiv {R₁ : Type u_3} {R₂ : Type u_4} {M₁ : Type u_6} {M₂ : Type u_7} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) : GeneralLinearGroup R₁ M₁ ≃* GeneralLinearGroup R₂ M₂

A semilinear equivalence from V to W determines an isomorphism of general linear groups.

Equations

• LinearMap.GeneralLinearGroup.congrLinearEquiv e₁₂ = Units.mapEquiv e₁₂.conjRingEquiv.toMulEquiv

@[simp]

theorem LinearMap.GeneralLinearGroup.congrLinearEquiv_apply {R₁ : Type u_3} {R₂ : Type u_4} {M₁ : Type u_6} {M₂ : Type u_7} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (g : GeneralLinearGroup R₁ M₁) : (congrLinearEquiv e₁₂) g = ofLinearEquiv (e₁₂.symm.trans (g.toLinearEquiv.trans e₁₂))

@[simp]

theorem LinearMap.GeneralLinearGroup.congrLinearEquiv_symm {R₁ : Type u_3} {R₂ : Type u_4} {M₁ : Type u_6} {M₂ : Type u_7} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) : (congrLinearEquiv e₁₂).symm = congrLinearEquiv e₁₂.symm

@[simp]

theorem LinearMap.GeneralLinearGroup.congrLinearEquiv_trans {R : Type u_1} [Semiring R] {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R N₁] [Module R N₂] [Module R N₃] (e₁₂ : N₁ ≃ₗ[R] N₂) (e₂₃ : N₂ ≃ₗ[R] N₃) : (congrLinearEquiv e₁₂).trans (congrLinearEquiv e₂₃) = congrLinearEquiv (e₁₂ ≪≫ₗ e₂₃)

theorem LinearMap.GeneralLinearGroup.congrLinearEquiv_trans' {R₁ : Type u_3} {R₂ : Type u_4} {R₃ : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomInvPair σ₃₁ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) : (congrLinearEquiv e₁₂).trans (congrLinearEquiv e₂₃) = congrLinearEquiv (e₁₂.trans e₂₃)

Stronger form of congrLinearEquiv.trans applying to semilinear maps. Not a simp lemma as σ₁₃ and σ₃₁ cannot be inferred from the LHS.

@[simp]

theorem LinearMap.GeneralLinearGroup.congrLinearEquiv_refl {R₁ : Type u_3} {M₁ : Type u_6} [Semiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] : congrLinearEquiv (LinearEquiv.refl R₁ M₁) = MulEquiv.refl (GeneralLinearGroup R₁ M₁)