Previous work in the file FLT.DedekindDomain.FiniteAdeleRing.BaseChange gives maps K_v -> L_w on completions of fields of fractions of Dedekind domains at maximal ideals. The product of such maps should give us a K-algebra homomorphism from prod_v K_v to prod_w L_w. I've mis-stated this claim in the declaration ProdAdicCompletions.baseChange because I've acidentally made it a K-module map rather than a K-algebra map. The sorries in the latter declaration should be straightforward but what really should be done is that my error should be fixed and this declaration should be beefed up to a K-algebra map; this should also hopefully be easy for someone who knows the algebra API.
maddycrim
commented
1 week ago
Previous work in the file
FLT.DedekindDomain.FiniteAdeleRing.BaseChangegives maps K_v -> L_w on completions of fields of fractions of Dedekind domains at maximal ideals. The product of such maps should give us a K-algebra homomorphism from prod_v K_v to prod_w L_w. I've mis-stated this claim in the declarationProdAdicCompletions.baseChangebecause I've acidentally made it a K-module map rather than a K-algebra map. The sorries in the latter declaration should be straightforward but what really should be done is that my error should be fixed and this declaration should be beefed up to a K-algebra map; this should also hopefully be easy for someone who knows the algebra API.