correspondence between finite abelian extensions and congruence subgroups I make self-study in class field theory  and I want to prove the following popular fact: 
Given a modulus $\mathfrak{m}$ of a number field $K$, the map $L\mapsto ker (\phi_{L/K,\mathfrak{m}}$) is an inclusion-reversing bijection between the set of finite abelian extensions of $K$ that admit $\mathfrak{m}$ and the set of congruence subgroups for $\mathfrak{m}$.  
An extension $L/K$ admits $\mathfrak{m}$ iff  $\mathfrak{m}$ is divisible by all primes that ramify in $L$ and $ker(\phi_{L/K,\mathfrak{m}})$ is congruence subgroup where $\phi_{L/K,\mathfrak{m}}$ is the Artin map.
As a result of Takagi existence theorem, the map is surjective. But I have problem about injectivity and inclusion-reserving. 
 A: I am studying this myself at the moment and do not have too much experience with class field theory, but this is how I understand things work:
For the inclusion reversing, note that if $L, L'$ are abelian extensions of $K$ and $L \subset L'$ then $\phi_{L/K}$ is the restriction of $\phi_{L'/K}$ to $L$ (at the primes where they are both defined). This implies that $ker(\phi_{L'/K}) \subset ker(\phi_{L/K})$. 
You can also see this the other way around. If $ker(\phi_{L'/K}) \subset ker(\phi_{L/K})$ then the primes of $K$ that split completely in $L'$ form a subset of those that split in $L$. Hence $L \subset L'$. 
For the injectivity to hold we need to put an equivalence relation on the set of congruence subgroups. For $i=1,2$, let $\mathfrak{m}_i$ be a modulus of $K$ and let $H_i$ be a congruence subgroup modulo $\mathfrak{m}_i$. We say $H_1$ and $H_2$ are equivalent if there is a modulus $\mathfrak{m}$ such that $H_1 \cap I_K^\mathfrak{m} = H_2 \cap I_K^\mathfrak{m}$. It is easy to check that this indeed gives an equivalence relation. Actually we may even assume that $\mathfrak{m}$ is divisible by both $\mathfrak{m}_i$. 
With the equivalence relation defined like this, your map gives an inclusion reversing bijection between abelian extensions of $K$ and equivalence classes of congruence subgroups. For a proof see for example Algebraic Number Fields by Gerald Janusz.
