Complements

In this file we define the complement of a subgroup.

Main definitions

• Subgroup.IsComplement 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.
• H.LeftTransversal where H is a subgroup of G is the type of all left-complements of H, i.e. the set of all S : Set G that contain exactly one element of each left coset of H.
• H.RightTransversal where H is a subgroup of G is the set of all right-complements of H, i.e. the set of all T : Set G that contain exactly one element of each right coset of H.

Main results

• isComplement'_of_coprime : Subgroups of coprime order are complements.

def Subgroup.IsComplement {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.

If S and T are SetLikes such as Subgroups, see isComplement_iff_bijective for a more ergonomic way to unfold.

Equations

• Subgroup.IsComplement S T = Function.Bijective fun (x : ↑S × ↑T) => ↑x.1 * ↑x.2

def AddSubgroup.IsComplement {G : Type u_1} [AddGroup G] (S T : Set G) : Prop

S and T are complements if (+) : S × T → G is a bijection

If S and T are SetLikes such as AddSubgroups, see isComplement_iff_bijective for a more ergonomic way to unfold.

Equations

• AddSubgroup.IsComplement S T = Function.Bijective fun (x : ↑S × ↑T) => ↑x.1 + ↑x.2

@[reducible, inline]

abbrev Subgroup.IsComplement' {G : Type u_1} [Group G] (H K : Subgroup G) : Prop

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

Equations

• H.IsComplement' K = Subgroup.IsComplement ↑H ↑K

@[reducible, inline]

abbrev AddSubgroup.IsComplement' {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : Prop

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

Equations

• H.IsComplement' K = AddSubgroup.IsComplement ↑H ↑K

theorem Subgroup.isComplement_iff_bijective {G : Type u_1} [Group G] {S : Type u_2} [SetLike S G] (s t : S) : IsComplement ↑s ↑t ↔ Function.Bijective fun (x : ↥s × ↥t) => ↑x.1 * ↑x.2

The correct way to unfold IsComplement for SetLikes such as Subgroups

theorem AddSubgroup.isComplement_iff_bijective {G : Type u_1} [AddGroup G] {S : Type u_2} [SetLike S G] (s t : S) : IsComplement ↑s ↑t ↔ Function.Bijective fun (x : ↥s × ↥t) => ↑x.1 + ↑x.2

The correct way to unfold IsComplement for SetLikes such as AddSubgroups

theorem Subgroup.isComplement'_def {G : Type u_1} [Group G] {H K : Subgroup G} : H.IsComplement' K ↔ IsComplement ↑H ↑K

theorem AddSubgroup.isComplement'_def {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : H.IsComplement' K ↔ IsComplement ↑H ↑K

theorem Subgroup.isComplement_iff_existsUnique {G : Type u_1} [Group G] {S T : Set G} : IsComplement S T ↔ ∀ (g : G), ∃! x : ↑S × ↑T, ↑x.1 * ↑x.2 = g

theorem AddSubgroup.isComplement_iff_existsUnique {G : Type u_1} [AddGroup G] {S T : Set G} : IsComplement S T ↔ ∀ (g : G), ∃! x : ↑S × ↑T, ↑x.1 + ↑x.2 = g

theorem Subgroup.IsComplement.existsUnique {G : Type u_1} [Group G] {S T : Set G} (h : IsComplement S T) (g : G) : ∃! x : ↑S × ↑T, ↑x.1 * ↑x.2 = g

theorem AddSubgroup.IsComplement.existsUnique {G : Type u_1} [AddGroup G] {S T : Set G} (h : IsComplement S T) (g : G) : ∃! x : ↑S × ↑T, ↑x.1 + ↑x.2 = g

theorem Subgroup.IsComplement'.symm {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.IsComplement' K) : K.IsComplement' H

theorem AddSubgroup.IsComplement'.symm {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H.IsComplement' K) : K.IsComplement' H

theorem Subgroup.isComplement'_comm {G : Type u_1} [Group G] {H K : Subgroup G} : H.IsComplement' K ↔ K.IsComplement' H

theorem AddSubgroup.isComplement'_comm {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : H.IsComplement' K ↔ K.IsComplement' H

theorem Subgroup.isComplement_univ_singleton {G : Type u_1} [Group G] {g : G} : IsComplement Set.univ {g}

theorem AddSubgroup.isComplement_univ_singleton {G : Type u_1} [AddGroup G] {g : G} : IsComplement Set.univ {g}

theorem Subgroup.isComplement_singleton_univ {G : Type u_1} [Group G] {g : G} : IsComplement {g} Set.univ

theorem AddSubgroup.isComplement_singleton_univ {G : Type u_1} [AddGroup G] {g : G} : IsComplement {g} Set.univ

