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

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.

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

@[inline, reducible]

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

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

The set of left-complements of T : Set G

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

The set of left-complements of T : Set G

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

The set of right-complements of S : Set G

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

The set of right-complements of S : Set G

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

theorem Subgroup.isComplement'_def {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} : Subgroup.IsComplement' H 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, ↑x.fst + ↑x.snd = 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, ↑x.fst * ↑x.snd = 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, ↑x.fst + ↑x.snd = 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, ↑x.fst * ↑x.snd = g

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

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

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

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

abbrev AddSubgroup.isComplement_top_singleton.match_2 {G : Type u_1} [AddGroup G] {g : G} : ∀ (x : ↑⊤ × ↑{g}) (motive : (x_1 : ↑⊤ × ↑{g}) → (fun x => ↑x.fst + ↑x.snd) x_1 = (fun x => ↑x.fst + ↑x.snd) x → Prop) (x_1 : ↑⊤ × ↑{g}) (h : (fun x => ↑x.fst + ↑x.snd) x_1 = (fun x => ↑x.fst + ↑x.snd) x), (∀ (fst : ↑⊤) (h : (fun x => ↑x.fst + ↑x.snd) (fst, { val := g, property := (_ : g = g) }) = (fun x => ↑x.fst + ↑x.snd) x), motive (fst, { val := g, property := (_ : g = g) }) h) → motive x_1 h

abbrev AddSubgroup.isComplement_top_singleton.match_1 {G : Type u_1} [AddGroup G] {g : G} : ∀ (fst : ↑⊤) (motive : (x : ↑⊤ × ↑{g}) → (fun x => ↑x.fst + ↑x.snd) (fst, { val := g, property := (_ : g = g) }) = (fun x => ↑x.fst + ↑x.snd) x → Prop) (x : ↑⊤ × ↑{g}) (h : (fun x => ↑x.fst + ↑x.snd) (fst, { val := g, property := (_ : g = g) }) = (fun x => ↑x.fst + ↑x.snd) x), (∀ (fst_1 : ↑⊤) (h : (fun x => ↑x.fst + ↑x.snd) (fst, { val := g, property := (_ : g = g) }) = (fun x => ↑x.fst + ↑x.snd) (fst_1, { val := g, property := (_ : g = g) })), motive (fst_1, { val := g, property := (_ : g = g) }) h) → motive x h

theorem AddSubgroup.isComplement_top_singleton {G : Type u_1} [AddGroup G] {g : G} : AddSubgroup.IsComplement ⊤ {g}

theorem Subgroup.isComplement_top_singleton {G : Type u_1} [Group G] {g : G} : Subgroup.IsComplement ⊤ {g}

theorem AddSubgroup.isComplement_singleton_top {G : Type u_1} [AddGroup G] {g : G} : AddSubgroup.IsComplement {g} ⊤

abbrev AddSubgroup.isComplement_singleton_top.match_1 {G : Type u_1} [AddGroup G] {g : G} : ∀ (snd : ↑⊤) (motive : (x : ↑{g} × ↑⊤) → (fun x => ↑x.fst + ↑x.snd) ({ val := g, property := (_ : g = g) }, snd) = (fun x => ↑x.fst + ↑x.snd) x → Prop) (x : ↑{g} × ↑⊤) (h : (fun x => ↑x.fst + ↑x.snd) ({ val := g, property := (_ : g = g) }, snd) = (fun x => ↑x.fst + ↑x.snd) x), (∀ (snd_1 : ↑⊤) (h : (fun x => ↑x.fst + ↑x.snd) ({ val := g, property := (_ : g = g) }, snd) = (fun x => ↑x.fst + ↑x.snd) ({ val := g, property := (_ : g = g) }, snd_1)), motive ({ val := g, property := (_ : g = g) }, snd_1) h) → motive x h

abbrev AddSubgroup.isComplement_singleton_top.match_2 {G : Type u_1} [AddGroup G] {g : G} : ∀ (x : ↑{g} × ↑⊤) (motive : (x_1 : ↑{g} × ↑⊤) → (fun x => ↑x.fst + ↑x.snd) x_1 = (fun x => ↑x.fst + ↑x.snd) x → Prop) (x_1 : ↑{g} × ↑⊤) (h : (fun x => ↑x.fst + ↑x.snd) x_1 = (fun x => ↑x.fst + ↑x.snd) x), (∀ (snd : ↑⊤) (h : (fun x => ↑x.fst + ↑x.snd) ({ val := g, property := (_ : g = g) }, snd) = (fun x => ↑x.fst + ↑x.snd) x), motive ({ val := g, property := (_ : g = g) }, snd) h) → motive x_1 h

theorem Subgroup.isComplement_singleton_top {G : Type u_1} [Group G] {g : G} : Subgroup.IsComplement {g} ⊤

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

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

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

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

