Clifford correspondence in Lean without double cosets: a Mackey sum plus restricting intertwiners

Goal: for N ⊴ G, θ irreducible on N, and ψ, ψ' reps of I ⊇ N with ψ_N = eθ, ψ'_N = e'θ and θ^z ≇ θ for z ∉ I, prove dim Hom_G(ψ^G, ψ'^G) = dim Hom_I(ψ, ψ'). This gives irreducibility and injectivity of the Clifford correspondence together.

1. Mackey sum, using only Fintype.sum_equiv: Σ_g ind a g · ind b g⁻¹ = |G|·|I|⁻²·Σ_z Σ_g ã(g)·b̃(z g⁻¹ z⁻¹), where ã is extension by zero. Reindex g ↦ x g x⁻¹, then y ↦ y x⁻¹. 2. For z ∈ I the inner sum is |I|·dim Hom_I(ψ,ψ'), by char_conj in I. 3. For z ∉ I, let J : Subgroup I := I.comap ((MulAut.conj z).toMonoidHom.comp I.subtype). Membership unfolds definitionally to z*h*z⁻¹ ∈ I. Take φ := (c.comp J.subtype).codRestrict I (fun j ↦ j.2), A := ψ'.comp J.subtype and B := ψ.comp φ. The sum is |J|·dim Hom_J(B, A). Map N into J with (Subgroup.inclusion hNI).codRestrict J _, then restrict intertwiners: build a linear map Hom(ρ,σ) → Hom(ρ.comp f, σ.comp f) as ⟨F.toLinearMap, fun h ↦ F.isIntertwining' (f h)⟩. It is injective, so LinearMap.finrank_le_finrank_of_injective gives dim Hom_J ≤ dim Hom_N(eθ^z, e'θ) = 0. Mathlib supplies Subsingleton (IntertwiningMap ρ σ) from [IsIrreducible σ] [IsEmpty (Equiv ρ σ)].

Gotchas. Define the inertia group by character invariance, {x | ∀ n, θ.character (MulAut.conjNormal x n) = θ.character n}; then mul_mem and inv_mem are just rw with map_mul and MulAut.mul_apply. Clifford inside I needs N.subgroupOf I. Transport θ with Subgroup.subgroupOfEquivOfLe; (ψ.comp (inclusion hNI)).comp f is defeq to ψ.comp N'.subtype, so change works. Module.finrank_pos_iff_exists_ne_zero sometimes needs (M := IntertwiningMap ρ σ) given explicitly, or the Zero instances don't unify.