theorem Subgroup.isComplement_singleton_left {G : Type u_1} [Group G] {S : Set G} {g : G} : IsComplement {g} S ↔ S = Set.univ

theorem AddSubgroup.isComplement_singleton_left {G : Type u_1} [AddGroup G] {S : Set G} {g : G} : IsComplement {g} S ↔ S = Set.univ

theorem Subgroup.isComplement_singleton_right {G : Type u_1} [Group G] {S : Set G} {g : G} : IsComplement S {g} ↔ S = Set.univ

theorem AddSubgroup.isComplement_singleton_right {G : Type u_1} [AddGroup G] {S : Set G} {g : G} : IsComplement S {g} ↔ S = Set.univ

theorem Subgroup.isComplement_univ_left {G : Type u_1} [Group G] {S : Set G} : IsComplement Set.univ S ↔ ∃ (g : G), S = {g}

theorem AddSubgroup.isComplement_univ_left {G : Type u_1} [AddGroup G] {S : Set G} : IsComplement Set.univ S ↔ ∃ (g : G), S = {g}

theorem Subgroup.isComplement_univ_right {G : Type u_1} [Group G] {S : Set G} : IsComplement S Set.univ ↔ ∃ (g : G), S = {g}

theorem AddSubgroup.isComplement_univ_right {G : Type u_1} [AddGroup G] {S : Set G} : IsComplement S Set.univ ↔ ∃ (g : G), S = {g}

theorem Subgroup.IsComplement.mul_eq {G : Type u_1} [Group G] {S T : Set G} (h : IsComplement S T) : S * T = Set.univ

theorem AddSubgroup.IsComplement.add_eq {G : Type u_1} [AddGroup G] {S T : Set G} (h : IsComplement S T) : S + T = Set.univ

@[simp]

theorem Subgroup.not_isComplement_empty_left {G : Type u_1} [Group G] {T : Set G} : ¬IsComplement ∅ T

@[simp]

theorem AddSubgroup.not_isComplement_empty_left {G : Type u_1} [AddGroup G] {T : Set G} : ¬IsComplement ∅ T

@[simp]

theorem Subgroup.not_isComplement_empty_right {G : Type u_1} [Group G] {S : Set G} : ¬IsComplement S ∅

@[simp]

theorem AddSubgroup.not_isComplement_empty_right {G : Type u_1} [AddGroup G] {S : Set G} : ¬IsComplement S ∅

theorem Subgroup.IsComplement.nonempty_left {G : Type u_1} [Group G] {S T : Set G} (hst : IsComplement S T) : S.Nonempty

theorem AddSubgroup.IsComplement.nonempty_left {G : Type u_1} [AddGroup G] {S T : Set G} (hst : IsComplement S T) : S.Nonempty

theorem Subgroup.IsComplement.nonempty_right {G : Type u_1} [Group G] {S T : Set G} (hst : IsComplement S T) : T.Nonempty

theorem AddSubgroup.IsComplement.nonempty_right {G : Type u_1} [AddGroup G] {S T : Set G} (hst : IsComplement S T) : T.Nonempty

theorem Subgroup.IsComplement.pairwiseDisjoint_smul {G : Type u_1} [Group G] {S T : Set G} (hst : IsComplement S T) : S.PairwiseDisjoint fun (x : G) => x • T

theorem AddSubgroup.IsComplement.pairwiseDisjoint_vadd {G : Type u_1} [AddGroup G] {S T : Set G} (hst : IsComplement S T) : S.PairwiseDisjoint fun (x : G) => x +ᵥ T

theorem Subgroup.IsComplement.card_mul_card {G : Type u_1} [Group G] {S T : Set G} (h : IsComplement S T) : Nat.card ↑S * Nat.card ↑T = Nat.card G

theorem AddSubgroup.IsComplement.card_mul_card {G : Type u_1} [AddGroup G] {S T : Set G} (h : IsComplement S T) : Nat.card ↑S * Nat.card ↑T = Nat.card G

theorem Subgroup.isComplement'_top_bot {G : Type u_1} [Group G] : ⊤.IsComplement' ⊥

theorem AddSubgroup.isComplement'_top_bot {G : Type u_1} [AddGroup G] : ⊤.IsComplement' ⊥

theorem Subgroup.isComplement'_bot_top {G : Type u_1} [Group G] : ⊥.IsComplement' ⊤

theorem AddSubgroup.isComplement'_bot_top {G : Type u_1} [AddGroup G] : ⊥.IsComplement' ⊤

@[simp]

theorem Subgroup.isComplement'_bot_left {G : Type u_1} [Group G] {H : Subgroup G} : ⊥.IsComplement' H ↔ H = ⊤

@[simp]

theorem AddSubgroup.isComplement'_bot_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : ⊥.IsComplement' H ↔ H = ⊤

@[simp]

