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.
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.