Mackey's irreducibility criterion in Lean: sum over elements, use H ∩ z⁻¹Hz as a comap

Mackey's formula is usually stated over double cosets HzH. Lean has no convenient API for double cosets with transversals, and you don't need one. Sum over all z ∈ G instead: |H|² · dim Hom_G(ψ^G, ψ'^G) = Σ_{z∈G} |H ∩ z⁻¹Hz| · dim Hom_{H∩z⁻¹Hz}(ψ^z, ψ'), with ψ^z(h) = ψ(z h z⁻¹). Each double coset HzH just appears |H|²/|H ∩ z⁻¹Hz| times.

Key definitions: - mackeySubgroup H z : Subgroup H := H.comap ((MulAut.conj z).toMonoidHom.comp H.subtype). Membership is definitionally z * h * z⁻¹ ∈ H, proved by Iff.rfl. - mackeyConj H z : mackeySubgroup H z →* H := (((MulAut.conj z).toMonoidHom.comp H.subtype).comp (mackeySubgroup H z).subtype).codRestrict H fun j ↦ j.2. Both live inside Subgroup H, so there is no N.subgroupOf retyping.

The proof is a character computation. Expand both induced characters, reindex g ↦ x g x⁻¹ and y ↦ y x⁻¹ (Fintype.sum_equiv). The inner sum Σ_g ψ̃'(g) ψ̃(z g⁻¹ z⁻¹) is supported on mackeySubgroup: use Finset.sum_filter_of_ne and then Finset.sum_subtype. Then card_inv_mul_sum_char_mul_char_eq_finrank finishes it.

The criterion (iff) follows in ℕ. The z ∈ H terms give |H|² · dim End ψ, and the other terms are ≥ 0. dim End ψ ≥ 1 because U is nontrivial; if U were trivial, the induced space G → U would be trivial. Use Finset.sum_eq_zero_iff, then mul_eq_zero with Nat.card_pos.

To get irreducible from dim End = 1: rewrite with IntertwiningMap.equivLinearMapAsModule, then use isSimpleModule_of_finrank_end_eq_one and irreducible_iff_isSimpleModule_asModule.