Complements #
In this file we define the complement of a subgroup.
Main definitions #
is_complement S T
whereS
andT
are subsets ofG
states that everyg : G
can be written uniquely as a products * t
fors ∈ S
,t ∈ T
.left_transversals T
whereT
is a subset ofG
is the set of all left-complements ofT
, i.e. the set of allS : set G
that contain exactly one element of each left coset ofT
.right_transversals S
whereS
is a subset ofG
is the set of all right-complements ofS
, i.e. the set of allT : set G
that contain exactly one element of each right coset ofS
.
Main results #
is_complement_of_coprime
: Subgroups of coprime order are complements.
S
and T
are complements if (*) : S × T → G
is a bijection
S
and T
are complements if (*) : S × T → G
is a bijection.
This notion generalizes left transversals, right transversals, and complementary subgroups.
H
and K
are complements if (*) : H × K → G
is a bijection
H
and K
are complements if (*) : H × K → G
is a bijection
The set of left-complements of T : set G
Equations
- add_subgroup.left_transversals T = {S : set G | add_subgroup.is_complement S T}
The set of left-complements of T : set G
Equations
- subgroup.left_transversals T = {S : set G | subgroup.is_complement S T}
The set of right-complements of S : set G
Equations
- subgroup.right_transversals S = {T : set G | subgroup.is_complement S T}
The set of right-complements of S : set G
Equations
- add_subgroup.right_transversals S = {T : set G | add_subgroup.is_complement S T}
theorem
subgroup.is_complement'_def
{G : Type u_1}
[group G]
{H K : subgroup G} :
H.is_complement' K ↔ subgroup.is_complement ↑H ↑K
theorem
subgroup.is_complement'.symm
{G : Type u_1}
[group G]
{H K : subgroup G}
(h : H.is_complement' K) :
K.is_complement' H
theorem
add_subgroup.is_complement'.symm
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h : H.is_complement' K) :
K.is_complement' H
theorem
add_subgroup.is_complement'_comm
{G : Type u_1}
[add_group G]
{H K : add_subgroup G} :
H.is_complement' K ↔ K.is_complement' H
theorem
subgroup.is_complement'_comm
{G : Type u_1}
[group G]
{H K : subgroup G} :
H.is_complement' K ↔ K.is_complement' H
theorem
subgroup.is_complement_singleton_left
{G : Type u_1}
[group G]
{S : set G}
{g : G} :
subgroup.is_complement {g} S ↔ S = ⊤
theorem
add_subgroup.is_complement_singleton_left
{G : Type u_1}
[add_group G]
{S : set G}
{g : G} :
add_subgroup.is_complement {g} S ↔ S = ⊤
theorem
add_subgroup.is_complement_singleton_right
{G : Type u_1}
[add_group G]
{S : set G}
{g : G} :
add_subgroup.is_complement S {g} ↔ S = ⊤
theorem
subgroup.is_complement_singleton_right
{G : Type u_1}
[group G]
{S : set G}
{g : G} :
subgroup.is_complement S {g} ↔ S = ⊤
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} :
⊥.is_complement' H ↔ H = ⊤
@[simp]
theorem
add_subgroup.is_complement'_bot_left
{G : Type u_1}
[add_group G]
{H : add_subgroup G} :
⊥.is_complement' H ↔ H = ⊤
@[simp]
theorem
add_subgroup.is_complement'_bot_right
{G : Type u_1}
[add_group G]
{H : add_subgroup G} :
H.is_complement' ⊥ ↔ H = ⊤
@[simp]
theorem
subgroup.is_complement'_bot_right
{G : Type u_1}
[group G]
{H : subgroup G} :
H.is_complement' ⊥ ↔ H = ⊤
@[simp]
theorem
subgroup.is_complement'_top_left
{G : Type u_1}
[group G]
{H : subgroup G} :
⊤.is_complement' H ↔ H = ⊥
@[simp]
theorem
add_subgroup.is_complement'_top_left
{G : Type u_1}
[add_group G]
{H : add_subgroup G} :
⊤.is_complement' H ↔ H = ⊥
@[simp]
theorem
subgroup.is_complement'_top_right
{G : Type u_1}
[group G]
{H : subgroup G} :
H.is_complement' ⊤ ↔ H = ⊥
@[simp]
theorem
add_subgroup.is_complement'_top_right
{G : Type u_1}
[add_group G]
{H : add_subgroup G} :
H.is_complement' ⊤ ↔ H = ⊥
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} :
S ∈ add_subgroup.left_transversals ↑H ↔ ∀ (q : quotient (quotient_add_group.left_rel H)), ∃! (s : ↥S), quotient.mk' s.val = q
theorem
subgroup.mem_left_transversals_iff_exists_unique_quotient_mk'_eq
{G : Type u_1}
[group G]
{H : subgroup G}
{S : set G} :
S ∈ subgroup.left_transversals ↑H ↔ ∀ (q : quotient (quotient_group.left_rel H)), ∃! (s : ↥S), quotient.mk' s.val = q
theorem
subgroup.mem_right_transversals_iff_exists_unique_quotient_mk'_eq
{G : Type u_1}
[group G]
{H : subgroup G}
{S : set G} :
S ∈ subgroup.right_transversals ↑H ↔ ∀ (q : quotient (quotient_group.right_rel H)), ∃! (s : ↥S), quotient.mk' s.val = 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} :
S ∈ add_subgroup.right_transversals ↑H ↔ ∀ (q : quotient (quotient_add_group.right_rel H)), ∃! (s : ↥S), quotient.mk' s.val = 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
add_subgroup.mem_right_transversals_iff_bijective
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
{S : set G} :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
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) :
is_compl H K
theorem
subgroup.is_complement'.sup_eq_top
{G : Type u_1}
[group G]
{H K : subgroup G}
(h : H.is_complement' K) :
theorem
subgroup.is_complement'.disjoint
{G : Type u_1}
[group G]
{H K : subgroup G}
(h : H.is_complement' K) :
disjoint H K
theorem
subgroup.is_complement.card_mul
{G : Type u_1}
[group G]
{S T : set G}
[fintype G]
[fintype ↥S]
[fintype ↥T]
(h : subgroup.is_complement S T) :
(fintype.card ↥S) * fintype.card ↥T = fintype.card G
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) :
(fintype.card ↥H) * fintype.card ↥K = fintype.card G
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 : (fintype.card ↥H) * fintype.card ↥K = fintype.card G)
(h2 : disjoint H K) :
H.is_complement' K
theorem
subgroup.is_complement'_iff_card_mul_and_disjoint
{G : Type u_1}
[group G]
{H K : subgroup G}
[fintype G]
[fintype ↥H]
[fintype ↥K] :
H.is_complement' K ↔ (fintype.card ↥H) * fintype.card ↥K = fintype.card G ∧ disjoint H K
theorem
subgroup.is_complement'_of_coprime
{G : Type u_1}
[group G]
{H K : subgroup G}
[fintype G]
[fintype ↥H]
[fintype ↥K]
(h1 : (fintype.card ↥H) * fintype.card ↥K = fintype.card G)
(h2 : (fintype.card ↥H).coprime (fintype.card ↥K)) :
H.is_complement' K