frobenius_kernel_isNormal.toml

id = "frobenius_kernel_isNormal"
title = "Frobenius's theorem: the Frobenius kernel is normal"
test = false
module = "LeanEval.GroupTheory.Frobenius"
holes = ["frobenius_kernel_isNormal"]
submitter = "Kim Morrison"
notes = "For a Frobenius group G acting transitively and faithfully on X with |X| ≥ 2, non-trivial point stabilisers, and the Frobenius condition (no non-identity element fixes more than one point), the set {1} ∪ {g | g fixes no point} is a normal subgroup. The only known proof uses Frobenius's induction-of-characters argument; no purely group-theoretic proof has been found in over a century."
source = "G. Frobenius, Über auflösbare Gruppen IV, Sitzungsber. Akad. Wiss. Berlin (1901)."
informal_solution = "Let H = stabilizer(x₀). Construct a class function θ on H of the form (1_H minus restriction of certain induced characters), and apply Frobenius reciprocity to lift θ to a generalised character of G whose kernel is exactly the Frobenius kernel K. The fact that the lift remains a virtual character (i.e. integer-valued combination of irreducibles) is exactly the content; that K is then a subgroup follows from K being a kernel."