Complements

In this file we define the complement of a subgroup.

Main definitions

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

Main results

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

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

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

Equations

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

def Subgroup.IsComplement {G : Type u_1} [Group G] (S : Set G) (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.IsComplement S T = Function.Bijective fun (x : ↑S × ↑T) => ↑x.1 * ↑x.2

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

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

The set of left-complements of T : Set G

Equations

• AddSubgroup.leftTransversals T = {S : Set G | AddSubgroup.IsComplement S T}

def Subgroup.leftTransversals {G : Type u_1} [Group G] (T : Set G) : Set (Set G)

The set of left-complements of T : Set G

Equations

• Subgroup.leftTransversals T = {S : Set G | Subgroup.IsComplement S T}

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

The set of right-complements of S : Set G

Equations

• AddSubgroup.rightTransversals S = {T : Set G | AddSubgroup.IsComplement S T}

def Subgroup.rightTransversals {G : Type u_1} [Group G] (S : Set G) : Set (Set G)

The set of right-complements of S : Set G

Equations

• Subgroup.rightTransversals S = {T : Set G | Subgroup.IsComplement S T}

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

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

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

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

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

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

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

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

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

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

abbrev AddSubgroup.isComplement_univ_singleton.match_1 {G : Type u_1} [AddGroup G] {g : G} : ∀ (fst : ↑Set.univ) (motive : (x : ↑Set.univ × ↑{g}) → (fun (x : ↑Set.univ × ↑{g}) => ↑x.1 + ↑x.2) (fst, ⟨g, ⋯⟩) = (fun (x : ↑Set.univ × ↑{g}) => ↑x.1 + ↑x.2) x → Prop) (x : ↑Set.univ × ↑{g}) (h : (fun (x : ↑Set.univ × ↑{g}) => ↑x.1 + ↑x.2) (fst, ⟨g, ⋯⟩) = (fun (x : ↑Set.univ × ↑{g}) => ↑x.1 + ↑x.2) x), (∀ (fst_1 : ↑Set.univ) (h : (fun (x : ↑Set.univ × ↑{g}) => ↑x.1 + ↑x.2) (fst, ⟨g, ⋯⟩) = (fun (x : ↑Set.univ × ↑{g}) => ↑x.1 + ↑x.2) (fst_1, ⟨g, ⋯⟩)), motive (fst_1, ⟨g, ⋯⟩) h) → motive x h

Equations

• ⋯ = ⋯

abbrev AddSubgroup.isComplement_univ_singleton.match_2 {G : Type u_1} [AddGroup G] {g : G} : ∀ (x : ↑Set.univ × ↑{g}) (motive : (x_1 : ↑Set.univ × ↑{g}) → (fun (x : ↑Set.univ × ↑{g}) => ↑x.1 + ↑x.2) x_1 = (fun (x : ↑Set.univ × ↑{g}) => ↑x.1 + ↑x.2) x → Prop) (x_1 : ↑Set.univ × ↑{g}) (h : (fun (x : ↑Set.univ × ↑{g}) => ↑x.1 + ↑x.2) x_1 = (fun (x : ↑Set.univ × ↑{g}) => ↑x.1 + ↑x.2) x), (∀ (fst : ↑Set.univ) (h : (fun (x : ↑Set.univ × ↑{g}) => ↑x.1 + ↑x.2) (fst, ⟨g, ⋯⟩) = (fun (x : ↑Set.univ × ↑{g}) => ↑x.1 + ↑x.2) x), motive (fst, ⟨g, ⋯⟩) h) → motive x_1 h

Equations

• ⋯ = ⋯

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

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

abbrev AddSubgroup.isComplement_singleton_univ.match_2 {G : Type u_1} [AddGroup G] {g : G} : ∀ (x : ↑{g} × ↑Set.univ) (motive : (x_1 : ↑{g} × ↑Set.univ) → (fun (x : ↑{g} × ↑Set.univ) => ↑x.1 + ↑x.2) x_1 = (fun (x : ↑{g} × ↑Set.univ) => ↑x.1 + ↑x.2) x → Prop) (x_1 : ↑{g} × ↑Set.univ) (h : (fun (x : ↑{g} × ↑Set.univ) => ↑x.1 + ↑x.2) x_1 = (fun (x : ↑{g} × ↑Set.univ) => ↑x.1 + ↑x.2) x), (∀ (snd : ↑Set.univ) (h : (fun (x : ↑{g} × ↑Set.univ) => ↑x.1 + ↑x.2) (⟨g, ⋯⟩, snd) = (fun (x : ↑{g} × ↑Set.univ) => ↑x.1 + ↑x.2) x), motive (⟨g, ⋯⟩, snd) h) → motive x_1 h

Equations

• ⋯ = ⋯

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

abbrev AddSubgroup.isComplement_singleton_univ.match_1 {G : Type u_1} [AddGroup G] {g : G} : ∀ (snd : ↑Set.univ) (motive : (x : ↑{g} × ↑Set.univ) → (fun (x : ↑{g} × ↑Set.univ) => ↑x.1 + ↑x.2) (⟨g, ⋯⟩, snd) = (fun (x : ↑{g} × ↑Set.univ) => ↑x.1 + ↑x.2) x → Prop) (x : ↑{g} × ↑Set.univ) (h : (fun (x : ↑{g} × ↑Set.univ) => ↑x.1 + ↑x.2) (⟨g, ⋯⟩, snd) = (fun (x : ↑{g} × ↑Set.univ) => ↑x.1 + ↑x.2) x), (∀ (snd_1 : ↑Set.univ) (h : (fun (x : ↑{g} × ↑Set.univ) => ↑x.1 + ↑x.2) (⟨g, ⋯⟩, snd) = (fun (x : ↑{g} × ↑Set.univ) => ↑x.1 + ↑x.2) (⟨g, ⋯⟩, snd_1)), motive (⟨g, ⋯⟩, snd_1) h) → motive x h

Equations

• ⋯ = ⋯

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem AddSubgroup.mem_leftTransversals_iff_existsUnique_quotient_mk''_eq {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} : S ∈ AddSubgroup.leftTransversals ↑H ↔ ∀ (q : Quotient (QuotientAddGroup.leftRel H)), ∃! s : ↑S, Quotient.mk'' ↑s = q

theorem Subgroup.mem_leftTransversals_iff_existsUnique_quotient_mk''_eq {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} : S ∈ Subgroup.leftTransversals ↑H ↔ ∀ (q : Quotient (QuotientGroup.leftRel H)), ∃! s : ↑S, Quotient.mk'' ↑s = q

theorem AddSubgroup.mem_rightTransversals_iff_existsUnique_quotient_mk''_eq {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} : S ∈ AddSubgroup.rightTransversals ↑H ↔ ∀ (q : Quotient (QuotientAddGroup.rightRel H)), ∃! s : ↑S, Quotient.mk'' ↑s = q

theorem Subgroup.mem_rightTransversals_iff_existsUnique_quotient_mk''_eq {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} : S ∈ Subgroup.rightTransversals ↑H ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! s : ↑S, Quotient.mk'' ↑s = q

theorem AddSubgroup.mem_leftTransversals_iff_bijective {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} : S ∈ AddSubgroup.leftTransversals ↑H ↔ Function.Bijective (S.restrict Quotient.mk'')

theorem Subgroup.mem_leftTransversals_iff_bijective {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} : S ∈ Subgroup.leftTransversals ↑H ↔ Function.Bijective (S.restrict Quotient.mk'')

theorem AddSubgroup.mem_rightTransversals_iff_bijective {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} : S ∈ AddSubgroup.rightTransversals ↑H ↔ Function.Bijective (S.restrict Quotient.mk'')

theorem Subgroup.mem_rightTransversals_iff_bijective {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} : S ∈ Subgroup.rightTransversals ↑H ↔ Function.Bijective (S.restrict Quotient.mk'')

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

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

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

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

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

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

theorem AddSubgroup.range_mem_rightTransversals {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) : Set.range f ∈ AddSubgroup.rightTransversals ↑H

theorem Subgroup.range_mem_rightTransversals {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) : Set.range f ∈ Subgroup.rightTransversals ↑H

theorem AddSubgroup.exists_left_transversal {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (g : G) : ∃ S ∈ AddSubgroup.leftTransversals ↑H, g ∈ S

theorem Subgroup.exists_left_transversal {G : Type u_1} [Group G] (H : Subgroup G) (g : G) : ∃ S ∈ Subgroup.leftTransversals ↑H, g ∈ S

theorem AddSubgroup.exists_right_transversal {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (g : G) : ∃ S ∈ AddSubgroup.rightTransversals ↑H, g ∈ S

theorem Subgroup.exists_right_transversal {G : Type u_1} [Group G] (H : Subgroup G) (g : G) : ∃ S ∈ Subgroup.rightTransversals ↑H, g ∈ S

theorem AddSubgroup.exists_left_transversal_of_le {G : Type u_1} [AddGroup G] {H' : AddSubgroup G} {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_left_transversal_of_le {G : Type u_1} [Group G] {H' : Subgroup G} {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_right_transversal_of_le {G : Type u_1} [AddGroup G] {H' : AddSubgroup G} {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

theorem Subgroup.exists_right_transversal_of_le {G : Type u_1} [Group G] {H' : Subgroup G} {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.

noncomputable def Subgroup.IsComplement.equiv {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.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 : Set G} {T : Set G} (hST : Subgroup.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 : Set G} {T : Set G} (hST : Subgroup.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 : Set G} {T : Set G} (hST : Subgroup.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 : Set G} {T : Set G} (hST : Subgroup.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 : Subgroup.IsComplement S ↑K) {g₁ : 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 : Subgroup.IsComplement (↑H) T) {g₁ : 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 : Subgroup.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 : Subgroup.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 : Set G} {T : Set G} (hST : Subgroup.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 : Set G} {T : Set G} (hST : Subgroup.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 : Set G} {T : Set G} (hST : Subgroup.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 : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) : (hST.equiv g).1 = ⟨1, h1⟩

@[simp]

theorem Subgroup.IsComplement.equiv_mul_right {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : Subgroup.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 : Subgroup.IsComplement S ↑K) {g : G} {k : G} (h : k ∈ K) : hSK.equiv (g * k) = ((hSK.equiv g).1, (hSK.equiv g).2 * ⟨k, h⟩)

@[simp]

theorem Subgroup.IsComplement.equiv_mul_left {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hHT : Subgroup.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 : Subgroup.IsComplement (↑H) T) {h : G} {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 : Set G} {T : Set G} (hST : Subgroup.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 : Set G} {T : Set G} (hST : Subgroup.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 : Set G} {T : Set G} (hST : Subgroup.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 : Set G} {T : Set G} (hST : Subgroup.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 : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 ∈ T) : ↑(hST.equiv g).2 = 1 ↔ g ∈ S

noncomputable def AddSubgroup.MemLeftTransversals.toEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : S ∈ AddSubgroup.leftTransversals ↑H) : G ⧸ H ≃ ↑S

A left transversal is in bijection with left cosets.

Equations

• AddSubgroup.MemLeftTransversals.toEquiv hS = (Equiv.ofBijective (S.restrict Quotient.mk'') ⋯).symm

theorem AddSubgroup.MemLeftTransversals.toEquiv.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : S ∈ AddSubgroup.leftTransversals ↑H) : Function.Bijective (S.restrict Quotient.mk'')

noncomputable def Subgroup.MemLeftTransversals.toEquiv {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : S ∈ Subgroup.leftTransversals ↑H) : G ⧸ H ≃ ↑S

A left transversal is in bijection with left cosets.

Equations

• Subgroup.MemLeftTransversals.toEquiv hS = (Equiv.ofBijective (S.restrict Quotient.mk'') ⋯).symm

theorem AddSubgroup.MemLeftTransversals.finite_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (h : S ∈ AddSubgroup.leftTransversals ↑H) : Finite ↑S ↔ H.FiniteIndex

A left transversal is finite iff the subgroup has finite index

theorem Subgroup.MemLeftTransversals.finite_iff {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : S ∈ Subgroup.leftTransversals ↑H) : Finite ↑S ↔ H.FiniteIndex

theorem AddSubgroup.MemLeftTransversals.mk''_toEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : S ∈ AddSubgroup.leftTransversals ↑H) (q : G ⧸ H) : Quotient.mk'' ↑((AddSubgroup.MemLeftTransversals.toEquiv hS) q) = q

theorem Subgroup.MemLeftTransversals.mk''_toEquiv {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : S ∈ Subgroup.leftTransversals ↑H) (q : G ⧸ H) : Quotient.mk'' ↑((Subgroup.MemLeftTransversals.toEquiv hS) q) = q

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

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

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

• AddSubgroup.MemLeftTransversals.toFun hS = ⇑(AddSubgroup.MemLeftTransversals.toEquiv hS) ∘ Quotient.mk''

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

• Subgroup.MemLeftTransversals.toFun hS = ⇑(Subgroup.MemLeftTransversals.toEquiv hS) ∘ Quotient.mk''

theorem AddSubgroup.MemLeftTransversals.neg_toFun_add_mem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : S ∈ AddSubgroup.leftTransversals ↑H) (g : G) : -↑(AddSubgroup.MemLeftTransversals.toFun hS g) + g ∈ H

theorem Subgroup.MemLeftTransversals.inv_toFun_mul_mem {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : S ∈ Subgroup.leftTransversals ↑H) (g : G) : (↑(Subgroup.MemLeftTransversals.toFun hS g))⁻¹ * g ∈ H

theorem AddSubgroup.MemLeftTransversals.neg_add_toFun_mem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : S ∈ AddSubgroup.leftTransversals ↑H) (g : G) : -g + ↑(AddSubgroup.MemLeftTransversals.toFun hS g) ∈ H

theorem Subgroup.MemLeftTransversals.inv_mul_toFun_mem {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : S ∈ Subgroup.leftTransversals ↑H) (g : G) : g⁻¹ * ↑(Subgroup.MemLeftTransversals.toFun hS g) ∈ H

noncomputable def AddSubgroup.MemRightTransversals.toEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : S ∈ AddSubgroup.rightTransversals ↑H) : Quotient (QuotientAddGroup.rightRel H) ≃ ↑S

