Invertible_Matrix_corresponds_to_Automorphism

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Invertible_Matrix_corresponds_to_Automorphism is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Let $R$ be a ring with unity. Let $n \in \Z_{>0}$ be a (strictly) positive integer. Let $G$ be an $n$-dimensional $R$-module. Let $\map {\mathcal M_R} n$ be the $n \times n$ matrix space over $R$. Let $\map {\mathcal L_R} G$ be the set of all linear operators on $G$. Then the invertible elements of the ring of square matrices $\struct {\map {\mathcal M_R} n, +, \times}$ correspond directly to automorphisms of $\map {\mathcal L_R} G$.

Why this node was retired

The posted statement is

theorem Invertible_Matrix_corresponds_to_Automorphism {R : Type _} [CommRing R] (n : ℕ) (A : Matrix (Fin n) (Fin n) R) (hA : IsUnit A) : ∃ (phi : (Fin n → R) ≃ₗ[R] (Fin n → R)), True := by sorry

The goal is ∃ (phi : (Fin n → R) ≃ₗ[R] (Fin n → R)), True, which is witnessed by the identity map. The matrix A and its invertibility hypothesis hA play no part in the conclusion, so no correspondence between A and phi is asserted.

What a faithful statement would require

The conclusion must state that the linear map Matrix.toLin' A is an isomorphism, i.e. tie phi to A by phi = Matrix.toLin' A or an equivalent identification.

No corrected replacement node exists yet.