Historically (as I gather from Learning Class Field Theory: Local or Global First?), global class field theory was proved first, and then used to deduce local class field theory. But nowadays most treatments do the local theory first.
Can someone give me a summary of how the global-to-local argument goes, or a reference to where the argument appears?
I'm interested in seeing this as a toy model for how to think about the current state of Langlands, where it's still the case that many local statements (e.g. local Langlands for $GL_n$) are proved via global methods.
I think these proofs start off by globalizing the local situation, getting a corresponding global object on the other side, and then extracting a local component. The issue is then showing that this construction doesn't depend on the globalization. Can you prove local class field theory along these lines?