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.

source

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

add_subgroup.is_complement S T = function.bijective (λ (x : ↥S × ↥T), x.fst.val + x.snd.val)

source

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

subgroup.is_complement S T = function.bijective (λ (x : ↥S × ↥T), (x.fst.val) * x.snd.val)

source

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

source

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

source

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

add_subgroup.left_transversals T = {S : set G | add_subgroup.is_complement S T}

source

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

subgroup.left_transversals T = {S : set G | subgroup.is_complement S T}

source

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

subgroup.right_transversals S = {T : set G | subgroup.is_complement S T}

source

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

add_subgroup.right_transversals S = {T : set G | add_subgroup.is_complement S T}

source

theorem subgroup.is_complement'_def {G : Type u_1} [group G] {H K : subgroup G} :

H.is_complement' K ↔ subgroup.is_complement ↑H ↑K

source

theorem add_subgroup.is_complement'_def {G : Type u_1} [add_group G] {H K : add_subgroup G} :

H.is_complement' K ↔ add_subgroup.is_complement ↑H ↑K

source

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

source

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

source

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

source

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

source

theorem subgroup.is_complement'.symm {G : Type u_1} [group G] {H K : subgroup G} (h : H.is_complement' K) :

K.is_complement' H

source

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

source

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

source

theorem subgroup.is_complement'_comm {G : Type u_1} [group G] {H K : subgroup G} :

H.is_complement' K ↔ K.is_complement' H

source

theorem subgroup.is_complement_top_singleton {G : Type u_1} [group G] {g : G} :

subgroup.is_complement ⊤ {g}

source

theorem add_subgroup.is_complement_top_singleton {G : Type u_1} [add_group G] {g : G} :

add_subgroup.is_complement ⊤ {g}

source

theorem subgroup.is_complement_singleton_top {G : Type u_1} [group G] {g : G} :

subgroup.is_complement {g} ⊤

source

theorem add_subgroup.is_complement_singleton_top {G : Type u_1} [add_group G] {g : G} :

add_subgroup.is_complement {g} ⊤

source

theorem subgroup.is_complement_singleton_left {G : Type u_1} [group G] {S : set G} {g : G} :

subgroup.is_complement {g} S ↔ S = ⊤

source

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 = ⊤

source

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 = ⊤

source

theorem subgroup.is_complement_singleton_right {G : Type u_1} [group G] {S : set G} {g : G} :

subgroup.is_complement S {g} ↔ S = ⊤

source

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}

source

theorem subgroup.is_complement_top_left {G : Type u_1} [group G] {S : set G} :

subgroup.is_complement ⊤ S ↔ ∃ (g : G), S = {g}

source

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}

source

theorem subgroup.is_complement_top_right {G : Type u_1} [group G] {S : set G} :

subgroup.is_complement S ⊤ ↔ ∃ (g : G), S = {g}

source

theorem subgroup.is_complement'_top_bot {G : Type u_1} [group G] :

⊤.is_complement' ⊥

source

theorem add_subgroup.is_complement'_top_bot {G : Type u_1} [add_group G] :

⊤.is_complement' ⊥

source

theorem subgroup.is_complement'_bot_top {G : Type u_1} [group G] :

⊥.is_complement' ⊤

source

theorem add_subgroup.is_complement'_bot_top {G : Type u_1} [add_group G] :

⊥.is_complement' ⊤

source

@[simp]

theorem subgroup.is_complement'_bot_left {G : Type u_1} [group G] {H : subgroup G} :

⊥.is_complement' H ↔ H = ⊤

source

@[simp]

theorem add_subgroup.is_complement'_bot_left {G : Type u_1} [add_group G] {H : add_subgroup G} :

⊥.is_complement' H ↔ H = ⊤

source

@[simp]

theorem add_subgroup.is_complement'_bot_right {G : Type u_1} [add_group G] {H : add_subgroup G} :

