Two-sided invertible equivalence of matrices

Matrices related by L * A * R with L and R invertible. Rows and columns are transformed independently, so the two index types are separate, and nothing here needs more than a semiring.

Main results

• Matrix.GeneralLinearGroup.inv_mul_mul_inv_of_mul_mul_eq: inverting a two-sided invertible transformation.
• Equiv.reindexGL: reindexing the rows and columns of a general linear group along an equivalence of index types, with Equiv.reindexGL_refl and Equiv.reindexGL_symm.

theorem Matrix.GeneralLinearGroup.inv_mul_mul_inv_of_mul_mul_eq {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {S : Type u_3} [Semiring S] {A B : Matrix ι κ S} (L : GL ι S) (R : GL κ S) (h : ↑L * A * ↑R = B) : ↑L⁻¹ * B * ↑R⁻¹ = A

Inverting a two-sided invertible transformation. The rows and columns are transformed independently, so they need not share an index type.

def Equiv.reindexGL {n : Type u_1} {p : Type u_2} [Fintype n] [DecidableEq n] [Fintype p] [DecidableEq p] (e : n ≃ p) (R : Type u) [CommSemiring R] : GL n R ≃* GL p R

Reindexing along an equivalence of index types, as a group isomorphism of general linear groups.

Equations

• e.reindexGL R = Units.mapEquiv (Matrix.reindexAlgEquiv R R e).toRingEquiv.toMulEquiv

@[simp]

theorem Equiv.coe_reindexGL {n : Type u_1} {p : Type u_2} [Fintype n] [DecidableEq n] [Fintype p] [DecidableEq p] (e : n ≃ p) (R : Type u) [CommSemiring R] (M : GL n R) : ↑((e.reindexGL R) M) = (↑M).submatrix ⇑e.symm ⇑e.symm

@[simp]

theorem Equiv.reindexGL_refl {n : Type u_1} [Fintype n] [DecidableEq n] (R : Type u) [CommSemiring R] : (Equiv.refl n).reindexGL R = MulEquiv.refl (GL n R)

Reindexing along the identity equivalence is the identity.

theorem Equiv.reindexGL_symm {n : Type u_1} {p : Type u_2} [Fintype n] [DecidableEq n] [Fintype p] [DecidableEq p] (e : n ≃ p) (R : Type u) [CommSemiring R] : e.symm.reindexGL R = (e.reindexGL R).symm

Reindexing along the inverse equivalence is the inverse isomorphism.