theorem Subgroup.isComplement'_bot_right {G : Type u_1} [Group G] {H : Subgroup G} : H.IsComplement' ⊥ ↔ H = ⊤

@[simp]

theorem AddSubgroup.isComplement'_bot_right {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.IsComplement' ⊥ ↔ H = ⊤

@[simp]

theorem Subgroup.isComplement'_top_left {G : Type u_1} [Group G] {H : Subgroup G} : ⊤.IsComplement' H ↔ H = ⊥

@[simp]

theorem AddSubgroup.isComplement'_top_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : ⊤.IsComplement' H ↔ H = ⊥

@[simp]

theorem Subgroup.isComplement'_top_right {G : Type u_1} [Group G] {H : Subgroup G} : H.IsComplement' ⊤ ↔ H = ⊥

@[simp]

theorem AddSubgroup.isComplement'_top_right {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.IsComplement' ⊤ ↔ H = ⊥

theorem Subgroup.isComplement_iff_existsUnique_inv_mul_mem {G : Type u_1} [Group G] {S T : Set G} : IsComplement S T ↔ ∀ (g : G), ∃! s : ↑S, (↑s)⁻¹ * g ∈ T

theorem AddSubgroup.isComplement_iff_existsUnique_neg_add_mem {G : Type u_1} [AddGroup G] {S T : Set G} : IsComplement S T ↔ ∀ (g : G), ∃! s : ↑S, -↑s + g ∈ T

theorem Subgroup.isComplement_iff_existsUnique_mul_inv_mem {G : Type u_1} [Group G] {S T : Set G} : IsComplement S T ↔ ∀ (g : G), ∃! t : ↑T, g * (↑t)⁻¹ ∈ S

theorem AddSubgroup.isComplement_iff_existsUnique_add_neg_mem {G : Type u_1} [AddGroup G] {S T : Set G} : IsComplement S T ↔ ∀ (g : G), ∃! t : ↑T, g + -↑t ∈ S

theorem Subgroup.isComplement_subgroup_right_iff_existsUnique_quotientGroupMk {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} : IsComplement S ↑H ↔ ∀ (q : G ⧸ H), ∃! s : ↑S, ↑↑s = q

theorem AddSubgroup.isComplement_addSubgroup_right_iff_existsUnique_quotientAddGroupMk {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} : IsComplement S ↑H ↔ ∀ (q : G ⧸ H), ∃! s : ↑S, ↑↑s = q

theorem Subgroup.isComplement_subgroup_left_iff_existsUnique_quotientMk'' {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} : IsComplement (↑H) T ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t : ↑T, Quotient.mk'' ↑t = q

theorem AddSubgroup.isComplement_addSubgroup_left_iff_existsUnique_quotientMk'' {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} : IsComplement (↑H) T ↔ ∀ (q : Quotient (QuotientAddGroup.rightRel H)), ∃! t : ↑T, Quotient.mk'' ↑t = q

theorem Subgroup.isComplement_subgroup_right_iff_bijective {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} : IsComplement S ↑H ↔ Function.Bijective (S.restrict QuotientGroup.mk)

theorem AddSubgroup.isComplement_addSubgroup_right_iff_bijective {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} : IsComplement S ↑H ↔ Function.Bijective (S.restrict QuotientAddGroup.mk)

theorem Subgroup.isComplement_subgroup_left_iff_bijective {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} : IsComplement (↑H) T ↔ Function.Bijective (T.restrict Quotient.mk'')

theorem AddSubgroup.isComplement_addSubgroup_left_iff_bijective {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} : IsComplement (↑H) T ↔ Function.Bijective (T.restrict Quotient.mk'')

theorem Subgroup.IsComplement.card_left {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : IsComplement S ↑H) : Nat.card ↑S = H.index

theorem AddSubgroup.IsComplement.card_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (h : IsComplement S ↑H) : Nat.card ↑S = H.index

theorem Subgroup.IsComplement.ncard_left {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : IsComplement S ↑H) : S.ncard = H.index

theorem AddSubgroup.IsComplement.ncard_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (h : IsComplement S ↑H) : S.ncard = H.index

