Documentation

TauCeti.GroupTheory.Index.Two

A subgroup of index two inverted by one outside element #

Let N be a subgroup of index two in a group G, and suppose a single element s outside N conjugates N by inversion, s * x * s⁻¹ = x⁻¹. Conjugation by s then reverses products while being an automorphism, so N is abelian, and every other element outside N is s * n with n ∈ N, whose conjugation action is the same as that of s: the inversion hypothesis on one outside element is already the inversion hypothesis on all of them.

This is the shape of a dihedral group over its rotations and of a dicyclic group over its cyclic subgroup, and three further elementary consequences of it are recorded here: all the elements outside N have one and the same square, that common square squares to one, and -- for a finite G -- the elements outside N are exactly as many as those inside.

The file also records the coset structure of an arbitrary subgroup of index two, which needs no inverting element: G ⧸ N consists of the trivial coset and the coset of any s ∉ N, so a finite sum over G ⧸ N has exactly those two terms.

Main statements #

source
theorem TauCeti.isMulCommutative_of_conj_eq_inv {G : Type u_1} [Group G] {N : Subgroup G} {s : G} (hinv : ∀ x ∈ N, s * x * s⁻¹ = x⁻¹) :
IsMulCommutative ↥N

A subgroup conjugated by inversion is abelian. If s * x * s⁻¹ = x⁻¹ for every x ∈ N, then N is commutative. Neither s ∉ N nor any hypothesis on the index of N is needed.

source
theorem TauCeti.sq_eq_one_of_mem_of_conj_eq_inv {G : Type u_1} [Group G] {N : Subgroup G} {s : G} (hs : s ∈ N) (hinv : ∀ x ∈ N, s * x * s⁻¹ = x⁻¹) {x : G} (hx : x ∈ N) :
x ^ 2 = 1

A subgroup inverted by conjugation by one of its own elements has exponent two. If an element s ∈ N satisfies s * x * s⁻¹ = x⁻¹ for every x ∈ N, then x ^ 2 = 1 for every x ∈ N.

source
theorem TauCeti.monoidHom_sq_eq_one_of_mem_of_conj_eq_inv {G : Type u_1} [Group G] {N : Subgroup G} {M : Type u_2} [CommMonoid M] {s : G} (hs : s ∈ N) (hinv : ∀ x ∈ N, s * x * s⁻¹ = x⁻¹) (ψ : ↥N →* M) :
ψ ^ 2 = 1

A homomorphism to a commutative monoid squares to one on a subgroup inverted by one of its own elements, that subgroup having exponent two (TauCeti.sq_eq_one_of_mem_of_conj_eq_inv). Read contrapositively, a single ψ with ψ ^ 2 ≠ 1 places every element inverting N outside N.

source
theorem TauCeti.conj_eq_inv_of_notMem_of_index_two {G : Type u_1} [Group G] {N : Subgroup G} (hindex : N.index = 2) {s : G} (hs : s ∉ N) (hinv : ∀ x ∈ N, s * x * s⁻¹ = x⁻¹) {t : G} (ht : t ∉ N) {x : G} (hx : x ∈ N) :
t * x * t⁻¹ = x⁻¹

One inverting element outside a subgroup of index two makes every element outside it invert. If some s ∉ N satisfies s * x * s⁻¹ = x⁻¹ for every x ∈ N, then so does every t ∉ N; the inversion hypothesis may therefore be checked on a single outside element.

source
theorem TauCeti.sq_eq_sq_of_notMem_of_index_two {G : Type u_1} [Group G] {N : Subgroup G} (hindex : N.index = 2) {s : G} (hs : s ∉ N) (hinv : ∀ x ∈ N, s * x * s⁻¹ = x⁻¹) {g : G} (hg : g ∉ N) :
g ^ 2 = s ^ 2

All the elements outside an inverted subgroup of index two have the same square, namely the square of the chosen inverting element s. That square lies in N by Subgroup.sq_mem_of_index_two.

source
theorem TauCeti.sq_sq_eq_one_of_conj_eq_inv {G : Type u_1} [Group G] {N : Subgroup G} {s : G} (hsq : s ^ 2 ∈ N) (hinv : ∀ x ∈ N, s * x * s⁻¹ = x⁻¹) :
(s ^ 2) ^ 2 = 1

The common square of the elements outside an inverted subgroup squares to one: (s ^ 2) ^ 2 = 1. Only membership of s ^ 2 in N is needed, which Subgroup.sq_mem_of_index_two supplies when N has index two.

