The order of the projective general linear group

The projective general linear group PGL(n, R) is the quotient of GL n R by its centre, and for n nonempty that centre is a copy of the unit group Rˣ, embedded as the scalar matrices. So |PGL(n, R)| · |Rˣ| = |GL n R|, the projective counterpart of Mathlib's Matrix.card_SL_mul_card_units. Over a finite field 𝔽_q this gives |PGL(n, 𝔽_q)| = ∏ i, (qⁿ - qⁱ) / (q - 1), and in size two |PGL(2, 𝔽_q)| = q³ - q.

Main results

• Matrix.ProjGenLinGroup.instFinite: PGL(n, R) is finite when R is.
• Matrix.GeneralLinearGroup.card_center: for nonempty n the centre of GL n R has order |Rˣ|.
• Matrix.card_PGL_mul_card_units: |PGL(n, R)| · |Rˣ| = |GL n R| for nonempty n.
• Matrix.card_PGL: |PGL(n, R)| = |GL n R| / |Rˣ| when R has finitely many units.
• Matrix.card_PGL_field: |PGL(n, 𝔽_q)| = ∏ i, (qⁿ - qⁱ) / (q - 1).
• TauCeti.natCard_PGL_fin_two: |PGL(2, 𝔽_q)| = q³ - q.

instance Matrix.ProjGenLinGroup.instFinite {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] [Finite R] : Finite (ProjGenLinGroup n R)

The projective general linear group over a finite ring is finite.

theorem Matrix.GeneralLinearGroup.card_center {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] [Nonempty n] : Nat.card ↥(Subgroup.center (GL n R)) = Nat.card Rˣ

For nonempty n, the centre of GL n R has as many elements as Rˣ: it is the image of the injective scalar embedding.

theorem Matrix.card_PGL_mul_card_units {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] [Nonempty n] : Nat.card (ProjGenLinGroup n R) * Nat.card Rˣ = Nat.card (GL n R)

The order of PGL(n, R) times the number of units is the order of GL n R, for nonempty n.

theorem Matrix.card_PGL {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] [Nonempty n] [Finite Rˣ] : Nat.card (ProjGenLinGroup n R) = Nat.card (GL n R) / Nat.card Rˣ

The order of the projective general linear group over a commutative ring with finitely many units.

theorem Matrix.card_PGL_field {𝔽 : Type u_1} [Field 𝔽] [Fintype 𝔽] (n : ℕ) [NeZero n] : Nat.card (ProjGenLinGroup (Fin n) 𝔽) = (∏ i : Fin n, (Fintype.card 𝔽 ^ n - Fintype.card 𝔽 ^ ↑i)) / (Fintype.card 𝔽 - 1)

The order of the projective general linear group over a finite field: |PGL(n, 𝔽_q)| = ∏ i, (qⁿ - qⁱ) / (q - 1).

theorem TauCeti.natCard_PGL_fin_two (F : Type u_1) [Field F] [Fintype F] : Nat.card (Matrix.ProjGenLinGroup (Fin 2) F) = Fintype.card F ^ 3 - Fintype.card F

The order of PGL(2, 𝔽_q) is q³ - q.