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} [] (S : Set G) (T : Set G) :

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

Equations
Instances For
def Subgroup.IsComplement {G : Type u_1} [] (S : Set G) (T : Set G) :

S and T are complements if (*) : S × T → G is a bijection. This notion generalizes left transversals, right transversals, and complementary subgroups.

Equations
Instances For
@[reducible, inline]
abbrev AddSubgroup.IsComplement' {G : Type u_1} [] (H : ) (K : ) :

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

Equations
• H.IsComplement' K =
Instances For
@[reducible, inline]
abbrev Subgroup.IsComplement' {G : Type u_1} [] (H : ) (K : ) :

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

Equations
• H.IsComplement' K =
Instances For
def AddSubgroup.leftTransversals {G : Type u_1} [] (T : Set G) :
Set (Set G)

The set of left-complements of T : Set G

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

The set of left-complements of T : Set G

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

The set of right-complements of S : Set G

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

The set of right-complements of S : Set G

Equations
Instances For
theorem AddSubgroup.isComplement'_def {G : Type u_1} [] {H : } {K : } :
H.IsComplement' K
theorem Subgroup.isComplement'_def {G : Type u_1} [] {H : } {K : } :
H.IsComplement' K
theorem AddSubgroup.isComplement_iff_existsUnique {G : Type u_1} [] {S : Set G} {T : Set G} :
∀ (g : G), ∃! x : S × T, x.1 + x.2 = g
theorem Subgroup.isComplement_iff_existsUnique {G : Type u_1} [] {S : Set G} {T : Set G} :
∀ (g : G), ∃! x : S × T, x.1 * x.2 = g
theorem AddSubgroup.IsComplement.existsUnique {G : Type u_1} [] {S : Set G} {T : Set G} (h : ) (g : G) :
∃! x : S × T, x.1 + x.2 = g
theorem Subgroup.IsComplement.existsUnique {G : Type u_1} [] {S : Set G} {T : Set G} (h : ) (g : G) :
∃! x : S × T, x.1 * x.2 = g
theorem AddSubgroup.IsComplement'.symm {G : Type u_1} [] {H : } {K : } (h : H.IsComplement' K) :
K.IsComplement' H
theorem Subgroup.IsComplement'.symm {G : Type u_1} [] {H : } {K : } (h : H.IsComplement' K) :
K.IsComplement' H
theorem AddSubgroup.isComplement'_comm {G : Type u_1} [] {H : } {K : } :
H.IsComplement' K K.IsComplement' H
theorem Subgroup.isComplement'_comm {G : Type u_1} [] {H : } {K : } :
H.IsComplement' K K.IsComplement' H
@[inline]
abbrev AddSubgroup.isComplement_univ_singleton.match_1 {G : Type u_1} [] {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) xProp) (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
• =
Instances For
@[inline]
abbrev AddSubgroup.isComplement_univ_singleton.match_2 {G : Type u_1} [] {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) xProp) (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
• =
Instances For
theorem Subgroup.isComplement_univ_singleton {G : Type u_1} [] {g : G} :
@[inline]
abbrev AddSubgroup.isComplement_singleton_univ.match_2 {G : Type u_1} [] {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) xProp) (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
• =
Instances For
@[inline]
abbrev AddSubgroup.isComplement_singleton_univ.match_1 {G : Type u_1} [] {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) xProp) (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
• =
Instances For
theorem Subgroup.isComplement_singleton_univ {G : Type u_1} [] {g : G} :
theorem AddSubgroup.isComplement_singleton_left {G : Type u_1} [] {S : Set G} {g : G} :
S = Set.univ
theorem Subgroup.isComplement_singleton_left {G : Type u_1} [] {S : Set G} {g : G} :
S = Set.univ
theorem AddSubgroup.isComplement_singleton_right {G : Type u_1} [] {S : Set G} {g : G} :
S = Set.univ
theorem Subgroup.isComplement_singleton_right {G : Type u_1} [] {S : Set G} {g : G} :
S = Set.univ
theorem AddSubgroup.isComplement_univ_left {G : Type u_1} [] {S : Set G} :
AddSubgroup.IsComplement Set.univ S ∃ (g : G), S = {g}
theorem Subgroup.isComplement_univ_left {G : Type u_1} [] {S : Set G} :
Subgroup.IsComplement Set.univ S ∃ (g : G), S = {g}
theorem AddSubgroup.isComplement_univ_right {G : Type u_1} [] {S : Set G} :
AddSubgroup.IsComplement S Set.univ ∃ (g : G), S = {g}
theorem Subgroup.isComplement_univ_right {G : Type u_1} [] {S : Set G} :
Subgroup.IsComplement S Set.univ ∃ (g : G), S = {g}
theorem AddSubgroup.IsComplement.add_eq {G : Type u_1} [] {S : Set G} {T : Set G} (h : ) :
S + T = Set.univ
theorem Subgroup.IsComplement.mul_eq {G : Type u_1} [] {S : Set G} {T : Set G} (h : ) :
S * T = Set.univ
theorem AddSubgroup.IsComplement.card_mul_card {G : Type u_1} [] {S : Set G} {T : Set G} (h : ) :
Nat.card S * Nat.card T =
theorem Subgroup.IsComplement.card_mul_card {G : Type u_1} [] {S : Set G} {T : Set G} (h : ) :
Nat.card S * Nat.card T =
theorem AddSubgroup.isComplement'_top_bot {G : Type u_1} [] :
.IsComplement'
theorem Subgroup.isComplement'_top_bot {G : Type u_1} [] :
.IsComplement'
theorem AddSubgroup.isComplement'_bot_top {G : Type u_1} [] :
.IsComplement'
theorem Subgroup.isComplement'_bot_top {G : Type u_1} [] :
.IsComplement'
@[simp]
theorem AddSubgroup.isComplement'_bot_left {G : Type u_1} [] {H : } :
.IsComplement' H H =
@[simp]
theorem Subgroup.isComplement'_bot_left {G : Type u_1} [] {H : } :
.IsComplement' H H =
@[simp]
theorem AddSubgroup.isComplement'_bot_right {G : Type u_1} [] {H : } :
H.IsComplement' H =
@[simp]
theorem Subgroup.isComplement'_bot_right {G : Type u_1} [] {H : } :
H.IsComplement' H =
@[simp]
theorem AddSubgroup.isComplement'_top_left {G : Type u_1} [] {H : } :
.IsComplement' H H =
@[simp]
theorem Subgroup.isComplement'_top_left {G : Type u_1} [] {H : } :
.IsComplement' H H =
@[simp]
theorem AddSubgroup.isComplement'_top_right {G : Type u_1} [] {H : } :
H.IsComplement' H =
@[simp]
theorem Subgroup.isComplement'_top_right {G : Type u_1} [] {H : } :
H.IsComplement' H =
theorem AddSubgroup.mem_leftTransversals_iff_existsUnique_neg_add_mem {G : Type u_1} [] {S : Set G} {T : Set G} :
∀ (g : G), ∃! s : S, -s + g T
theorem Subgroup.mem_leftTransversals_iff_existsUnique_inv_mul_mem {G : Type u_1} [] {S : Set G} {T : Set G} :
∀ (g : G), ∃! s : S, (↑s)⁻¹ * g T
theorem AddSubgroup.mem_rightTransversals_iff_existsUnique_add_neg_mem {G : Type u_1} [] {S : Set G} {T : Set G} :
∀ (g : G), ∃! s : S, g + -s T
theorem Subgroup.mem_rightTransversals_iff_existsUnique_mul_inv_mem {G : Type u_1} [] {S : Set G} {T : Set G} :
∀ (g : G), ∃! s : S, g * (↑s)⁻¹ T
theorem AddSubgroup.mem_leftTransversals_iff_existsUnique_quotient_mk''_eq {G : Type u_1} [] {H : } {S : Set G} :
∀ (q : ), ∃! s : S, = q
theorem Subgroup.mem_leftTransversals_iff_existsUnique_quotient_mk''_eq {G : Type u_1} [] {H : } {S : Set G} :
∀ (q : ), ∃! s : S, = q
theorem AddSubgroup.mem_rightTransversals_iff_existsUnique_quotient_mk''_eq {G : Type u_1} [] {H : } {S : Set G} :
∀ (q : ), ∃! s : S, = q
theorem Subgroup.mem_rightTransversals_iff_existsUnique_quotient_mk''_eq {G : Type u_1} [] {H : } {S : Set G} :
∀ (q : ), ∃! s : S, = q
theorem AddSubgroup.mem_leftTransversals_iff_bijective {G : Type u_1} [] {H : } {S : Set G} :
Function.Bijective (S.restrict Quotient.mk'')
theorem Subgroup.mem_leftTransversals_iff_bijective {G : Type u_1} [] {H : } {S : Set G} :
Function.Bijective (S.restrict Quotient.mk'')
theorem AddSubgroup.mem_rightTransversals_iff_bijective {G : Type u_1} [] {H : } {S : Set G} :
Function.Bijective (S.restrict Quotient.mk'')
theorem Subgroup.mem_rightTransversals_iff_bijective {G : Type u_1} [] {H : } {S : Set G} :
Function.Bijective (S.restrict Quotient.mk'')
theorem AddSubgroup.card_left_transversal {G : Type u_1} [] {H : } {S : Set G} (h : ) :
Nat.card S = H.index
theorem Subgroup.card_left_transversal {G : Type u_1} [] {H : } {S : Set G} (h : ) :
Nat.card S = H.index
theorem AddSubgroup.card_right_transversal {G : Type u_1} [] {H : } {S : Set G} (h : ) :
Nat.card S = H.index
theorem Subgroup.card_right_transversal {G : Type u_1} [] {H : } {S : Set G} (h : ) :
Nat.card S = H.index
theorem AddSubgroup.range_mem_leftTransversals {G : Type u_1} [] {H : } {f : G HG} (hf : ∀ (q : G H), (f q) = q) :
theorem Subgroup.range_mem_leftTransversals {G : Type u_1} [] {H : } {f : G HG} (hf : ∀ (q : G H), (f q) = q) :
theorem AddSubgroup.range_mem_rightTransversals {G : Type u_1} [] {H : } {f : } (hf : ∀ (q : ), Quotient.mk'' (f q) = q) :
theorem Subgroup.range_mem_rightTransversals {G : Type u_1} [] {H : } {f : } (hf : ∀ (q : ), Quotient.mk'' (f q) = q) :
theorem AddSubgroup.exists_left_transversal {G : Type u_1} [] (H : ) (g : G) :
S, g S
theorem Subgroup.exists_left_transversal {G : Type u_1} [] (H : ) (g : G) :
S, g S
theorem AddSubgroup.exists_right_transversal {G : Type u_1} [] (H : ) (g : G) :
S, g S
theorem Subgroup.exists_right_transversal {G : Type u_1} [] (H : ) (g : G) :
S, g S
theorem AddSubgroup.exists_left_transversal_of_le {G : Type u_1} [] {H' : } {H : } (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} [] {H' : } {H : } (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} [] {H' : } {H : } (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} [] {H' : } {H : } (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} [] {S : Set G} {T : Set G} (hST : ) :
G S × T

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

Equations
Instances For
@[simp]
theorem Subgroup.IsComplement.equiv_symm_apply {G : Type u_1} [] {S : Set G} {T : Set G} (hST : ) (x : S × T) :
hST.equiv.symm x = x.1 * x.2
@[simp]
theorem Subgroup.IsComplement.equiv_fst_mul_equiv_snd {G : Type u_1} [] {S : Set G} {T : Set G} (hST : ) (g : G) :
(hST.equiv g).1 * (hST.equiv g).2 = g
theorem Subgroup.IsComplement.equiv_fst_eq_mul_inv {G : Type u_1} [] {S : Set G} {T : Set G} (hST : ) (g : G) :
(hST.equiv g).1 = g * (↑(hST.equiv g).2)⁻¹
theorem Subgroup.IsComplement.equiv_snd_eq_inv_mul {G : Type u_1} [] {S : Set G} {T : Set G} (hST : ) (g : G) :
(hST.equiv g).2 = (↑(hST.equiv g).1)⁻¹ * g
theorem Subgroup.IsComplement.equiv_fst_eq_iff_leftCosetEquivalence {G : Type u_1} [] {K : } {S : Set G} (hSK : ) {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} [] {H : } {T : Set G} (hHT : ) {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} [] {K : } {S : Set G} (hSK : ) (g : G) :
LeftCosetEquivalence (↑K) g (hSK.equiv g).1
theorem Subgroup.IsComplement.rightCosetEquivalence_equiv_snd {G : Type u_1} [] {H : } {T : Set G} (hHT : ) (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} [] {S : Set G} {T : Set G} (hST : ) {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} [] {S : Set G} {T : Set G} (hST : ) {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} [] {S : Set G} {T : Set G} (hST : ) {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} [] {S : Set G} {T : Set G} (hST : ) {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} [] {K : } {S : Set G} (hSK : ) (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} [] {K : } {S : Set G} (hSK : ) {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} [] {H : } {T : Set G} (hHT : ) (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} [] {H : } {T : Set G} (hHT : ) {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} [] {S : Set G} {T : Set G} (hST : ) (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} [] {S : Set G} {T : Set G} (hST : ) {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} [] {S : Set G} {T : Set G} (hST : ) {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} [] {S : Set G} {T : Set G} (hST : ) {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} [] {S : Set G} {T : Set G} (hST : ) {g : G} (h1 : 1 T) :
(hST.equiv g).2 = 1 g S
noncomputable def AddSubgroup.MemLeftTransversals.toEquiv {G : Type u_1} [] {H : } {S : Set G} (hS : ) :
G H S

A left transversal is in bijection with left cosets.

Equations
Instances For
theorem AddSubgroup.MemLeftTransversals.toEquiv.proof_1 {G : Type u_1} [] {H : } {S : Set G} (hS : ) :
Function.Bijective (S.restrict Quotient.mk'')
noncomputable def Subgroup.MemLeftTransversals.toEquiv {G : Type u_1} [] {H : } {S : Set G} (hS : ) :
G H S

A left transversal is in bijection with left cosets.

Equations
Instances For
theorem AddSubgroup.MemLeftTransversals.finite_iff {G : Type u_1} [] {H : } {S : Set G} (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} [] {H : } {S : Set G} (h : ) :
Finite S H.FiniteIndex
theorem AddSubgroup.MemLeftTransversals.mk''_toEquiv {G : Type u_1} [] {H : } {S : Set G} (hS : ) (q : G H) :
theorem Subgroup.MemLeftTransversals.mk''_toEquiv {G : Type u_1} [] {H : } {S : Set G} (hS : ) (q : G H) :
theorem AddSubgroup.MemLeftTransversals.toEquiv_apply {G : Type u_1} [] {H : } {f : G HG} (hf : ∀ (q : G H), (f q) = q) (q : G H) :
= f q
theorem Subgroup.MemLeftTransversals.toEquiv_apply {G : Type u_1} [] {H : } {f : G HG} (hf : ∀ (q : G H), (f q) = q) (q : G H) :
= f q
noncomputable def AddSubgroup.MemLeftTransversals.toFun {G : Type u_1} [] {H : } {S : Set G} (hS : ) :
GS

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

Equations
• = Quotient.mk''
Instances For
noncomputable def Subgroup.MemLeftTransversals.toFun {G : Type u_1} [] {H : } {S : Set G} (hS : ) :
GS

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

Equations
• = Quotient.mk''
Instances For
theorem AddSubgroup.MemLeftTransversals.neg_toFun_add_mem {G : Type u_1} [] {H : } {S : Set G} (hS : ) (g : G) :
H
theorem Subgroup.MemLeftTransversals.inv_toFun_mul_mem {G : Type u_1} [] {H : } {S : Set G} (hS : ) (g : G) :
(↑)⁻¹ * g H
theorem AddSubgroup.MemLeftTransversals.neg_add_toFun_mem {G : Type u_1} [] {H : } {S : Set G} (hS : ) (g : G) :
H
theorem Subgroup.MemLeftTransversals.inv_mul_toFun_mem {G : Type u_1} [] {H : } {S : Set G} (hS : ) (g : G) :
H
noncomputable def AddSubgroup.MemRightTransversals.toEquiv {G : Type u_1} [] {H : } {S : Set G} (hS : ) :

A right transversal is in bijection with right cosets.

Equations
Instances For
theorem AddSubgroup.MemRightTransversals.toEquiv.proof_1 {G : Type u_1} [] {H : } {S : Set G} (hS : ) :
Function.Bijective (S.restrict Quotient.mk'')
noncomputable def Subgroup.MemRightTransversals.toEquiv {G : Type u_1} [] {H : } {S : Set G} (hS : ) :

A right transversal is in bijection with right cosets.

Equations
Instances For
theorem AddSubgroup.MemRightTransversals.finite_iff {G : Type u_1} [] {H : } {S : Set G} (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} [] {H : } {S : Set G} (h : ) :
Finite S H.FiniteIndex
theorem AddSubgroup.MemRightTransversals.mk''_toEquiv {G : Type u_1} [] {H : } {S : Set G} (hS : ) (q : ) :
theorem Subgroup.MemRightTransversals.mk''_toEquiv {G : Type u_1} [] {H : } {S : Set G} (hS : ) (q : ) :
theorem AddSubgroup.MemRightTransversals.toEquiv_apply {G : Type u_1} [] {H : } {f : } (hf : ∀ (q : ), Quotient.mk'' (f q) = q) (q : ) :
= f q
theorem Subgroup.MemRightTransversals.toEquiv_apply {G : Type u_1} [] {H : } {f : } (hf : ∀ (q : ), Quotient.mk'' (f q) = q) (q : ) :
= f q
noncomputable def AddSubgroup.MemRightTransversals.toFun {G : Type u_1} [] {H : } {S : Set G} (hS : ) :
GS

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

Equations
• = Quotient.mk''
Instances For
noncomputable def Subgroup.MemRightTransversals.toFun {G : Type u_1} [] {H : } {S : Set G} (hS : ) :
GS

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

Equations
• = Quotient.mk''
Instances For
theorem AddSubgroup.MemRightTransversals.add_neg_toFun_mem {G : Type u_1} [] {H : } {S : Set G} (hS : ) (g : G) :
H
theorem Subgroup.MemRightTransversals.mul_inv_toFun_mem {G : Type u_1} [] {H : } {S : Set G} (hS : ) (g : G) :
g * (↑)⁻¹ H
theorem AddSubgroup.MemRightTransversals.toFun_add_neg_mem {G : Type u_1} [] {H : } {S : Set G} (hS : ) (g : G) :
H
theorem Subgroup.MemRightTransversals.toFun_mul_inv_mem {G : Type u_1} [] {H : } {S : Set G} (hS : ) (g : G) :
H
theorem AddSubgroup.instAddActionElemSetLeftTransversalsCoe.proof_1 {G : Type u_1} [] {H : } {F : Type u_2} [] [] [] (f : F) (T : ) :
f +ᵥ T
theorem AddSubgroup.instAddActionElemSetLeftTransversalsCoe.proof_2 {G : Type u_1} [] {H : } {F : Type u_2} [] [] [] (T : ) :
0 +ᵥ T = T
noncomputable instance AddSubgroup.instAddActionElemSetLeftTransversalsCoe {G : Type u_1} [] {H : } {F : Type u_2} [] [] [] :
Equations
theorem AddSubgroup.instAddActionElemSetLeftTransversalsCoe.proof_3 {G : Type u_1} [] {H : } {F : Type u_2} [] [] [] (f₁ : F) (f₂ : F) (T : ) :
f₁ + f₂ +ᵥ T = f₁ +ᵥ (f₂ +ᵥ T)
noncomputable instance Subgroup.instMulActionElemSetLeftTransversalsCoe {G : Type u_1} [] {H : } {F : Type u_2} [] [] [] :
Equations
• Subgroup.instMulActionElemSetLeftTransversalsCoe =
theorem AddSubgroup.vadd_toFun {G : Type u_1} [] {H : } {F : Type u_2} [] [] [] (f : F) (T : ) (g : G) :
=
theorem Subgroup.smul_toFun {G : Type u_1} [] {H : } {F : Type u_2} [] [] [] (f : F) (T : ) (g : G) :
theorem AddSubgroup.vadd_toEquiv {G : Type u_1} [] {H : } {F : Type u_2} [] [] [] (f : F) (T : ) (q : G H) :
= ( (f +ᵥ q))
theorem Subgroup.smul_toEquiv {G : Type u_1} [] {H : } {F : Type u_2} [] [] [] (f : F) (T : ) (q : G H) :
f = ( (f q))
theorem AddSubgroup.vadd_apply_eq_vadd_apply_neg_vadd {G : Type u_1} [] {H : } {F : Type u_2} [] [] [] (f : F) (T : ) (q : G H) :
= f +ᵥ ( (-f +ᵥ q))
theorem Subgroup.smul_apply_eq_smul_apply_inv_smul {G : Type u_1} [] {H : } {F : Type u_2} [] [] [] (f : F) (T : ) (q : G H) :
= f ( (f⁻¹ q))
Equations
• AddSubgroup.instInhabitedElemSetLeftTransversalsCoe = { default := Set.range Quotient.out', }
Equations
• Subgroup.instInhabitedElemSetLeftTransversalsCoe = { default := Set.range Quotient.out', }
Equations
• AddSubgroup.instInhabitedElemSetRightTransversalsCoe = { default := Set.range Quotient.out', }
Equations
• Subgroup.instInhabitedElemSetRightTransversalsCoe = { default := Set.range Quotient.out', }
theorem Subgroup.IsComplement'.isCompl {G : Type u_1} [] {H : } {K : } (h : H.IsComplement' K) :
theorem Subgroup.IsComplement'.sup_eq_top {G : Type u_1} [] {H : } {K : } (h : H.IsComplement' K) :
H K =
theorem Subgroup.IsComplement'.disjoint {G : Type u_1} [] {H : } {K : } (h : H.IsComplement' K) :
theorem Subgroup.IsComplement'.index_eq_card {G : Type u_1} [] {H : } {K : } (h : H.IsComplement' K) :
K.index = Nat.card H
theorem Subgroup.IsComplement.card_mul {G : Type u_1} [] {S : Set G} {T : Set G} (h : ) :
Nat.card S * Nat.card T =
theorem Subgroup.IsComplement'.card_mul {G : Type u_1} [] {H : } {K : } (h : H.IsComplement' K) :
Nat.card H * Nat.card K =
theorem Subgroup.isComplement'_of_disjoint_and_mul_eq_univ {G : Type u_1} [] {H : } {K : } (h1 : Disjoint H K) (h2 : H * K = Set.univ) :
H.IsComplement' K
theorem Subgroup.isComplement'_of_card_mul_and_disjoint {G : Type u_1} [] {H : } {K : } [] (h1 : Nat.card H * Nat.card K = ) (h2 : Disjoint H K) :
H.IsComplement' K
theorem Subgroup.isComplement'_iff_card_mul_and_disjoint {G : Type u_1} [] {H : } {K : } [] :
H.IsComplement' K Nat.card H * Nat.card K = Disjoint H K
theorem Subgroup.isComplement'_of_coprime {G : Type u_1} [] {H : } {K : } [] (h1 : Nat.card H * Nat.card K = ) (h2 : (Nat.card H).Coprime (Nat.card K)) :
H.IsComplement' K
theorem Subgroup.isComplement'_stabilizer {G : Type u_1} [] {H : } {α : Type u_2} [] (a : α) (h1 : ∀ (h : H), h a = ah = 1) (h2 : ∀ (g : G), ∃ (h : H), h g a = a) :
H.IsComplement'
noncomputable def Subgroup.quotientEquivSigmaZMod {G : Type u} [] (H : ) (g : G) :
G H (q : MulAction.orbitRel.Quotient (↥) (G H)) × ZMod (Function.minimalPeriod (fun (x : G H) => g x) )

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Subgroup.quotientEquivSigmaZMod_symm_apply {G : Type u} [] (H : ) (g : G) (q : MulAction.orbitRel.Quotient (↥) (G H)) (k : ZMod (Function.minimalPeriod (fun (x : G H) => g x) )) :
(H.quotientEquivSigmaZMod g).symm q, k = g ^ k.cast
theorem Subgroup.quotientEquivSigmaZMod_apply {G : Type u} [] (H : ) (g : G) (q : MulAction.orbitRel.Quotient (↥) (G H)) (k : ) :
(H.quotientEquivSigmaZMod g) (g ^ k ) = q, k
noncomputable def Subgroup.transferFunction {G : Type u} [] (H : ) (g : G) :
G HG

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
Instances For
theorem Subgroup.transferFunction_apply {G : Type u} [] (H : ) (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} [] (H : ) (g : G) (q : G H) :
(H.transferFunction g q) = q
def Subgroup.transferSet {G : Type u} [] (H : ) (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)
Instances For
theorem Subgroup.mem_transferSet {G : Type u} [] (H : ) (g : G) (q : G H) :
H.transferFunction g q H.transferSet g
def Subgroup.transferTransversal {G : Type u} [] (H : ) (g : G) :

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,
Instances For
theorem Subgroup.transferTransversal_apply {G : Type u} [] (H : ) (g : G) (q : G H) :
= H.transferFunction g q
theorem Subgroup.transferTransversal_apply' {G : Type u} [] (H : ) (g : G) (q : MulAction.orbitRel.Quotient (↥) (G H)) (k : ZMod (Function.minimalPeriod (fun (x : G H) => g x) )) :
( (g ^ k.cast )) = g ^ k.cast *
theorem Subgroup.transferTransversal_apply'' {G : Type u} [] (H : ) (g : G) (q : MulAction.orbitRel.Quotient (↥) (G H)) (k : ZMod (Function.minimalPeriod (fun (x : G H) => g x) )) :
( (g ^ k.cast )) = if k = 0 then g ^ Function.minimalPeriod (fun (x : G H) => g x) * else g ^ k.cast *