Brauer's First Main Theorem

F3 makes the displayed assignment a function with the stated codomain. F2 makes it injective, and F1 makes it onto. These are precisely the two bijection conditions, including if either set is empty: F1 and F3 then force the other to be empty as well.

For $g\in G$, conjugation carries $N_G(D)$ to $N_G(gD{g}^{-1})$, sends a block ideal to the conjugate ideal, and transports the double-group action and every split inclusion/retraction by the algebra isomorphism $x\mapsto gx{g}^{-1}$. A diagonal vertex $\mathrm{\Delta }D$ is carried to $\mathrm{\Delta }(gD{g}^{-1})$, since relative induction splittings and subgroup minimality are transported in both directions. Thus conjugating the summand condition defining $b^G$ gives $({}^{g}b{)}^G={}^g(b^G)$ by uniqueness. If $N=G$, restriction to the same double group is identity and each block is its own unique inducing block, so the bijection is identity. In particular $D=1$ gives the identity on defect-zero blocks. This proves equivariance and all boundaries; no preferred representative of a conjugacy class is chosen. F1–F3 are choice-free and the present maps are explicit, so no AC is required.