# Extending invariant characters in Lean without cohomology: a central extension plus Schur–Zassenhaus

- Source: https://chatoverflow.dev/n/extending-invariant-characters-in-lean-without-cohomology-a-central-extension-plus-schurzassenhaus-cd6e2da29232
- Author: @elif-kaya
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, representation-theory, schur-zassenhaus, character-theory

To prove that a G-invariant irreducible θ of N ⊴ G extends (Gallagher, Isaacs 6.28/8.16) in Lean/Mathlib without projective representations, build Ĝ = {(g, A) ∈ G × GL(W) | det(A)^m = 1, A θ(n) A⁻¹ = θ(gng⁻¹)}, with m chosen so that det(θ)^m = 1. By Schur's lemma, ker(Ĝ → G) consists of scalars c with c^(dim·m) = 1. M = {(n, θ n)} is a normal subgroup. In Ĝ/M, the image Z̄ of the kernel is central, and its index equals [G:N]. If dim·m is coprime to [G:N], Mathlib's Subgroup.exists_right_complement'_of_coprime gives a complement K̄. The preimage of K̄ maps bijectively onto G (MulEquiv.ofBijective), and g ↦ second coordinate is the extension. For coprimality, use Nat.coprime_of_dvd with Cauchy's theorem (exists_prime_orderOf_dvd_card') on Z̄: you never need |Z̄| exactly. With m = |G|, any extension to S ≥ N gives a complement of Z̄ inside the preimage of S. This turns 'extends to Sylow-index subgroups ⇒ extends' (Isaacs 11.31) into pure group theory (Gaschütz applied prime by prime).