theorem AddSubgroup.isComplement_top_left {G : Type u_1} [AddGroup G] {S : Set G} : AddSubgroup.IsComplement ⊤ S ↔ ∃ g, S = {g}

theorem Subgroup.isComplement_top_left {G : Type u_1} [Group G] {S : Set G} : Subgroup.IsComplement ⊤ S ↔ ∃ g, S = {g}

theorem AddSubgroup.isComplement_top_right {G : Type u_1} [AddGroup G] {S : Set G} : AddSubgroup.IsComplement S ⊤ ↔ ∃ g, S = {g}

theorem Subgroup.isComplement_top_right {G : Type u_1} [Group G] {S : Set G} : Subgroup.IsComplement S ⊤ ↔ ∃ g, S = {g}

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Subgroup.isComplement'_top_right {G : Type u_1} [Group G] {H : Subgroup G} : Subgroup.IsComplement' H ⊤ ↔ 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 + 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)⁻¹ * 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, 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, 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, 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, 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, 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, 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 (Set.restrict S 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 (Set.restrict S 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 (Set.restrict S 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 (Set.restrict S 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 = AddSubgroup.index H

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 = Subgroup.index H

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 = AddSubgroup.index H

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 = Subgroup.index H

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, S ∈ AddSubgroup.leftTransversals ↑H ∧ g ∈ S

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

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

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

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

@[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) : ↑(Subgroup.IsComplement.equiv hST).symm x = ↑x.fst * ↑x.snd

@[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) : ↑(↑(Subgroup.IsComplement.equiv hST) g).fst * ↑(↑(Subgroup.IsComplement.equiv hST) g).snd = 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) : ↑(↑(Subgroup.IsComplement.equiv hST) g).fst = g * (↑(↑(Subgroup.IsComplement.equiv hST) g).snd)⁻¹

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) : ↑(↑(Subgroup.IsComplement.equiv hST) g).snd = (↑(↑(Subgroup.IsComplement.equiv hST) g).fst)⁻¹ * 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} : (↑(Subgroup.IsComplement.equiv hSK) g₁).fst = (↑(Subgroup.IsComplement.equiv hSK) g₂).fst ↔ 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} : (↑(Subgroup.IsComplement.equiv hHT) g₁).snd = (↑(Subgroup.IsComplement.equiv hHT) g₂).snd ↔ 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 ↑(↑(Subgroup.IsComplement.equiv hSK) g).fst

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 ↑(↑(Subgroup.IsComplement.equiv hHT) g).snd

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) : (↑(Subgroup.IsComplement.equiv hST) g).fst = { val := g, property := 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) : (↑(Subgroup.IsComplement.equiv hST) g).snd = { val := g, property := 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) : (↑(Subgroup.IsComplement.equiv hST) g).snd = { val := 1, property := 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) : (↑(Subgroup.IsComplement.equiv hST) g).fst = { val := 1, property := 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 : { x // x ∈ K }) : ↑(Subgroup.IsComplement.equiv hSK) (g * ↑k) = ((↑(Subgroup.IsComplement.equiv hSK) g).fst, (↑(Subgroup.IsComplement.equiv hSK) g).snd * 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) : ↑(Subgroup.IsComplement.equiv hSK) (g * k) = ((↑(Subgroup.IsComplement.equiv hSK) g).fst, (↑(Subgroup.IsComplement.equiv hSK) g).snd * { val := k, property := 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 : { x // x ∈ H }) (g : G) : ↑(Subgroup.IsComplement.equiv hHT) (↑h * g) = (h * (↑(Subgroup.IsComplement.equiv hHT) g).fst, (↑(Subgroup.IsComplement.equiv hHT) g).snd)

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) : ↑(Subgroup.IsComplement.equiv hHT) (h * g) = ({ val := h, property := hh } * (↑(Subgroup.IsComplement.equiv hHT) g).fst, (↑(Subgroup.IsComplement.equiv hHT) g).snd)

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) : ↑(Subgroup.IsComplement.equiv hST) 1 = ({ val := 1, property := hs1 }, { val := 1, property := 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) : ↑(↑(Subgroup.IsComplement.equiv hST) g).fst = 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) : ↑(↑(Subgroup.IsComplement.equiv hST) g).snd = 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) : ↑(↑(Subgroup.IsComplement.equiv hST) g).fst = 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) : ↑(↑(Subgroup.IsComplement.equiv hST) g).snd = 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.

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 (Set.restrict S 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.

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 (_ : (Set.range fun q => f q) ∈ AddSubgroup.leftTransversals ↑H)) 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 (_ : (Set.range fun q => f q) ∈ Subgroup.leftTransversals ↑H)) 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.

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.

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.

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 (Set.restrict S 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.

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 (_ : (Set.range fun q => f q) ∈ AddSubgroup.rightTransversals ↑H)) 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 (_ : (Set.range fun q => f q) ∈ Subgroup.rightTransversals ↑H)) 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.

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.

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.instAddActionElemSetLeftTransversalsCoeAddSubgroupInstSetLikeAddSubgroupToAddMonoidToSubNegAddMonoid.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)

