# mathlibdocumentation

group_theory.complement

# Complements #

In this file we define the complement of a subgroup.

## Main definitions #

• is_complement S T where S and T are subsets of G states that every g : G can be written uniquely as a product s * t for s ∈ S, t ∈ T.
• left_transversals T where T is a subset of G is the set of all left-complements of T, i.e. the set of all S : set G that contain exactly one element of each left coset of T.
• right_transversals S where S is a subset of G is the set of all right-complements of S, i.e. the set of all T : set G that contain exactly one element of each right coset of S.

## Main results #

• is_complement_of_coprime : Subgroups of coprime order are complements.
• exists_right_complement_of_coprime : 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.
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} :
∀ (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} :
∀ (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 : 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 : T) (g : G) :
∃! (x : S × T), x.fst.val + x.snd.val = g
theorem add_subgroup.is_complement.symm {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : K) :
theorem subgroup.is_complement.symm {G : Type u_1} [group G] {H K : subgroup G} (h : K) :
theorem subgroup.is_complement_comm {G : Type u_1} [group G] {H K : subgroup G} :
theorem subgroup.mem_left_transversals_iff_exists_unique_inv_mul_mem {G : Type u_1} [group G] {S T : set G} :
∀ (g : G), ∃! (s : S), (s)⁻¹ * g 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} :
∀ (g : G), ∃! (s : S), g * (s)⁻¹ T
∀ (g : G), ∃! (s : S), g + -s T
theorem add_subgroup.mem_left_transversals_iff_exists_unique_quotient_mk'_eq {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} :
∀ (q : , ∃! (s : S), = q
theorem subgroup.mem_left_transversals_iff_exists_unique_quotient_mk'_eq {G : Type u_1} [group G] {H : subgroup G} {S : set G} :
∀ (q : , ∃! (s : S), = q
theorem subgroup.mem_right_transversals_iff_exists_unique_quotient_mk'_eq {G : Type u_1} [group G] {H : subgroup G} {S : set G} :
∀ (q : , ∃! (s : S), = q
theorem add_subgroup.mem_right_transversals_iff_exists_unique_quotient_mk'_eq {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} :
∀ (q : , ∃! (s : S), = q
theorem subgroup.mem_left_transversals_iff_bijective {G : Type u_1} [group G] {H : subgroup G} {S : set G} :
theorem add_subgroup.mem_left_transversals_iff_bijective {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} :
theorem subgroup.mem_right_transversals_iff_bijective {G : Type u_1} [group G] {H : subgroup G} {S : set G} :
@[instance]
@[instance]
def subgroup.left_transversals.inhabited {G : Type u_1} [group G] {H : subgroup G} :
Equations
@[instance]
def subgroup.right_transversals.inhabited {G : Type u_1} [group G] {H : subgroup G} :
Equations
@[instance]
theorem subgroup.is_complement_of_disjoint {G : Type u_1} [group G] {H K : subgroup G} [fintype G] [fintype H] [fintype K] (h1 : = ) (h2 : K) :
theorem subgroup.is_complement_of_coprime {G : Type u_1} [group G] {H K : subgroup G} [fintype G] [fintype H] [fintype K] (h1 : = ) (h2 : .coprime ) :
@[instance]
@[instance]
def subgroup.left_transversals.mul_action {G : Type u_1} [group G] {H : subgroup G} :
Equations
theorem subgroup.smul_symm_apply_eq_mul_symm_apply_inv_smul {G : Type u_1} [group G] {H : subgroup G} (g : G) (α : ) (q : quotient_group.quotient H) :
(((equiv.of_bijective (g α).val) _).symm) q) = g * (.symm) (g⁻¹ q))
def add_subgroup.diff {G : Type u_1} [add_group G] {H : add_subgroup G} [H.is_commutative] (α β : ) [hH : H.normal] :

The difference of two left transversals

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

The difference of two left transversals

Equations
=
theorem subgroup.diff_mul_diff {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] (α β γ : ) [H.normal] :
β) * =
theorem subgroup.diff_self {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] (α : ) [H.normal] :
= 1
theorem add_subgroup.diff_self {G : Type u_1} [add_group G] {H : add_subgroup G} [H.is_commutative] (α : ) [H.normal] :
= 0
theorem add_subgroup.diff_neg {G : Type u_1} [add_group G] {H : add_subgroup G} [H.is_commutative] (α β : ) [H.normal] :
theorem subgroup.diff_inv {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] (α β : ) [H.normal] :
β)⁻¹ =
theorem subgroup.smul_diff_smul {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] (α β : ) [hH : H.normal] (g : G) :
subgroup.diff (g α) (g β) = (g * β)) * g⁻¹, _⟩
theorem subgroup.smul_diff {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] (α β : ) [H.normal] (h : H) :
subgroup.diff (h α) β = *
@[instance]
def subgroup.setoid_diff {G : Type u_1} [group G] (H : subgroup G) [H.is_commutative] [H.normal] :
Equations
def subgroup.quotient_diff {G : Type u_1} [group G] (H : subgroup G) [H.is_commutative] [H.normal] :
Type u_1

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

Equations
@[instance]
def subgroup.quotient_diff.inhabited {G : Type u_1} [group G] (H : subgroup G) [H.is_commutative] [H.normal] :
Equations
@[instance]
def subgroup.quotient_diff.mul_action {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [H.normal] :
Equations
theorem subgroup.exists_smul_eq {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [fintype H] [H.normal] (α β : H.quotient_diff) (hH : .coprime ) :
∃ (h : H), h α = β
theorem subgroup.smul_left_injective {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [fintype H] [H.normal] (α : H.quotient_diff) (hH : .coprime ) :
function.injective (λ (h : H), h α)
theorem subgroup.is_complement_stabilizer_of_coprime {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [fintype H] [fintype G] [H.normal] {α : H.quotient_diff} (hH : .coprime ) :
theorem subgroup.exists_right_complement_of_coprime {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [fintype H] [fintype G] [H.normal] (hH : .coprime ) :
∃ (K : subgroup G),

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.

theorem subgroup.exists_left_complement_of_coprime {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [fintype H] [fintype G] [H.normal] (hH : .coprime ) :
∃ (K : subgroup G),

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.