beef up a ring homomorphism to an algebra homomorphism

[kbuzzard]

The completion machinery works for ring homomorphisms but not for algebra homomorphisms (as far as I know). We use it to complete the ring homomorphism K -> L to a ring homomorphism K_v -> L_w. But we need that this is a K-algebra homomorphism. The sorry in adicCompletion_comap_algHom in the file FLT.DedekindDomain.FiniteAdeleRing.BaseChange is data, but the data is all created in adicCompletion_comap_ringHom, and the claim about it being an algebra hom is just a claim about how the map commutes with the K-action.

[WilliamCoram]

claim

[WilliamCoram]

propose #218