theorem Subgroup.IsComplement.card_right {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (h : IsComplement (↑H) T) : Nat.card ↑T = H.index

theorem AddSubgroup.IsComplement.card_right {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (h : IsComplement (↑H) T) : Nat.card ↑T = H.index

theorem Subgroup.IsComplement.ncard_right {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (h : IsComplement (↑H) T) : T.ncard = H.index

theorem AddSubgroup.IsComplement.ncard_right {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (h : IsComplement (↑H) T) : T.ncard = H.index

theorem Subgroup.isComplement_range_left {G : Type u_1} [Group G] {H : Subgroup G} {f : G ⧸ H → G} (hf : ∀ (q : G ⧸ H), ↑(f q) = q) : IsComplement (Set.range f) ↑H

theorem AddSubgroup.isComplement_range_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {f : G ⧸ H → G} (hf : ∀ (q : G ⧸ H), ↑(f q) = q) : IsComplement (Set.range f) ↑H

theorem Subgroup.isComplement_range_right {G : Type u_1} [Group G] {H : Subgroup G} {f : Quotient (QuotientGroup.rightRel H) → G} (hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q) : IsComplement (↑H) (Set.range f)

theorem AddSubgroup.isComplement_range_right {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {f : Quotient (QuotientAddGroup.rightRel H) → G} (hf : ∀ (q : Quotient (QuotientAddGroup.rightRel H)), Quotient.mk'' (f q) = q) : IsComplement (↑H) (Set.range f)

theorem Subgroup.exists_isComplement_left {G : Type u_1} [Group G] (H : Subgroup G) (g : G) : ∃ (S : Set G), IsComplement S ↑H ∧ g ∈ S

theorem AddSubgroup.exists_isComplement_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (g : G) : ∃ (S : Set G), IsComplement S ↑H ∧ g ∈ S

theorem Subgroup.exists_isComplement_right {G : Type u_1} [Group G] (H : Subgroup G) (g : G) : ∃ (T : Set G), IsComplement (↑H) T ∧ g ∈ T

theorem AddSubgroup.exists_isComplement_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (g : G) : ∃ (T : Set G), IsComplement (↑H) T ∧ g ∈ T

theorem Subgroup.exists_left_transversal_of_le {G : Type u_1} [Group G] {H' H : Subgroup G} (h : H' ≤ H) : ∃ (S : Set G), S * ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H

Given two subgroups H' ⊆ H, there exists a left transversal to H' inside H.

theorem AddSubgroup.exists_left_transversal_of_le {G : Type u_1} [AddGroup G] {H' H : AddSubgroup G} (h : H' ≤ H) : ∃ (S : Set G), S + ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H

Given two subgroups H' ⊆ H, there exists a transversal to H' inside H

theorem Subgroup.exists_right_transversal_of_le {G : Type u_1} [Group G] {H' H : Subgroup G} (h : H' ≤ H) : ∃ (S : Set G), ↑H' * S = ↑H ∧ Nat.card ↥H' * Nat.card ↑S = Nat.card ↥H

Given two subgroups H' ⊆ H, there exists a right transversal to H' inside H.

theorem AddSubgroup.exists_right_transversal_of_le {G : Type u_1} [AddGroup G] {H' H : AddSubgroup G} (h : H' ≤ H) : ∃ (S : Set G), ↑H' + S = ↑H ∧ Nat.card ↥H' * Nat.card ↑S = Nat.card ↥H

Given two subgroups H' ⊆ H, there exists a transversal to H' inside H

noncomputable def Subgroup.IsComplement.equiv {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) : G ≃ ↑S × ↑T

The equivalence G ≃ S × T, such that the inverse is (*) : S × T → G

Equations

• hST.equiv = (Equiv.ofBijective (fun (x : ↑S × ↑T) => ↑x.1 * ↑x.2) hST).symm

@[simp]

theorem Subgroup.IsComplement.equiv_symm_apply {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) (x : ↑S × ↑T) : hST.equiv.symm x = ↑x.1 * ↑x.2

@[simp]

theorem Subgroup.IsComplement.equiv_fst_mul_equiv_snd {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) (g : G) : ↑(hST.equiv g).1 * ↑(hST.equiv g).2 = g

theorem Subgroup.IsComplement.equiv_fst_eq_mul_inv {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) (g : G) : ↑(hST.equiv g).1 = g * (↑(hST.equiv g).2)⁻¹

theorem Subgroup.IsComplement.equiv_snd_eq_inv_mul {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) (g : G) : ↑(hST.equiv g).2 = (↑(hST.equiv g).1)⁻¹ * g

theorem Subgroup.IsComplement.equiv_fst_eq_iff_leftCosetEquivalence {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : IsComplement S ↑K) {g₁ g₂ : G} : (hSK.equiv g₁).1 = (hSK.equiv g₂).1 ↔ LeftCosetEquivalence (↑K) g₁ g₂

theorem Subgroup.IsComplement.equiv_snd_eq_iff_rightCosetEquivalence {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hHT : IsComplement (↑H) T) {g₁ g₂ : G} : (hHT.equiv g₁).2 = (hHT.equiv g₂).2 ↔ RightCosetEquivalence (↑H) g₁ g₂

theorem Subgroup.IsComplement.leftCosetEquivalence_equiv_fst {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : IsComplement S ↑K) (g : G) : LeftCosetEquivalence (↑K) g ↑(hSK.equiv g).1

theorem Subgroup.IsComplement.rightCosetEquivalence_equiv_snd {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hHT : IsComplement (↑H) T) (g : G) : RightCosetEquivalence (↑H) g ↑(hHT.equiv g).2

theorem Subgroup.IsComplement.equiv_fst_eq_self_of_mem_of_one_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 ∈ T) (hg : g ∈ S) : (hST.equiv g).1 = ⟨g, hg⟩

theorem Subgroup.IsComplement.equiv_snd_eq_self_of_mem_of_one_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) : (hST.equiv g).2 = ⟨g, hg⟩

theorem Subgroup.IsComplement.equiv_snd_eq_one_of_mem_of_one_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 ∈ T) (hg : g ∈ S) : (hST.equiv g).2 = ⟨1, h1⟩

theorem Subgroup.IsComplement.equiv_fst_eq_one_of_mem_of_one_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) : (hST.equiv g).1 = ⟨1, h1⟩

theorem Subgroup.IsComplement.equiv_mul_right {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : IsComplement S ↑K) (g : G) (k : ↥K) : hSK.equiv (g * ↑k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k)

theorem Subgroup.IsComplement.equiv_mul_right_of_mem {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : IsComplement S ↑K) {g k : G} (h : k ∈ K) : hSK.equiv (g * k) = ((hSK.equiv g).1, (hSK.equiv g).2 * ⟨k, h⟩)

theorem Subgroup.IsComplement.equiv_mul_left {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hHT : IsComplement (↑H) T) (h : ↥H) (g : G) : hHT.equiv (↑h * g) = (h * (hHT.equiv g).1, (hHT.equiv g).2)

theorem Subgroup.IsComplement.equiv_mul_left_of_mem {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hHT : IsComplement (↑H) T) {h g : G} (hh : h ∈ H) : hHT.equiv (h * g) = (⟨h, hh⟩ * (hHT.equiv g).1, (hHT.equiv g).2)

theorem Subgroup.IsComplement.equiv_one {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) (hs1 : 1 ∈ S) (ht1 : 1 ∈ T) : hST.equiv 1 = (⟨1, hs1⟩, ⟨1, ht1⟩)

theorem Subgroup.IsComplement.equiv_fst_eq_self_iff_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 ∈ T) : ↑(hST.equiv g).1 = g ↔ g ∈ S

