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

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
def add_subgroup.is_complement' {G : Type u_1} [add_group G] (H K : add_subgroup G) :
Prop

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

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 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.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 subgroup.is_complement_singleton_top {G : Type u_1} [group G] {g : G} :
theorem subgroup.is_complement_singleton_left {G : Type u_1} [group G] {S : set G} {g : G} :
theorem add_subgroup.is_complement_singleton_left {G : Type u_1} [add_group G] {S : set G} {g : G} :
theorem add_subgroup.is_complement_singleton_right {G : Type u_1} [add_group G] {S : set G} {g : G} :
theorem subgroup.is_complement_singleton_right {G : Type u_1} [group G] {S : set G} {g : G} :
theorem add_subgroup.is_complement_top_left {G : Type u_1} [add_group G] {S : set G} :
add_subgroup.is_complement S ∃ (g : G), S = {g}
theorem subgroup.is_complement_top_left {G : Type u_1} [group G] {S : set G} :
subgroup.is_complement S ∃ (g : G), S = {g}
theorem add_subgroup.is_complement_top_right {G : Type u_1} [add_group G] {S : set G} :
add_subgroup.is_complement S ∃ (g : G), S = {g}
theorem subgroup.is_complement_top_right {G : Type u_1} [group G] {S : set G} :
subgroup.is_complement S ∃ (g : G), S = {g}
@[simp]
theorem subgroup.is_complement'_bot_left {G : Type u_1} [group G] {H : subgroup G} :
@[simp]
@[simp]
@[simp]
theorem subgroup.is_complement'_bot_right {G : Type u_1} [group G] {H : subgroup G} :
@[simp]
theorem subgroup.is_complement'_top_left {G : Type u_1} [group G] {H : subgroup G} :
@[simp]
@[simp]
theorem subgroup.is_complement'_top_right {G : Type u_1} [group G] {H : subgroup G} :
@[simp]
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
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.exists_left_transversal {G : Type u_1} [add_group G] {H : add_subgroup G} (g : G) :
∃ (S : set G) (H : S add_subgroup.left_transversals H), g S
theorem subgroup.exists_left_transversal {G : Type u_1} [group G] {H : subgroup G} (g : G) :
∃ (S : set G) (H : S subgroup.left_transversals H), g S
theorem add_subgroup.exists_right_transversal {G : Type u_1} [add_group G] {H : add_subgroup G} (g : G) :
∃ (S : set G) (H : S add_subgroup.right_transversals H), g S
theorem subgroup.exists_right_transversal {G : Type u_1} [group G] {H : subgroup G} (g : G) :
∃ (S : set G) (H : S subgroup.right_transversals 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 subgroup.left_transversals H) :
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 add_subgroup.left_transversals H) :
G H S

A left transversal is in bijection with left cosets.

Equations
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) :
noncomputable def subgroup.mem_left_transversals.to_fun {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S subgroup.left_transversals H) :
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 add_subgroup.left_transversals H) :
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

A right transversal is in bijection with right cosets.

Equations

A right transversal is in bijection with right cosets.

Equations
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 add_subgroup.right_transversals H) :
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 subgroup.right_transversals H) :
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
@[protected, instance]
Equations
theorem subgroup.is_complement'.is_compl {G : Type u_1} [group G] {H K : subgroup G} (h : H.is_complement' 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) :
theorem subgroup.is_complement'_stabilizer {G : Type u_1} [group G] {H : subgroup G} {α : Type u_2} [mul_action G α] (a : α) (h1 : ∀ (h : H), h a = ah = 1) (h2 : ∀ (g : G), ∃ (h : H), h g a = a) :