The sign indicator of a subgroup

For a subgroup H of a group G, its sign indicator is the function which is 1 on H and -1 off H. This function is multiplicative exactly when the index of H divides two. For a finite quotient, this is the familiar criterion that the index is at most two.

The divisibility formulation is the unrestricted one because Mathlib defines the index of an infinite-index subgroup to be zero. It therefore excludes infinite index without an additional finiteness assumption, while the numerical bound H.index ≤ 2 does not.

This elementary character packages the last group-theoretic step in arguments where a subgroup is proved to have index two. In particular, it turns a norm subgroup of index two into the sign-valued character used to prove bimultiplicativity of the Hilbert symbol.

Main declarations

• Subgroup.signIndicator: the function equal to 1 on a subgroup and -1 off it.
• Subgroup.signIndicator_mul_iff_index_dvd_two: the unrestricted multiplicativity criterion.
• Subgroup.signIndicator_mul_iff_index_le_two: the finite-index form of the criterion.
• Subgroup.signIndicatorHom: the resulting homomorphism when the index divides two.

References

• Mathlib's Subgroup.index_dvd_two_iff and Subgroup.mul_mem_iff_of_index_two provide the index-two subgroup criteria used to prove multiplicativity.

noncomputable def Subgroup.signIndicator {G : Type u_1} [Group G] (H : Subgroup G) (x : G) : ℤˣ

The sign indicator of a subgroup: it is 1 on the subgroup and -1 off it.

Equations

• H.signIndicator x = (↑H)ᶜ.mulIndicator (fun (x : G) => -1) x

@[simp]

theorem Subgroup.signIndicator_of_mem {G : Type u_1} [Group G] (H : Subgroup G) {x : G} (hx : x ∈ H) : H.signIndicator x = 1

The sign indicator is 1 on its subgroup.

@[simp]

theorem Subgroup.signIndicator_of_notMem {G : Type u_1} [Group G] (H : Subgroup G) {x : G} (hx : x ∉ H) : H.signIndicator x = -1

The sign indicator is -1 outside its subgroup.

@[simp]

theorem Subgroup.signIndicator_eq_one_iff {G : Type u_1} [Group G] (H : Subgroup G) {x : G} : H.signIndicator x = 1 ↔ x ∈ H

The sign indicator detects membership by taking the value 1.

@[simp]

theorem Subgroup.signIndicator_eq_neg_one_iff {G : Type u_1} [Group G] (H : Subgroup G) {x : G} : H.signIndicator x = -1 ↔ x ∉ H

The sign indicator detects nonmembership by taking the value -1.

theorem Subgroup.signIndicator_mul_iff_index_dvd_two {G : Type u_1} [Group G] (H : Subgroup G) : (∀ (x y : G), H.signIndicator (x * y) = H.signIndicator x * H.signIndicator y) ↔ H.index ∣ 2

The sign indicator is multiplicative exactly when the subgroup index divides two.

This is the version without a finiteness assumption. The divisibility condition is essential: Mathlib records an infinite index as zero, which satisfies H.index ≤ 2 but does not divide two.

theorem Subgroup.signIndicator_mul_iff_index_le_two {G : Type u_1} [Group G] (H : Subgroup G) [H.FiniteIndex] : (∀ (x y : G), H.signIndicator (x * y) = H.signIndicator x * H.signIndicator y) ↔ H.index ≤ 2

For a subgroup with finite quotient, the sign indicator is multiplicative exactly when the subgroup has index at most two.

noncomputable def Subgroup.signIndicatorHom {G : Type u_1} [Group G] (H : Subgroup G) (hindex : H.index ∣ 2) : G →* ℤˣ

The sign indicator, bundled as a homomorphism when the subgroup index divides two.

Equations

• H.signIndicatorHom hindex = { toFun := H.signIndicator, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Subgroup.signIndicatorHom_apply {G : Type u_1} [Group G] (H : Subgroup G) (hindex : H.index ∣ 2) (x : G) : (H.signIndicatorHom hindex) x = H.signIndicator x

The bundled sign-indicator homomorphism evaluates to the underlying sign indicator.

@[simp]

theorem Subgroup.ker_signIndicatorHom {G : Type u_1} [Group G] (H : Subgroup G) (hindex : H.index ∣ 2) : (H.signIndicatorHom hindex).ker = H

The kernel of the sign-indicator homomorphism is the original subgroup.

theorem Subgroup.signIndicatorHom_surjective_iff {G : Type u_1} [Group G] (H : Subgroup G) (hindex : H.index ∣ 2) : Function.Surjective ⇑(H.signIndicatorHom hindex) ↔ H ≠ ⊤

The sign-indicator homomorphism is onto precisely when the subgroup is proper.

theorem Subgroup.signIndicatorHom_surjective_iff_index_eq_two {G : Type u_1} [Group G] (H : Subgroup G) (hindex : H.index ∣ 2) : Function.Surjective ⇑(H.signIndicatorHom hindex) ↔ H.index = 2

The sign-indicator homomorphism is onto precisely for a subgroup of index two.