Upper ramification groups commute with quotients (source code)

= Upper ramification groups commute with quotients
{title2=$(G/H)^u=G^uH/H$}

For a normal subgroup $H$ of a finite local <Galois group>, the <upper ramification numbering> on its quotient is obtained by projecting the upper groups. The <Herbrand function> is the change of variable that ensures this compatibility. In contrast, the <lower ramification numbering> restricts directly to subgroups.