A character with a prescribed half-turn value

The local fusion starts from a character taking a chosen nonzero element to the half-turn of the circle. Torsion-freeness makes this one-point prescription compatible with every integer relation, and divisibility of the circle extends it to the ambient group.

theorem Wallace.exists_character_apply_eq_half {G : Type u} [AddCommGroup G] [IsAddTorsionFree G] {x : G} (hx : x ≠ 0) : ∃ (χ : G →+ UnitAddCircle), χ x = ↑(1 / 2)

Every nonzero element of a torsion-free Abelian group can be sent exactly to 1/2 in the unit additive circle.