English
There is a natural bijection between GL_n(F) and the set of n vectors in F^n that are linearly independent; it sends a matrix to its column vectors.
Русский
Существует естественная биекция между GL_n(F) и множеством из n векторов в F^n, которые линейно независимы; матрица отправляется в векторы её столбцов.
LaTeX
$$GL_n(F) ≃ { s : Fin n → Fin n → F // LinearIndependent F s }$$
Lean4
/-- Equivalence between `GL n F` and `n` vectors of length `n` that are linearly independent. Given
by sending a matrix to its columns. -/
noncomputable def equiv_GL_linearindependent : GL (Fin n) 𝔽 ≃ { s : Fin n → Fin n → 𝔽 // LinearIndependent 𝔽 s }
where
toFun
M :=
⟨M.1.col, by
apply linearIndependent_iff_card_eq_finrank_span.2
rw [Set.finrank, ← rank_eq_finrank_span_cols, rank_unit]⟩
invFun
M :=
GeneralLinearGroup.mk'' (transpose (M.1)) <| by
classical
let b := basisOfPiSpaceOfLinearIndependent M.2
have := (Pi.basisFun 𝔽 (Fin n)).invertibleToMatrix b
rw [← Basis.coePiBasisFun.toMatrix_eq_transpose, ← coe_basisOfPiSpaceOfLinearIndependent M.2]
exact isUnit_det_of_invertible _
right_inv := by exact congrFun rfl