theorem Subgroup.IsComplement.equiv_snd_eq_self_iff_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 ∈ S) : ↑(hST.equiv g).2 = g ↔ g ∈ T

theorem Subgroup.IsComplement.coe_equiv_fst_eq_one_iff_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 ∈ S) : ↑(hST.equiv g).1 = 1 ↔ g ∈ T

theorem Subgroup.IsComplement.coe_equiv_snd_eq_one_iff_mem {G : Type u_1} [Group G] {S T : Set G} (hST : IsComplement S T) {g : G} (h1 : 1 ∈ T) : ↑(hST.equiv g).2 = 1 ↔ g ∈ S

noncomputable def Subgroup.IsComplement.leftQuotientEquiv {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S ↑H) : G ⧸ H ≃ ↑S

A left transversal is in bijection with left cosets.

Equations

• hS.leftQuotientEquiv = (Equiv.ofBijective (S.restrict QuotientGroup.mk) ⋯).symm

noncomputable def AddSubgroup.IsComplement.leftQuotientEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : IsComplement S ↑H) : G ⧸ H ≃ ↑S

A left transversal is in bijection with left cosets.

Equations

• hS.leftQuotientEquiv = (Equiv.ofBijective (S.restrict QuotientAddGroup.mk) ⋯).symm

theorem Subgroup.IsComplement.finite_left_iff {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : IsComplement S ↑H) : Finite ↑S ↔ H.FiniteIndex

A left transversal is finite iff the subgroup has finite index.

theorem AddSubgroup.IsComplement.finite_left_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (h : IsComplement S ↑H) : Finite ↑S ↔ H.FiniteIndex

A left transversal is finite iff the subgroup has finite index.

theorem Subgroup.IsComplement.finite_left {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} [H.FiniteIndex] (hS : IsComplement S ↑H) : S.Finite

theorem AddSubgroup.IsComplement.finite_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} [H.FiniteIndex] (hS : IsComplement S ↑H) : S.Finite

theorem Subgroup.IsComplement.quotientGroupMk_leftQuotientEquiv {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S ↑H) (q : G ⧸ H) : Quotient.mk'' ↑(hS.leftQuotientEquiv q) = q

theorem AddSubgroup.IsComplement.quotientAddGroupMk_leftQuotientEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : IsComplement S ↑H) (q : G ⧸ H) : Quotient.mk'' ↑(hS.leftQuotientEquiv q) = q