A right transversal is in bijection with right cosets.

Equations

• AddSubgroup.MemRightTransversals.toEquiv hS = (Equiv.ofBijective (S.restrict Quotient.mk'') ⋯).symm

theorem AddSubgroup.MemRightTransversals.toEquiv.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : S ∈ AddSubgroup.rightTransversals ↑H) : Function.Bijective (S.restrict Quotient.mk'')

noncomputable def Subgroup.MemRightTransversals.toEquiv {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : S ∈ Subgroup.rightTransversals ↑H) : Quotient (QuotientGroup.rightRel H) ≃ ↑S

A right transversal is in bijection with right cosets.

Equations

• Subgroup.MemRightTransversals.toEquiv hS = (Equiv.ofBijective (S.restrict Quotient.mk'') ⋯).symm

theorem AddSubgroup.MemRightTransversals.finite_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (h : S ∈ AddSubgroup.rightTransversals ↑H) : Finite ↑S ↔ H.FiniteIndex

A right transversal is finite iff the subgroup has finite index

theorem Subgroup.MemRightTransversals.finite_iff {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : S ∈ Subgroup.rightTransversals ↑H) : Finite ↑S ↔ H.FiniteIndex

theorem AddSubgroup.MemRightTransversals.mk''_toEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : S ∈ AddSubgroup.rightTransversals ↑H) (q : Quotient (QuotientAddGroup.rightRel H)) : Quotient.mk'' ↑((AddSubgroup.MemRightTransversals.toEquiv hS) q) = q

