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.