theorem Subgroup.IsComplement.leftQuotientEquiv_apply {G : Type u_1} [Group G] {H : Subgroup G} {f : G ⧸ H → G} (hf : ∀ (q : G ⧸ H), ↑(f q) = q) (q : G ⧸ H) : ↑(⋯.leftQuotientEquiv q) = f q

theorem AddSubgroup.IsComplement.leftQuotientEquiv_apply {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {f : G ⧸ H → G} (hf : ∀ (q : G ⧸ H), ↑(f q) = q) (q : G ⧸ H) : ↑(⋯.leftQuotientEquiv q) = f q

noncomputable def Subgroup.IsComplement.toLeftFun {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S ↑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

• hS.toLeftFun = ⇑hS.leftQuotientEquiv ∘ Quotient.mk''

noncomputable def AddSubgroup.IsComplement.toLeftFun {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : IsComplement S ↑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

• hS.toLeftFun = ⇑hS.leftQuotientEquiv ∘ Quotient.mk''

theorem Subgroup.IsComplement.inv_toLeftFun_mul_mem {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S ↑H) (g : G) : (↑(hS.toLeftFun g))⁻¹ * g ∈ H

theorem AddSubgroup.IsComplement.neg_toLeftFun_add_mem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : IsComplement S ↑H) (g : G) : -↑(hS.toLeftFun g) + g ∈ H

theorem Subgroup.IsComplement.inv_mul_toLeftFun_mem {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsComplement S ↑H) (g : G) : g⁻¹ * ↑(hS.toLeftFun g) ∈ H

theorem AddSubgroup.IsComplement.neg_add_toLeftFun_mem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : IsComplement S ↑H) (g : G) : -g + ↑(hS.toLeftFun g) ∈ H

noncomputable def Subgroup.IsComplement.rightQuotientEquiv {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hT : IsComplement (↑H) T) : Quotient (QuotientGroup.rightRel H) ≃ ↑T

A right transversal is in bijection with right cosets.

Equations

• hT.rightQuotientEquiv = (Equiv.ofBijective (T.restrict Quotient.mk'') ⋯).symm

noncomputable def AddSubgroup.IsComplement.rightQuotientEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : IsComplement (↑H) T) : Quotient (QuotientAddGroup.rightRel H) ≃ ↑T

A right transversal is in bijection with right cosets.

Equations

• hT.rightQuotientEquiv = (Equiv.ofBijective (T.restrict Quotient.mk'') ⋯).symm

theorem Subgroup.IsComplement.finite_right_iff {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (h : IsComplement (↑H) T) : Finite ↑T ↔ H.FiniteIndex

A right transversal is finite iff the subgroup has finite index.

theorem AddSubgroup.IsComplement.finite_right_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (h : IsComplement (↑H) T) : Finite ↑T ↔ H.FiniteIndex

A right transversal is finite iff the subgroup has finite index.

theorem Subgroup.IsComplement.finite_right {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} [H.FiniteIndex] (hT : IsComplement (↑H) T) : T.Finite

theorem AddSubgroup.IsComplement.finite_right {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} [H.FiniteIndex] (hT : IsComplement (↑H) T) : T.Finite

theorem Subgroup.IsComplement.mk''_rightQuotientEquiv {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hT : IsComplement (↑H) T) (q : Quotient (QuotientGroup.rightRel H)) : Quotient.mk'' ↑(hT.rightQuotientEquiv q) = q

theorem AddSubgroup.IsComplement.mk''_rightQuotientEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : IsComplement (↑H) T) (q : Quotient (QuotientAddGroup.rightRel H)) : Quotient.mk'' ↑(hT.rightQuotientEquiv q) = q

theorem Subgroup.IsComplement.rightQuotientEquiv_apply {G : Type u_1} [Group G] {H : Subgroup G} {f : Quotient (QuotientGroup.rightRel H) → G} (hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q) (q : Quotient (QuotientGroup.rightRel H)) : ↑(⋯.rightQuotientEquiv q) = f q

theorem AddSubgroup.IsComplement.rightQuotientEquiv_apply {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {f : Quotient (QuotientAddGroup.rightRel H) → G} (hf : ∀ (q : Quotient (QuotientAddGroup.rightRel H)), Quotient.mk'' (f q) = q) (q : Quotient (QuotientAddGroup.rightRel H)) : ↑(⋯.rightQuotientEquiv q) = f q

noncomputable def Subgroup.IsComplement.toRightFun {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hT : IsComplement (↑H) T) : G → ↑T

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

Equations

• hT.toRightFun = ⇑hT.rightQuotientEquiv ∘ Quotient.mk''

noncomputable def AddSubgroup.IsComplement.toRightFun {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : IsComplement (↑H) T) : G → ↑T

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

Equations

• hT.toRightFun = ⇑hT.rightQuotientEquiv ∘ Quotient.mk''

theorem Subgroup.IsComplement.mul_inv_toRightFun_mem {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hT : IsComplement (↑H) T) (g : G) : g * (↑(hT.toRightFun g))⁻¹ ∈ H

theorem AddSubgroup.IsComplement.add_neg_toRightFun_mem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : IsComplement (↑H) T) (g : G) : g + -↑(hT.toRightFun g) ∈ H