theorem AddSubgroup.instAddActionElemSetLeftTransversalsCoeAddSubgroupInstSetLikeAddSubgroupToAddMonoidToSubNegAddMonoid.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.instAddActionElemSetLeftTransversalsCoeAddSubgroupInstSetLikeAddSubgroupToAddMonoidToSubNegAddMonoid {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)

theorem AddSubgroup.instAddActionElemSetLeftTransversalsCoeAddSubgroupInstSetLikeAddSubgroupToAddMonoidToSubNegAddMonoid.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

noncomputable instance Subgroup.instMulActionElemSetLeftTransversalsCoeSubgroupInstSetLikeSubgroupToMonoidToDivInvMonoid {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)

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 (_ : ↑T ∈ AddSubgroup.leftTransversals ↑H) g) = ↑(AddSubgroup.MemLeftTransversals.toFun (_ : ↑(f +ᵥ T) ∈ AddSubgroup.leftTransversals ↑H) (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 (_ : ↑T ∈ Subgroup.leftTransversals ↑H) g) = ↑(Subgroup.MemLeftTransversals.toFun (_ : ↑(f • T) ∈ Subgroup.leftTransversals ↑H) (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 (_ : ↑T ∈ AddSubgroup.leftTransversals ↑H)) q) = ↑(↑(AddSubgroup.MemLeftTransversals.toEquiv (_ : ↑(f +ᵥ T) ∈ AddSubgroup.leftTransversals ↑H)) (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 (_ : ↑T ∈ Subgroup.leftTransversals ↑H)) q) = ↑(↑(Subgroup.MemLeftTransversals.toEquiv (_ : ↑(f • T) ∈ Subgroup.leftTransversals ↑H)) (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 (_ : ↑(f +ᵥ T) ∈ AddSubgroup.leftTransversals ↑H)) q) = f +ᵥ ↑(↑(AddSubgroup.MemLeftTransversals.toEquiv (_ : ↑T ∈ AddSubgroup.leftTransversals ↑H)) (-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 (_ : ↑(f • T) ∈ Subgroup.leftTransversals ↑H)) q) = f • ↑(↑(Subgroup.MemLeftTransversals.toEquiv (_ : ↑T ∈ Subgroup.leftTransversals ↑H)) (f⁻¹ • q))

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

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

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

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

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

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

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

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

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

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

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

theorem Subgroup.IsComplement'.card_mul {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [Fintype G] [Fintype { x // x ∈ H }] [Fintype { x // x ∈ K }] (h : Subgroup.IsComplement' H K) : Fintype.card { x // x ∈ H } * Fintype.card { x // x ∈ K } = Fintype.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) : Subgroup.IsComplement' H K

theorem Subgroup.isComplement'_of_card_mul_and_disjoint {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [Fintype G] [Fintype { x // x ∈ H }] [Fintype { x // x ∈ K }] (h1 : Fintype.card { x // x ∈ H } * Fintype.card { x // x ∈ K } = Fintype.card G) (h2 : Disjoint H K) : Subgroup.IsComplement' H K

theorem Subgroup.isComplement'_iff_card_mul_and_disjoint {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [Fintype G] [Fintype { x // x ∈ H }] [Fintype { x // x ∈ K }] : Subgroup.IsComplement' H K ↔ Fintype.card { x // x ∈ H } * Fintype.card { x // x ∈ K } = Fintype.card G ∧ Disjoint H K

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

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

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

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

theorem Subgroup.quotientEquivSigmaZMod_symm_apply {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient { x // x ∈ Subgroup.zpowers g } (G ⧸ H)) (k : ZMod (Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))) : ↑(Subgroup.quotientEquivSigmaZMod H g).symm { fst := q, snd := k } = g ^ ↑k • Quotient.out' q

theorem Subgroup.quotientEquivSigmaZMod_apply {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient { x // x ∈ Subgroup.zpowers g } (G ⧸ H)) (k : ℤ) : ↑(Subgroup.quotientEquivSigmaZMod H g) (g ^ k • Quotient.out' q) = { fst := q, snd := ↑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₀.

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

theorem Subgroup.coe_transferFunction {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : G ⧸ H) : ↑(Subgroup.transferFunction H 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.

theorem Subgroup.mem_transferSet {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : G ⧸ H) : Subgroup.transferFunction H g q ∈ Subgroup.transferSet H 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.

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

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

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