# 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.
• transfer_transversal H g is a specific left_transversal of H that is used in the computation of the transfer homomorphism evaluated at an element g : G.

## Main results #

• is_complement_of_coprime : Subgroups of coprime order are complements.
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

Equations
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
@[reducible]
Prop

H and K are complements if (*) : H × K → G is a bijection

@[reducible]
def subgroup.is_complement' {G : Type u_1} [group G] (H K : subgroup G) :
Prop

H and K are complements if (*) : H × K → G is a bijection

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

Equations
Instances for ↥add_subgroup.left_transversals
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
Instances for ↥subgroup.left_transversals
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
Instances for ↥subgroup.right_transversals
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

Equations
Instances for ↥add_subgroup.right_transversals
theorem subgroup.is_complement'_def {G : Type u_1} [group G] {H K : subgroup 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 subgroup.is_complement'.symm {G : Type u_1} [group G] {H K : subgroup G} (h : H.is_complement' K) :
theorem add_subgroup.is_complement'.symm {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H.is_complement' K) :
theorem subgroup.is_complement'_comm {G : Type u_1} [group G] {H K : subgroup G} :
theorem subgroup.is_complement_top_singleton {G : Type u_1} [group G] {g : G} :
theorem add_subgroup.is_complement_top_singleton {G : Type u_1} [add_group G] {g : G} :
theorem subgroup.is_complement_singleton_top {G : Type u_1} [group G] {g : G} :
theorem add_subgroup.is_complement_singleton_top {G : Type u_1} [add_group G] {g : G} :
theorem subgroup.is_complement_singleton_left {G : Type u_1} [group G] {S : set G} {g : G} :
S =
theorem add_subgroup.is_complement_singleton_left {G : Type u_1} [add_group G] {S : set G} {g : G} :
S =
theorem add_subgroup.is_complement_singleton_right {G : Type u_1} [add_group G] {S : set G} {g : G} :
S =
theorem subgroup.is_complement_singleton_right {G : Type u_1} [group G] {S : set G} {g : G} :
S =
theorem add_subgroup.is_complement_top_left {G : Type u_1} [add_group G] {S : set G} :
∃ (g : G), S = {g}
theorem subgroup.is_complement_top_left {G : Type u_1} [group G] {S : set G} :
∃ (g : G), S = {g}
theorem add_subgroup.is_complement_top_right {G : Type u_1} [add_group G] {S : set G} :
∃ (g : G), S = {g}
theorem subgroup.is_complement_top_right {G : Type u_1} [group G] {S : set G} :
∃ (g : G), S = {g}
theorem subgroup.is_complement'_top_bot {G : Type u_1} [group G] :
theorem subgroup.is_complement'_bot_top {G : Type u_1} [group G] :
@[simp]
theorem subgroup.is_complement'_bot_left {G : Type u_1} [group G] {H : subgroup G} :
H =
@[simp]
H =
@[simp]
H =
@[simp]
theorem subgroup.is_complement'_bot_right {G : Type u_1} [group G] {H : subgroup G} :
H =
@[simp]
theorem subgroup.is_complement'_top_left {G : Type u_1} [group G] {H : subgroup G} :
H =
@[simp]
H =
@[simp]
theorem subgroup.is_complement'_top_right {G : Type u_1} [group G] {H : subgroup G} :
H =
@[simp]
H =
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} :
theorem subgroup.range_mem_left_transversals {G : Type u_1} [group G] {H : subgroup G} {f : G H → G} (hf : ∀ (q : G H), (f q) = q) :
theorem add_subgroup.range_mem_left_transversals {G : Type u_1} [add_group G] {H : add_subgroup G} {f : G H → G} (hf : ∀ (q : G H), (f q) = q) :
theorem add_subgroup.range_mem_right_transversals {G : Type u_1} [add_group G] {H : add_subgroup G} {f : → G} (hf : ∀ (q : , quotient.mk' (f q) = q) :
theorem subgroup.range_mem_right_transversals {G : Type u_1} [group G] {H : subgroup G} {f : → G} (hf : ∀ (q : , quotient.mk' (f q) = q) :
∃ (S : set G) (H : , g S
theorem subgroup.exists_left_transversal {G : Type u_1} [group G] {H : subgroup G} (g : G) :
∃ (S : set G) (H : , g S
∃ (S : set G) (H : , g S
theorem subgroup.exists_right_transversal {G : Type u_1} [group G] {H : subgroup G} (g : G) :
∃ (S : set G) (H : , g S
noncomputable def subgroup.mem_left_transversals.to_equiv {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ) :
G H S

A left transversal is in bijection with left cosets.

Equations
noncomputable def add_subgroup.mem_left_transversals.to_equiv {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ) :
G H S

A left transversal is in bijection with left cosets.

Equations
theorem subgroup.mem_left_transversals.mk'_to_equiv {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ) (q : G H) :
theorem add_subgroup.mem_left_transversals.mk'_to_equiv {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ) (q : G H) :
theorem add_subgroup.mem_left_transversals.to_equiv_apply {G : Type u_1} [add_group G] {H : add_subgroup G} {f : G H → G} (hf : ∀ (q : G H), (f q) = q) (q : G H) :
theorem subgroup.mem_left_transversals.to_equiv_apply {G : Type u_1} [group G] {H : subgroup G} {f : G H → G} (hf : ∀ (q : G H), (f q) = q) (q : G H) :
= f q
noncomputable def subgroup.mem_left_transversals.to_fun {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ) :
G → S

A left transversal can be viewed as a function mapping each element of the group to the chosen representative from that left coset.

Equations
noncomputable def add_subgroup.mem_left_transversals.to_fun {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ) :
G → S

A left transversal can be viewed as a function mapping each element of the group to the chosen representative from that left coset.

Equations
theorem add_subgroup.mem_left_transversals.neg_to_fun_add_mem {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ) (g : G) :
theorem subgroup.mem_left_transversals.inv_to_fun_mul_mem {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ) (g : G) :
H
theorem subgroup.mem_left_transversals.inv_mul_to_fun_mem {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ) (g : G) :
H
theorem add_subgroup.mem_left_transversals.neg_add_to_fun_mem {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ) (g : G) :
noncomputable def add_subgroup.mem_right_transversals.to_equiv {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ) :

A right transversal is in bijection with right cosets.

Equations
noncomputable def subgroup.mem_right_transversals.to_equiv {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ) :

A right transversal is in bijection with right cosets.

Equations
theorem add_subgroup.mem_right_transversals.mk'_to_equiv {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ) (q : quotient ) :
theorem subgroup.mem_right_transversals.mk'_to_equiv {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ) (q : quotient ) :
theorem subgroup.mem_right_transversals.to_equiv_apply {G : Type u_1} [group G] {H : subgroup G} {f : → G} (hf : ∀ (q : , quotient.mk' (f q) = q) (q : quotient ) :
= f q
theorem add_subgroup.mem_right_transversals.to_equiv_apply {G : Type u_1} [add_group G] {H : add_subgroup G} {f : → G} (hf : ∀ (q : , quotient.mk' (f q) = q) (q : quotient ) :
noncomputable def add_subgroup.mem_right_transversals.to_fun {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ) :
G → S

A right transversal can be viewed as a function mapping each element of the group to the chosen representative from that right coset.

Equations
noncomputable def subgroup.mem_right_transversals.to_fun {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ) :
G → S

A right transversal can be viewed as a function mapping each element of the group to the chosen representative from that right coset.

Equations
theorem add_subgroup.mem_right_transversals.add_neg_to_fun_mem {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ) (g : G) :
theorem subgroup.mem_right_transversals.mul_inv_to_fun_mem {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ) (g : G) :
H
theorem subgroup.mem_right_transversals.to_fun_mul_inv_mem {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ) (g : G) :
H
theorem add_subgroup.mem_right_transversals.to_fun_add_neg_mem {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ) (g : G) :
@[protected, instance]
Equations
@[protected, instance]
def subgroup.left_transversals.mul_action {G : Type u_1} [group G] {H : subgroup G} {F : Type u_2} [group F] [ G]  :
Equations
theorem subgroup.smul_to_fun {G : Type u_1} [group G] {H : subgroup G} {F : Type u_2} [group F] [ G] (f : F) (T : ) (g : G) :
= (f g))
theorem add_subgroup.vadd_to_fun {G : Type u_1} [add_group G] {H : add_subgroup G} {F : Type u_2} [add_group F] [ G] (f : F) (T : ) (g : G) :
theorem subgroup.smul_to_equiv {G : Type u_1} [group G] {H : subgroup G} {F : Type u_2} [group F] [ G] (f : F) (T : ) (q : G H) :
= (f q))
theorem add_subgroup.vadd_to_equiv {G : Type u_1} [add_group G] {H : add_subgroup G} {F : Type u_2} [add_group F] [ G] (f : F) (T : ) (q : G H) :
= (f +ᵥ q))
= f +ᵥ (-f +ᵥ q))
theorem subgroup.smul_apply_eq_smul_apply_inv_smul {G : Type u_1} [group G] {H : subgroup G} {F : Type u_2} [group F] [ G] (f : F) (T : ) (q : G H) :
= f (f⁻¹ q))
@[protected, instance]
Equations
@[protected, instance]
def subgroup.left_transversals.inhabited {G : Type u_1} [group G] {H : subgroup G} :
Equations
@[protected, instance]
def subgroup.right_transversals.inhabited {G : Type u_1} [group G] {H : subgroup G} :
Equations
@[protected, instance]
Equations
theorem subgroup.is_complement'.is_compl {G : Type u_1} [group G] {H K : subgroup G} (h : H.is_complement' K) :
K
theorem subgroup.is_complement'.sup_eq_top {G : Type u_1} [group G] {H K : subgroup G} (h : H.is_complement' K) :
H K =
theorem subgroup.is_complement'.disjoint {G : Type u_1} [group G] {H K : subgroup G} (h : H.is_complement' K) :
K
theorem subgroup.is_complement.card_mul {G : Type u_1} [group G] {S T : set G} [fintype G] [fintype S] [fintype T] (h : T) :
theorem subgroup.is_complement'.card_mul {G : Type u_1} [group G] {H K : subgroup G} [fintype G] [fintype H] [fintype K] (h : H.is_complement' K) :
theorem subgroup.is_complement'_of_card_mul_and_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 ) :
theorem subgroup.is_complement'_stabilizer {G : Type u_1} [group G] {H : subgroup G} {α : Type u_2} [ α] (a : α) (h1 : ∀ (h : H), h a = ah = 1) (h2 : ∀ (g : G), ∃ (h : H), h g a = a) :
noncomputable def subgroup.quotient_equiv_sigma_zmod {G : Type u} [group G] (H : subgroup G) (g : G) :
G H Σ (q : (G H)),

Partition G ⧸ H into orbits of the action of g : G.

Equations
theorem subgroup.quotient_equiv_sigma_zmod_symm_apply {G : Type u} [group G] (H : subgroup G) (g : G) (q : (G H)) (k : zmod ) :
.symm) q, k⟩ = g ^ k
theorem subgroup.quotient_equiv_sigma_zmod_apply {G : Type u} [group G] (H : subgroup G) (g : G) (q : (G H)) (k : ) :
(g ^ k = q, k⟩
noncomputable def subgroup.transfer_function {G : Type u} [group G] (H : subgroup G) (g : G) :
G H → G

The transfer transversal as a function. Given a ⟨g⟩-orbit q₀, g • q₀, ..., g ^ (m - 1) • q₀ in G ⧸ H, an element g ^ k • q₀ is mapped to g ^ k • g₀ for a fixed choice of representative g₀ of q₀.

Equations
theorem subgroup.transfer_function_apply {G : Type u} [group G] (H : subgroup G) (g : G) (q : G H) :
theorem subgroup.coe_transfer_function {G : Type u} [group G] (H : subgroup G) (g : G) (q : G H) :
q) = q
def subgroup.transfer_set {G : Type u} [group G] (H : subgroup G) (g : G) :
set G

The transfer transversal as a set. Contains elements of the form g ^ k • g₀ for fixed choices of representatives g₀ of fixed choices of representatives q₀ of ⟨g⟩-orbits in G ⧸ H.

Equations
theorem subgroup.mem_transfer_set {G : Type u} [group G] (H : subgroup G) (g : G) (q : G H) :
def subgroup.transfer_transversal {G : Type u} [group G] (H : subgroup G) (g : G) :

The transfer transversal. Contains elements of the form g ^ k • g₀ for fixed choices of representatives g₀ of fixed choices of representatives q₀ of ⟨g⟩-orbits in G ⧸ H.

Equations
theorem subgroup.transfer_transversal_apply {G : Type u} [group G] (H : subgroup G) (g : G) (q : G H) :
theorem subgroup.transfer_transversal_apply' {G : Type u} [group G] (H : subgroup G) (g : G) (q : (G H)) (k : zmod ) :
(g ^ k = g ^ k *
theorem subgroup.transfer_transversal_apply'' {G : Type u} [group G] (H : subgroup G) (g : G) (q : (G H)) (k : zmod ) :
(g ^ k = ite (k = 0) * (g ^ k *