English
For every unit u ∈ ℤˣ, define toSubgroup(u) to be A when u = 1 and B when u ≠ 1. This encodes which subgroup governs the relation t^u a = φ_u(a) t^u.
Русский
Для каждого элемента u ∈ ℤˣ определить toSubgroup(u) равным A, если u = 1, и B — если u ≠ 1. Это задание указывает, какая подгруппа задаёт отношение t^u a = φ_u(a) t^u.
LaTeX
$$$\\mathrm toSubgroup(u) = \\begin{cases} A, & u = 1, \\\\ B, & u ≠ 1. \\end{cases}$$$
Lean4
/-- To avoid duplicating code, we define `toSubgroup A B u` and `toSubgroupEquiv u`
where `u : ℤˣ` is `1` or `-1`. `toSubgroup A B u` is `A` when `u = 1` and `B` when `u = -1`,
and `toSubgroupEquiv` is `φ` when `u = 1` and `φ⁻¹` when `u = -1`. `toSubgroup u` is the subgroup
such that for any `a ∈ toSubgroup u`, `t ^ (u : ℤ) * a = toSubgroupEquiv a * t ^ (u : ℤ)`. -/
def toSubgroup (u : ℤˣ) : Subgroup G :=
if u = 1 then A else B
