Post #4352790

@highergeometer@mathstodon.xyz Ha ha :-) But this was 2017, before my eyes had been opened. In fact it was later that year, when I failed to apply a lemma about R[1/fg] to R[1/f][1/g] when translating a Stacks Project lemma into Lean, that the penny dropped. Conversely I claim that the convention is a great one when you're not formalising mathematics 🙂 Interestingly, I have seen both normalisations of that "=" used in the literature. If p is a prime not dividing N then there's an unambiguous p on the right hand side, and there's an ambiguous p on the left hand side: you either use the "arithmetic Frobenius" or the "geometric Frobenius". The notation for both of these is "Frob_p" and one is the inverse of the other. Arithmetic Frobenius sends a root of unity z in Q(zeta_n) to z^p. The canonical isomorphism of course sends the unambiguous p on the right hand side to...one of the Frobeniuses. Geometric Frobenius exists because people (Deligne?) were annoyed about how arithmetic Frobenius acted on etale cohomology -- there were too many - signs in the theorems. But if you're interested in Heegner points and Tate modules then there are too many - signs with the geometric convention. So there are always arguments for both conventions. Maybe they're both canonical? 🙂