source
theorem TauCeti.card_filter_notMem_eq_card_of_index_two {G : Type u_1} [Group G] {N : Subgroup G} [Fintype G] [DecidablePred fun (x : G) => x ∈ N] (hindex : N.index = 2) :
{x : G | x ∉ N}.card = Nat.card ↥N

The complement of a subgroup of index two has as many elements as the subgroup: in a finite group, both halves of G have Nat.card N elements.

The two cosets of a subgroup of index two #

source
theorem TauCeti.mk_ne_mk_one_of_notMem {G : Type u_1} [Group G] {N : Subgroup G} {s : G} (hs : s ∉ N) :
↑s ≠ ↑1

The coset of an element outside N is not the trivial coset. No hypothesis on the index is needed.

source
theorem TauCeti.eq_mk_one_or_eq_mk_of_index_two {G : Type u_1} [Group G] {N : Subgroup G} (hindex : N.index = 2) {s : G} (hs : s ∉ N) (u : G ⧸ N) :
u = ↑1 ∨ u = ↑s

A subgroup of index two has exactly two cosets: the trivial coset and the coset of any element s outside it.

source
theorem TauCeti.sum_quotient_eq_add_of_index_two {G : Type u_1} [Group G] {N : Subgroup G} [Fintype (G ⧸ N)] {M : Type u_2} [AddCommMonoid M] (hindex : N.index = 2) {s : G} (hs : s ∉ N) (f : G ⧸ N → M) :
∑ u : G ⧸ N, f u = f ↑1 + f ↑s

A finite sum over the cosets of a subgroup of index two has two terms, one at the trivial coset and one at the coset of any element s outside the subgroup.

source
theorem TauCeti.smul_mk_one_of_notMem_of_index_two {G : Type u_1} [Group G] {N : Subgroup G} (hindex : N.index = 2) {s γ : G} (hs : s ∉ N) (hγ : γ ∉ N) :
γ • ↑1 = ↑s

An element outside a subgroup of index two carries the trivial coset to the coset of any other element outside it.

source
theorem TauCeti.smul_mk_of_notMem_of_index_two {G : Type u_1} [Group G] {N : Subgroup G} (hindex : N.index = 2) {s γ : G} (hs : s ∉ N) (hγ : γ ∉ N) :
γ • ↑s = ↑1

An element outside a subgroup of index two carries the coset of any element outside it to the trivial coset.

The character of a subgroup of index two #

source
noncomputable def Subgroup.indexTwoCharacter {G : Type u_1} [Group G] (N : Subgroup G) (hN : N.index = 2) :
G →* Multiplicative (ZMod 2)

The character of a subgroup of index two: the homomorphism χ_N : G → 𝔽₂, written multiplicatively, that is 0 on N and 1 off it. It is the sign indicator Subgroup.signIndicatorHom read through the identification TauCeti.additiveIntUnitsAddEquiv of ℤˣ with ZMod 2. Its kernel is N (Subgroup.ker_indexTwoCharacter).

Equations
Instances For
    source
    @[simp]
    theorem Subgroup.toAdd_indexTwoCharacter_of_mem {G : Type u_1} [Group G] {N : Subgroup G} (hN : N.index = 2) {γ : G} (h : γ ∈ N) :
    Multiplicative.toAdd ((N.indexTwoCharacter hN) γ) = 0

    The character of a subgroup of index two vanishes on the subgroup.

    source
    @[simp]
    theorem Subgroup.toAdd_indexTwoCharacter_of_notMem {G : Type u_1} [Group G] {N : Subgroup G} (hN : N.index = 2) {γ : G} (h : γ ∉ N) :
    Multiplicative.toAdd ((N.indexTwoCharacter hN) γ) = 1

    The character of a subgroup of index two is 1 off the subgroup.

    source
    @[simp]
    theorem Subgroup.indexTwoCharacter_eq_one_iff {G : Type u_1} [Group G] {N : Subgroup G} (hN : N.index = 2) {γ : G} :
    (N.indexTwoCharacter hN) γ = 1 ↔ γ ∈ N

    The character of a subgroup of index two is trivial exactly on the subgroup.

    source
    @[simp]
    theorem Subgroup.ker_indexTwoCharacter {G : Type u_1} [Group G] {N : Subgroup G} (hN : N.index = 2) :
    (N.indexTwoCharacter hN).ker = N

    The kernel of the character of a subgroup of index two is the subgroup.