Invertible matrices of linear automorphisms in a basis

Mathlib identifies GL ι k with the general linear group LinearMap.GeneralLinearGroup k V of a module with a finite basis (Matrix.GeneralLinearGroup.toLin'), and that group with the linear automorphisms V ≃ₗ[k] V (LinearMap.GeneralLinearGroup.generalLinearEquiv). This file records the composite, which sends a linear automorphism to its invertible matrix in the chosen basis.

Main definitions

• Module.Basis.toGL: the group isomorphism (V ≃ₗ[k] V) ≃* GL ι k given by a basis.

Main statements

• Module.Basis.toLin'_toGL: reading the matrix back through toLin' recovers the automorphism.
• Module.Basis.coe_toGL: the matrix of f is LinearMap.toMatrix b b f, so its (i, j) entry is the i-th coordinate of f (b j).
• Module.Basis.toGL_smulOfUnit: multiplication by a unit has the scalar matrix of that unit.
• Module.Basis.finTwoProd_toGL_symm_apply: in the standard basis of R × R, an invertible 2 × 2 matrix acts by multiplication of column vectors.
• Module.Basis.fin_two_basis_generators: an invertible two-by-two change of basis has nonzero first generator and generates the whole module.

noncomputable def Module.Basis.toGL {k : Type u_1} {V : Type u_2} {ι : Type u_3} [CommRing k] [AddCommGroup V] [Module k V] [Fintype ι] [DecidableEq ι] (b : Basis ι k V) : (V ≃ₗ[k] V) ≃* GL ι k

The invertible matrix of a linear automorphism in the basis b, as a group isomorphism between the linear automorphisms of V and GL ι k.

@[simp]

theorem Module.Basis.toLin'_toGL {k : Type u_1} {V : Type u_2} {ι : Type u_3} [CommRing k] [AddCommGroup V] [Module k V] [Fintype ι] [DecidableEq ι] (b : Basis ι k V) (f : V ≃ₗ[k] V) : (Matrix.GeneralLinearGroup.toLin' b) (b.toGL f) = (LinearMap.GeneralLinearGroup.generalLinearEquiv k V).symm f

The matrix of f in the basis b acts through Matrix.GeneralLinearGroup.toLin' b as f itself.

@[simp]

theorem Module.Basis.coe_toGL {k : Type u_1} {V : Type u_2} {ι : Type u_3} [CommRing k] [AddCommGroup V] [Module k V] [Fintype ι] [DecidableEq ι] (b : Basis ι k V) (f : V ≃ₗ[k] V) : ↑(b.toGL f) = (LinearMap.toMatrix b b) ↑f

The invertible matrix of f in the basis b is its matrix LinearMap.toMatrix b b f: the (i, j) entry is the i-th coordinate of f (b j).

@[simp]

theorem Module.Basis.toGL_smulOfUnit {k : Type u_1} {V : Type u_2} {ι : Type u_3} [CommRing k] [AddCommGroup V] [Module k V] [Fintype ι] [DecidableEq ι] (b : Basis ι k V) (a : kˣ) : b.toGL (LinearEquiv.smulOfUnit a) = (Matrix.GeneralLinearGroup.scalar ι) a

Multiplication by a unit a has matrix the scalar matrix a in every basis.

@[simp]

theorem Module.Basis.finTwoProd_toGL_symm_apply {R : Type u_4} [CommRing R] (g : GL (Fin 2) R) (x y : R) : ((Basis.finTwoProd R).toGL.symm g) (x, y) = (↑g 0 0 * x + ↑g 0 1 * y, ↑g 1 0 * x + ↑g 1 1 * y)

In the standard basis of R × R, the linear automorphism of an invertible matrix g is multiplication of column vectors by g: it sends (x, y) to (g₀₀ x + g₀₁ y, g₁₀ x + g₁₁ y).

theorem Module.Basis.fin_two_basis_generators {R : Type u_4} {M : Type u_5} [CommRing R] [Nontrivial R] [AddCommGroup M] [Module R M] (b : Basis (Fin 2) R M) (γ : GL (Fin 2) R) : ↑γ 0 0 • b 0 + ↑γ 1 0 • b 1 ≠ 0 ∧ ∀ (z : M), ∃ (m : R) (n : R), m • (↑γ 0 0 • b 0 + ↑γ 1 0 • b 1) + n • (↑γ 0 1 • b 0 + ↑γ 1 1 • b 1) = z

An invertible change of a two-element basis has nonzero first generator and still generates every element over the coefficient ring.