Index three from three covering cosets

Let H be a subgroup of a group G. If some g has g² ∉ H and every element of G lies in one of the left cosets H, g H and g⁻¹ H, then H has index three: the hypothesis g² ∉ H rules out each coincidence H = g H, H = g⁻¹ H and g H = g⁻¹ H, so the classes of 1, g and g⁻¹ enumerate G ⧸ H without repetition.

For example, at Tate's reduction symbol IV* the points of an elliptic curve with singular reduction fall into two classes, one for each root of a residue quadratic, and negation exchanges the classes. So if some point has singular reduction, the subgroup of points with nonsingular reduction has index three; otherwise it is the whole group.

Main results

• Subgroup.index_eq_three_of_sq_notMem and AddSubgroup.index_eq_three_of_two_nsmul_notMem: if g² ∉ H and every element lies in H, g H or g⁻¹ H, then H.index = 3.

theorem Subgroup.index_eq_three_of_sq_notMem {G : Type u_1} [Group G] {H : Subgroup G} {g : G} (hg : g ^ 2 ∉ H) (h : ∀ (a : G), a ∈ H ∨ g⁻¹ * a ∈ H ∨ g * a ∈ H) : H.index = 3

Three covering cosets give index three. If g² ∉ H and every a satisfies a ∈ H, g⁻¹ a ∈ H or g a ∈ H (that is, a lies in H, g H or g⁻¹ H), then H.index = 3.

theorem AddSubgroup.index_eq_three_of_two_nsmul_notMem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {g : G} (hg : 2 • g ∉ H) (h : ∀ (a : G), a ∈ H ∨ -g + a ∈ H ∨ g + a ∈ H) : H.index = 3

Three covering cosets give index three. If 2 • g ∉ H and every a satisfies a ∈ H, -g + a ∈ H or g + a ∈ H (that is, a lies in H, g + H or -g + H), then H.index = 3.