Characters that are −1 at an involution and trivial on a subgroup

For a finite commutative group G, an element s with s² = 1 and a subgroup H, there is a character χ : G →* ℂˣ with χ s = −1 and χ trivial on H iff s ∉ H. Applied to G = (ZMod N)ˣ, s = −1: an odd character trivial on ⟨u⟩ exists iff −1 ∉ ⟨u⟩. The separation of points by characters is Mathlib's CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity.

Main results

• ConjeturaC.exists_char_neg_one_iff: the general statement.
• ConjeturaC.exists_oddChar_trivial_on_zpowers_iff: G = (ZMod N)ˣ, s = −1, H = ⟨u⟩.
• ConjeturaC.exists_oddChar_trivial_on_two_iff: the case u = 2, N odd.

References

• C. Marín, Where the character values of Sp(2m) at a torsion element fail to generate the ring of integers, Zenodo (2026), doi:10.5281/zenodo.22813216 (odd characters trivial on ⟨2⟩).

theorem ConjeturaC.units_sq_eq_one {u : ℂˣ} (hu : u ^ 2 = 1) : u = 1 ∨ u = -1

A unit of ℂ whose square is 1 is 1 or -1.

theorem ConjeturaC.exists_char_ne_one {Q : Type u_1} [CommGroup Q] [Finite Q] {a : Q} (ha : a ≠ 1) : ∃ (φ : Q →* ℂˣ), φ a ≠ 1

Characters of a finite commutative group with values in ℂˣ separate points.

theorem ConjeturaC.exists_char_neg_one_iff {G : Type u_1} [CommGroup G] [Finite G] {s : G} (hs : s ^ 2 = 1) (H : Subgroup G) : (∃ (χ : G →* ℂˣ), χ s = -1 ∧ ∀ h ∈ H, χ h = 1) ↔ s ∉ H

A character with χ s = −1 and trivial on H exists iff s ∉ H. (A hypothesis s ≠ 1 is not needed: it follows from s ∉ H, and the forward direction never uses it.)

theorem ConjeturaC.exists_oddChar_trivial_on_zpowers_iff {N : ℕ} [NeZero N] (u : (ZMod N)ˣ) : (∃ (χ : (ZMod N)ˣ →* ℂˣ), χ (-1) = -1 ∧ ∀ h ∈ Subgroup.zpowers u, χ h = 1) ↔ -1 ∉ Subgroup.zpowers u

Application: an odd character of (ZMod N)ˣ trivial on ⟨u⟩ exists iff -1 ∉ ⟨u⟩.

theorem ConjeturaC.exists_oddChar_trivial_on_two_iff {N : ℕ} [NeZero N] (hN : Nat.Coprime 2 N) : (∃ (χ : (ZMod N)ˣ →* ℂˣ), χ (-1) = -1 ∧ ∀ h ∈ Subgroup.zpowers (ZMod.unitOfCoprime 2 hN), χ h = 1) ↔ -1 ∉ Subgroup.zpowers (ZMod.unitOfCoprime 2 hN)

Concrete form for u = 2, N odd.