theorem Subgroup.MemRightTransversals.mk''_toEquiv {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : S ∈ Subgroup.rightTransversals ↑H) (q : Quotient (QuotientGroup.rightRel H)) : Quotient.mk'' ↑((Subgroup.MemRightTransversals.toEquiv hS) q) = q

theorem AddSubgroup.MemRightTransversals.toEquiv_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)) : ↑((AddSubgroup.MemRightTransversals.toEquiv ⋯) q) = f q

theorem Subgroup.MemRightTransversals.toEquiv_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)) : ↑((Subgroup.MemRightTransversals.toEquiv ⋯) q) = f q

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

• AddSubgroup.MemRightTransversals.toFun hS = ⇑(AddSubgroup.MemRightTransversals.toEquiv hS) ∘ Quotient.mk''

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

• Subgroup.MemRightTransversals.toFun hS = ⇑(Subgroup.MemRightTransversals.toEquiv hS) ∘ Quotient.mk''

theorem AddSubgroup.MemRightTransversals.add_neg_toFun_mem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : S ∈ AddSubgroup.rightTransversals ↑H) (g : G) : g + -↑(AddSubgroup.MemRightTransversals.toFun hS g) ∈ H

theorem Subgroup.MemRightTransversals.mul_inv_toFun_mem {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : S ∈ Subgroup.rightTransversals ↑H) (g : G) : g * (↑(Subgroup.MemRightTransversals.toFun hS g))⁻¹ ∈ H