theorem Subgroup.IsComplement.toRightFun_mul_inv_mem {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hT : IsComplement (↑H) T) (g : G) : ↑(hT.toRightFun g) * g⁻¹ ∈ H

theorem AddSubgroup.IsComplement.toRightFun_add_neg_mem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : IsComplement (↑H) T) (g : G) : ↑(hT.toRightFun g) + -g ∈ H

theorem Subgroup.IsComplement.encard_left {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} [H.FiniteIndex] (h : IsComplement S ↑H) : S.encard = ↑H.index

theorem AddSubgroup.IsComplement.encard_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} [H.FiniteIndex] (h : IsComplement S ↑H) : S.encard = ↑H.index

theorem Subgroup.IsComplement.encard_right {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} [H.FiniteIndex] (h : IsComplement (↑H) T) : T.encard = ↑H.index

theorem AddSubgroup.IsComplement.encard_right {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {T : Set G} [H.FiniteIndex] (h : IsComplement (↑H) T) : T.encard = ↑H.index

@[reducible, inline]

abbrev Subgroup.LeftTransversal {G : Type u_1} [Group G] (H : Subgroup G) : Type u_1

The collection of left transversals of a subgroup

Equations

• H.LeftTransversal = { S : Set G // Subgroup.IsComplement S ↑H }

@[reducible, inline]

abbrev AddSubgroup.LeftTransversal {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Type u_1

The collection of left transversals of a subgroup.

Equations

• H.LeftTransversal = { S : Set G // AddSubgroup.IsComplement S ↑H }

@[reducible, inline]

abbrev Subgroup.RightTransversal {G : Type u_1} [Group G] (H : Subgroup G) : Type u_1

The collection of right transversals of a subgroup

Equations

• H.RightTransversal = { T : Set G // Subgroup.IsComplement (↑H) T }

@[reducible, inline]

abbrev AddSubgroup.RightTransversal {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Type u_1

The collection of right transversals of a subgroup.

Equations

• H.RightTransversal = { T : Set G // AddSubgroup.IsComplement (↑H) T }

noncomputable instance Subgroup.instMulActionLeftTransversal {G : Type u_1} [Group G] {H : Subgroup G} {F : Type u_2} [Group F] [MulAction F G] [MulAction.QuotientAction F H] : MulAction F H.LeftTransversal

Equations

• Subgroup.instMulActionLeftTransversal = { smul := fun (f : F) (T : H.LeftTransversal) => ⟨f • ↑T, ⋯⟩, mul_smul := ⋯, one_smul := ⋯ }

noncomputable instance AddSubgroup.instAddActionLeftTransversal {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {F : Type u_2} [AddGroup F] [AddAction F G] [AddAction.QuotientAction F H] : AddAction F H.LeftTransversal

Equations

• AddSubgroup.instAddActionLeftTransversal = { vadd := fun (f : F) (T : H.LeftTransversal) => ⟨f +ᵥ ↑T, ⋯⟩, add_vadd := ⋯, zero_vadd := ⋯ }

theorem Subgroup.smul_toLeftFun {G : Type u_1} [Group G] {H : Subgroup G} {F : Type u_2} [Group F] [MulAction F G] [MulAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (g : G) : f • ↑(⋯.toLeftFun g) = ↑(⋯.toLeftFun (f • g))

theorem AddSubgroup.vadd_toLeftFun {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {F : Type u_2} [AddGroup F] [AddAction F G] [AddAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (g : G) : f +ᵥ ↑(⋯.toLeftFun g) = ↑(⋯.toLeftFun (f +ᵥ g))

theorem Subgroup.smul_leftQuotientEquiv {G : Type u_1} [Group G] {H : Subgroup G} {F : Type u_2} [Group F] [MulAction F G] [MulAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (q : G ⧸ H) : f • ↑(⋯.leftQuotientEquiv q) = ↑(⋯.leftQuotientEquiv (f • q))

theorem AddSubgroup.vadd_leftQuotientEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {F : Type u_2} [AddGroup F] [AddAction F G] [AddAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (q : G ⧸ H) : f +ᵥ ↑(⋯.leftQuotientEquiv q) = ↑(⋯.leftQuotientEquiv (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] [MulAction F G] [MulAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (q : G ⧸ H) : ↑(⋯.leftQuotientEquiv q) = f • ↑(⋯.leftQuotientEquiv (f⁻¹ • q))

theorem AddSubgroup.vadd_apply_eq_vadd_apply_neg_vadd {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {F : Type u_2} [AddGroup F] [AddAction F G] [AddAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (q : G ⧸ H) : ↑(⋯.leftQuotientEquiv q) = f +ᵥ ↑(⋯.leftQuotientEquiv (-f +ᵥ q))

instance Subgroup.instInhabitedLeftTransversal {G : Type u_1} [Group G] {H : Subgroup G} : Inhabited H.LeftTransversal

Equations

• Subgroup.instInhabitedLeftTransversal = { default := ⟨Set.range Quotient.out, ⋯⟩ }

instance AddSubgroup.instInhabitedLeftTransversal {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : Inhabited H.LeftTransversal

Equations

• AddSubgroup.instInhabitedLeftTransversal = { default := ⟨Set.range Quotient.out, ⋯⟩ }

instance Subgroup.instInhabitedRightTransversal {G : Type u_1} [Group G] {H : Subgroup G} : Inhabited H.RightTransversal

Equations

• Subgroup.instInhabitedRightTransversal = { default := ⟨Set.range Quotient.out, ⋯⟩ }

instance AddSubgroup.instInhabitedRightTransversal {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : Inhabited H.RightTransversal

Equations

• AddSubgroup.instInhabitedRightTransversal = { default := ⟨Set.range Quotient.out, ⋯⟩ }

theorem Subgroup.IsComplement'.isCompl {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.IsComplement' K) : IsCompl H K

theorem Subgroup.IsComplement'.sup_eq_top {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.IsComplement' K) : H ⊔ K = ⊤

theorem Subgroup.IsComplement'.disjoint {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.IsComplement' K) : Disjoint H K

theorem Subgroup.IsComplement'.index_eq_card {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.IsComplement' K) : K.index = Nat.card ↥H

noncomputable def Subgroup.IsComplement'.QuotientMulEquiv {G : Type u_1} [Group G] {H K : Subgroup G} [K.Normal] (h : H.IsComplement' K) : G ⧸ K ≃* ↥H

If H and K are complementary with K normal, then G ⧸ K is isomorphic to H.

Equations

• h.QuotientMulEquiv = (let __src := (Subgroup.IsComplement.leftQuotientEquiv h).symm; { toEquiv := __src, map_mul' := ⋯ }).symm

@[simp]

theorem Subgroup.IsComplement'.QuotientMulEquiv_symm_apply {G : Type u_1} [Group G] {H K : Subgroup G} [K.Normal] (h : H.IsComplement' K) (a✝ : ↥H) : h.QuotientMulEquiv.symm a✝ = (IsComplement.leftQuotientEquiv h).symm a✝

@[simp]

theorem Subgroup.IsComplement'.QuotientMulEquiv_apply {G : Type u_1} [Group G] {H K : Subgroup G} [K.Normal] (h : H.IsComplement' K) (a✝ : G ⧸ K) : h.QuotientMulEquiv a✝ = (IsComplement.leftQuotientEquiv h) a✝

theorem Subgroup.IsComplement.card_mul {G : Type u_1} [Group G] {S T : Set G} (h : IsComplement S T) : Nat.card ↑S * Nat.card ↑T = Nat.card G

theorem Subgroup.IsComplement'.card_mul {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.IsComplement' K) : Nat.card ↥H * Nat.card ↥K = Nat.card G

theorem Subgroup.isComplement'_of_disjoint_and_mul_eq_univ {G : Type u_1} [Group G] {H K : Subgroup G} (h1 : Disjoint H K) (h2 : ↑H * ↑K = Set.univ) : H.IsComplement' K

theorem Subgroup.isComplement'_of_card_mul_and_disjoint {G : Type u_1} [Group G] {H K : Subgroup G} [Finite G] (h1 : Nat.card ↥H * Nat.card ↥K = Nat.card G) (h2 : Disjoint H K) : H.IsComplement' K

theorem Subgroup.isComplement'_iff_card_mul_and_disjoint {G : Type u_1} [Group G] {H K : Subgroup G} [Finite G] : H.IsComplement' K ↔ Nat.card ↥H * Nat.card ↥K = Nat.card G ∧ Disjoint H K

theorem Subgroup.isComplement'_of_coprime {G : Type u_1} [Group G] {H K : Subgroup G} [Finite G] (h1 : Nat.card ↥H * Nat.card ↥K = Nat.card G) (h2 : (Nat.card ↥H).Coprime (Nat.card ↥K)) : H.IsComplement' K

theorem Subgroup.isComplement'_stabilizer {G : Type u_1} [Group G] {H : Subgroup G} {α : Type u_2} [MulAction G α] (a : α) (h1 : ∀ (h : ↥H), h • a = a → h = 1) (h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a) : H.IsComplement' (MulAction.stabilizer G a)