Permutation homomorphisms lift through modular reduction (source code)

= Permutation homomorphisms lift through modular reduction

For coset <permutation modules>, <Mackey restriction formula> and <Frobenius reciprocity> identify the <homomorphism> space with a <free module> having one orbit-sum basis vector per double coset. The same basis works over the residue field, so reduction of <homomorphisms> is surjective. Applied to <endomorphisms> of a permutation <module>, <idempotent refinement theorem> lifts each modular direct summand to a trivial source lattice. Lifting inverse <isomorphisms> between reductions shows uniqueness among trivial source lattices.