map from prod_v K_v to prod_w L_w

[kbuzzard]

If L/K is a finite separable extension of fields of fractions of Dedekind domains B/A, with B the integral closure of A in L, then the K-algebra morphisms (which we have) from K_v to L_w of w|v give rise to a K-algebra morphism from prod_v K_v to prod_w L_w. This should be easy, but there's a catch; the definition of the map from K_v to L_w is in the process of being refactored in #229 so we should probably wait until the refactor hits main.

[kbuzzard]

Status: currently blocked on #229

[maddycrim]

claim

[maddycrim]

propose #270