mathlib documentation

group_theory.complement

Complements #

In this file we define the complement of a subgroup.

Main definitions #

Main results #

def add_subgroup.is_complement {G : Type u_1} [add_group G] (S T : set G) :
Prop

S and T are complements if (*) : S × T → G is a bijection

def subgroup.is_complement {G : Type u_1} [group G] (S T : set G) :
Prop

S and T are complements if (*) : S × T → G is a bijection. This notion generalizes left transversals, right transversals, and complementary subgroups.

Equations
def add_subgroup.left_transversals {G : Type u_1} [add_group G] (T : set G) :
set (set G)

The set of left-complements of T : set G

def subgroup.left_transversals {G : Type u_1} [group G] (T : set G) :
set (set G)

The set of left-complements of T : set G

Equations
def subgroup.right_transversals {G : Type u_1} [group G] (S : set G) :
set (set G)

The set of right-complements of S : set G

Equations
def add_subgroup.right_transversals {G : Type u_1} [add_group G] (S : set G) :
set (set G)

The set of right-complements of S : set G

theorem add_subgroup.is_complement_iff_exists_unique {G : Type u_1} [add_group G] {S T : set G} :
add_subgroup.is_complement S T ∀ (g : G), ∃! (x : S × T), x.fst.val + x.snd.val = g
theorem subgroup.is_complement_iff_exists_unique {G : Type u_1} [group G] {S T : set G} :
subgroup.is_complement S T ∀ (g : G), ∃! (x : S × T), (x.fst.val) * x.snd.val = g
theorem subgroup.is_complement.exists_unique {G : Type u_1} [group G] {S T : set G} (h : subgroup.is_complement S T) (g : G) :
∃! (x : S × T), (x.fst.val) * x.snd.val = g
theorem add_subgroup.is_complement.exists_unique {G : Type u_1} [add_group G] {S T : set G} (h : add_subgroup.is_complement S T) (g : G) :
∃! (x : S × T), x.fst.val + x.snd.val = g
theorem subgroup.mem_left_transversals_iff_exists_unique_inv_mul_mem {G : Type u_1} [group G] {S T : set G} :
S subgroup.left_transversals T ∀ (g : G), ∃! (s : S), (s)⁻¹ * g T
theorem add_subgroup.mem_left_transversals_iff_exists_unique_neg_add_mem {G : Type u_1} [add_group G] {S T : set G} :
S add_subgroup.left_transversals T ∀ (g : G), ∃! (s : S), -s + g T
theorem subgroup.mem_right_transversals_iff_exists_unique_mul_inv_mem {G : Type u_1} [group G] {S T : set G} :
S subgroup.right_transversals T ∀ (g : G), ∃! (s : S), g * (s)⁻¹ T

The difference of two left transversals

def subgroup.diff {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [fintype (quotient_group.quotient H)] (α β : (subgroup.left_transversals H)) [hH : H.normal] :

The difference of two left transversals

Equations
theorem subgroup.smul_diff_smul {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [fintype (quotient_group.quotient H)] (α β : (subgroup.left_transversals H)) [hH : H.normal] (g : G) :
subgroup.diff (g α) (g β) = (g * (subgroup.diff α β)) * g⁻¹, _⟩
@[instance]
Equations
def subgroup.quotient_diff {G : Type u_1} [group G] (H : subgroup G) [H.is_commutative] [fintype (quotient_group.quotient H)] [H.normal] :
Type u_1

The quotient of the transversals of an abelian normal N by the diff relation

Equations
theorem subgroup.exists_smul_eq {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [fintype (quotient_group.quotient H)] [fintype H] [H.normal] (α β : H.quotient_diff) (hH : (fintype.card H).coprime (fintype.card (quotient_group.quotient H))) :
∃ (h : H), h α = β

Schur-Zassenhaus for abelian normal subgroups: If H : subgroup G is abelian, normal, and has order coprime to its index, then there exists a subgroup K which is a (right) complement of H.

Schur-Zassenhaus for abelian normal subgroups: If H : subgroup G is abelian, normal, and has order coprime to its index, then there exists a subgroup K which is a (left) complement of H.