H.is_complement' ⊥ ↔ H = ⊤

source

@[simp]

theorem subgroup.is_complement'_bot_right {G : Type u_1} [group G] {H : subgroup G} :

H.is_complement' ⊥ ↔ H = ⊤

source

@[simp]

theorem subgroup.is_complement'_top_left {G : Type u_1} [group G] {H : subgroup G} :

⊤.is_complement' H ↔ H = ⊥

source

@[simp]

theorem add_subgroup.is_complement'_top_left {G : Type u_1} [add_group G] {H : add_subgroup G} :

⊤.is_complement' H ↔ H = ⊥

source

@[simp]

theorem subgroup.is_complement'_top_right {G : Type u_1} [group G] {H : subgroup G} :

H.is_complement' ⊤ ↔ H = ⊥

source

@[simp]

theorem add_subgroup.is_complement'_top_right {G : Type u_1} [add_group G] {H : add_subgroup G} :

H.is_complement' ⊤ ↔ H = ⊥

source

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

source

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

source

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

source

theorem add_subgroup.mem_right_transversals_iff_exists_unique_add_neg_mem {G : Type u_1} [add_group G] {S T : set G} :

S ∈ add_subgroup.right_transversals T ↔ ∀ (g : G), ∃! (s : ↥S), g + -↑s ∈ T

source

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

source

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

source

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

source

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

source

theorem subgroup.mem_left_transversals_iff_bijective {G : Type u_1} [group G] {H : subgroup G} {S : set G} :

S ∈ subgroup.left_transversals ↑H ↔ function.bijective (set.restrict quotient.mk' S)

source

theorem add_subgroup.mem_left_transversals_iff_bijective {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} :

S ∈ add_subgroup.left_transversals ↑H ↔ function.bijective (set.restrict quotient.mk' S)

source

theorem subgroup.mem_right_transversals_iff_bijective {G : Type u_1} [group G] {H : subgroup G} {S : set G} :

S ∈ subgroup.right_transversals ↑H ↔ function.bijective (set.restrict quotient.mk' S)

source

theorem add_subgroup.mem_right_transversals_iff_bijective {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} :

S ∈ add_subgroup.right_transversals ↑H ↔ function.bijective (set.restrict quotient.mk' S)

source

@[protected, instance]

def add_subgroup.left_transversals.inhabited {G : Type u_1} [add_group G] {H : add_subgroup G} :

inhabited ↥(add_subgroup.left_transversals ↑H)

Equations

add_subgroup.left_transversals.inhabited = {default := ⟨set.range quotient.out', _⟩}

source

@[protected, instance]

def subgroup.left_transversals.inhabited {G : Type u_1} [group G] {H : subgroup G} :

inhabited ↥(subgroup.left_transversals ↑H)

Equations

subgroup.left_transversals.inhabited = {default := ⟨set.range quotient.out', _⟩}

source

@[protected, instance]

def subgroup.right_transversals.inhabited {G : Type u_1} [group G] {H : subgroup G} :

inhabited ↥(subgroup.right_transversals ↑H)

Equations

subgroup.right_transversals.inhabited = {default := ⟨set.range quotient.out', _⟩}

source

@[protected, instance]

def add_subgroup.right_transversals.inhabited {G : Type u_1} [add_group G] {H : add_subgroup G} :

inhabited ↥(add_subgroup.right_transversals ↑H)

Equations

add_subgroup.right_transversals.inhabited = {default := ⟨set.range quotient.out', _⟩}

source

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

source

theorem subgroup.is_complement'.sup_eq_top {G : Type u_1} [group G] {H K : subgroup G} (h : H.is_complement' K) :

H ⊔ K = ⊤

source

theorem subgroup.is_complement'.disjoint {G : Type u_1} [group G] {H K : subgroup G} (h : H.is_complement' K) :

disjoint H K

source

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

source

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

source

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

source

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

source

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