theorem AddSubgroup.MemRightTransversals.toFun_add_neg_mem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : S ∈ AddSubgroup.rightTransversals ↑H) (g : G) : ↑(AddSubgroup.MemRightTransversals.toFun hS g) + -g ∈ H

theorem Subgroup.MemRightTransversals.toFun_mul_inv_mem {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : S ∈ Subgroup.rightTransversals ↑H) (g : G) : ↑(Subgroup.MemRightTransversals.toFun hS g) * g⁻¹ ∈ H

theorem AddSubgroup.instAddActionElemSetLeftTransversalsCoe.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {F : Type u_2} [AddGroup F] [AddAction F G] [AddAction.QuotientAction F H] (f : F) (T : ↑(AddSubgroup.leftTransversals ↑H)) : f +ᵥ ↑T ∈ AddSubgroup.leftTransversals ↑H

theorem AddSubgroup.instAddActionElemSetLeftTransversalsCoe.proof_2 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {F : Type u_2} [AddGroup F] [AddAction F G] [AddAction.QuotientAction F H] (T : ↑(AddSubgroup.leftTransversals ↑H)) : 0 +ᵥ T = T

noncomputable instance AddSubgroup.instAddActionElemSetLeftTransversalsCoe {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {F : Type u_2} [AddGroup F] [AddAction F G] [AddAction.QuotientAction F H] : AddAction F ↑(AddSubgroup.leftTransversals ↑H)

Equations

• AddSubgroup.instAddActionElemSetLeftTransversalsCoe = AddAction.mk ⋯ ⋯

theorem AddSubgroup.instAddActionElemSetLeftTransversalsCoe.proof_3 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {F : Type u_2} [AddGroup F] [AddAction F G] [AddAction.QuotientAction F H] (f₁ : F) (f₂ : F) (T : ↑(AddSubgroup.leftTransversals ↑H)) : f₁ + f₂ +ᵥ T = f₁ +ᵥ (f₂ +ᵥ T)

noncomputable instance Subgroup.instMulActionElemSetLeftTransversalsCoe {G : Type u_1} [Group G] {H : Subgroup G} {F : Type u_2} [Group F] [MulAction F G] [MulAction.QuotientAction F H] : MulAction F ↑(Subgroup.leftTransversals ↑H)

Equations

• Subgroup.instMulActionElemSetLeftTransversalsCoe = MulAction.mk ⋯ ⋯

theorem AddSubgroup.vadd_toFun {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {F : Type u_2} [AddGroup F] [AddAction F G] [AddAction.QuotientAction F H] (f : F) (T : ↑(AddSubgroup.leftTransversals ↑H)) (g : G) : f +ᵥ ↑(AddSubgroup.MemLeftTransversals.toFun ⋯ g) = ↑(AddSubgroup.MemLeftTransversals.toFun ⋯ (f +ᵥ g))

theorem Subgroup.smul_toFun {G : Type u_1} [Group G] {H : Subgroup G} {F : Type u_2} [Group F] [MulAction F G] [MulAction.QuotientAction F H] (f : F) (T : ↑(Subgroup.leftTransversals ↑H)) (g : G) : f • ↑(Subgroup.MemLeftTransversals.toFun ⋯ g) = ↑(Subgroup.MemLeftTransversals.toFun ⋯ (f • g))

theorem AddSubgroup.vadd_toEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {F : Type u_2} [AddGroup F] [AddAction F G] [AddAction.QuotientAction F H] (f : F) (T : ↑(AddSubgroup.leftTransversals ↑H)) (q : G ⧸ H) : f +ᵥ ↑((AddSubgroup.MemLeftTransversals.toEquiv ⋯) q) = ↑((AddSubgroup.MemLeftTransversals.toEquiv ⋯) (f +ᵥ q))

theorem Subgroup.smul_toEquiv {G : Type u_1} [Group G] {H : Subgroup G} {F : Type u_2} [Group F] [MulAction F G] [MulAction.QuotientAction F H] (f : F) (T : ↑(Subgroup.leftTransversals ↑H)) (q : G ⧸ H) : f • ↑((Subgroup.MemLeftTransversals.toEquiv ⋯) q) = ↑((Subgroup.MemLeftTransversals.toEquiv ⋯) (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) (T : ↑(AddSubgroup.leftTransversals ↑H)) (q : G ⧸ H) : ↑((AddSubgroup.MemLeftTransversals.toEquiv ⋯) q) = f +ᵥ ↑((AddSubgroup.MemLeftTransversals.toEquiv ⋯) (-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) (T : ↑(Subgroup.leftTransversals ↑H)) (q : G ⧸ H) : ↑((Subgroup.MemLeftTransversals.toEquiv ⋯) q) = f • ↑((Subgroup.MemLeftTransversals.toEquiv ⋯) (f⁻¹ • q))

theorem AddSubgroup.instInhabitedElemSetLeftTransversalsCoe.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : Set.range Quotient.out' ∈ AddSubgroup.leftTransversals ↑H

instance AddSubgroup.instInhabitedElemSetLeftTransversalsCoe {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : Inhabited ↑(AddSubgroup.leftTransversals ↑H)

Equations

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

instance Subgroup.instInhabitedElemSetLeftTransversalsCoe {G : Type u_1} [Group G] {H : Subgroup G} : Inhabited ↑(Subgroup.leftTransversals ↑H)

Equations

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

instance AddSubgroup.instInhabitedElemSetRightTransversalsCoe {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : Inhabited ↑(AddSubgroup.rightTransversals ↑H)

Equations

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

theorem AddSubgroup.instInhabitedElemSetRightTransversalsCoe.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : Set.range Quotient.out' ∈ AddSubgroup.rightTransversals ↑H

instance Subgroup.instInhabitedElemSetRightTransversalsCoe {G : Type u_1} [Group G] {H : Subgroup G} : Inhabited ↑(Subgroup.rightTransversals ↑H)

Equations

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

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

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

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

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

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

theorem Subgroup.IsComplement'.card_mul {G : Type u_1} [Group G] {H : Subgroup G} {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 : Subgroup G} {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 : Subgroup G} {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 : Subgroup G} {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 : Subgroup G} {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)

noncomputable def Subgroup.quotientEquivSigmaZMod {G : Type u} [Group G] (H : Subgroup G) (g : G) : G ⧸ H ≃ (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) × ZMod (Function.minimalPeriod (fun (x : G ⧸ H) => g • x) (Quotient.out' q))

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

Equations

• One or more equations did not get rendered due to their size.

theorem Subgroup.quotientEquivSigmaZMod_symm_apply {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) (k : ZMod (Function.minimalPeriod (fun (x : G ⧸ H) => g • x) (Quotient.out' q))) : (H.quotientEquivSigmaZMod g).symm ⟨q, k⟩ = g ^ k.cast • Quotient.out' q

theorem Subgroup.quotientEquivSigmaZMod_apply {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) (k : ℤ) : (H.quotientEquivSigmaZMod g) (g ^ k • Quotient.out' q) = ⟨q, ↑k⟩

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

• H.transferFunction g q = g ^ ((H.quotientEquivSigmaZMod g) q).snd.cast * Quotient.out' (Quotient.out' ((H.quotientEquivSigmaZMod g) q).fst)

theorem Subgroup.transferFunction_apply {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : G ⧸ H) : H.transferFunction g q = g ^ ((H.quotientEquivSigmaZMod g) q).snd.cast * Quotient.out' (Quotient.out' ((H.quotientEquivSigmaZMod g) q).fst)

theorem Subgroup.coe_transferFunction {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : G ⧸ H) : ↑(H.transferFunction g q) = q

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

• H.transferSet g = Set.range (H.transferFunction g)

theorem Subgroup.mem_transferSet {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : G ⧸ H) : H.transferFunction g q ∈ H.transferSet g

def Subgroup.transferTransversal {G : Type u} [Group G] (H : Subgroup G) (g : G) : ↑(Subgroup.leftTransversals ↑H)

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

• H.transferTransversal g = ⟨H.transferSet g, ⋯⟩

theorem Subgroup.transferTransversal_apply {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : G ⧸ H) : ↑((Subgroup.MemLeftTransversals.toEquiv ⋯) q) = H.transferFunction g q

theorem Subgroup.transferTransversal_apply' {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) (k : ZMod (Function.minimalPeriod (fun (x : G ⧸ H) => g • x) (Quotient.out' q))) : ↑((Subgroup.MemLeftTransversals.toEquiv ⋯) (g ^ k.cast • Quotient.out' q)) = g ^ k.cast * Quotient.out' (Quotient.out' q)

theorem Subgroup.transferTransversal_apply'' {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) (k : ZMod (Function.minimalPeriod (fun (x : G ⧸ H) => g • x) (Quotient.out' q))) : ↑((Subgroup.MemLeftTransversals.toEquiv ⋯) (g ^ k.cast • Quotient.out' q)) = if k = 0 then g ^ Function.minimalPeriod (fun (x : G ⧸ H) => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q) else g ^ k.cast * Quotient.out' (Quotient.out' q)