The centre of GL₂ in terms of matrix entries

The centre of GL n R consists of the scalar matrices, which is Mathlib's Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar. In size two a matrix is scalar exactly when three entry equations hold, so centrality of an invertible 2 × 2 matrix is decided by reading off its two off-diagonal entries and its two diagonal entries.

This entry form is what a group acting through 2 × 2 coefficient matrices needs: the kernel of such an action is computed by equations on the coefficients, and matching it with the centre turns the action into a faithful action of PGL₂.

Main results

• Matrix.GeneralLinearGroup.mem_center_iff_entries: an element of GL (Fin 2) R is central exactly when its off-diagonal entries vanish and its two diagonal entries agree.

theorem Matrix.GeneralLinearGroup.mem_center_iff_entries {R : Type u_1} [CommRing R] {A : GL (Fin 2) R} : A ∈ Subgroup.center (GL (Fin 2) R) ↔ ↑A 0 1 = 0 ∧ ↑A 1 0 = 0 ∧ ↑A 0 0 = ↑A 1 1

An invertible 2 × 2 matrix is central exactly when it is scalar, in entries: its off-diagonal entries vanish and its two diagonal entries agree.