group_theory.complement

source

def add_subgroup.is_complement {G : Type u_1} [add_group G] (S T : set G) :

Prop

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

Equations

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

source

def subgroup.is_complement {G : Type u_1} [group G] (S T : set G) :

Prop

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

Equations

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

source

@[reducible]

def add_subgroup.is_complement' {G : Type u_1} [add_group G] (H K : add_subgroup G) :

Prop

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

source

@[reducible]

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

Prop

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

source

def add_subgroup.left_transversals {G : Type u_1} [add_group G] (T : set G) :

set (set G)

The set of left-complements of T : set G

Equations

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

Instances for ↥add_subgroup.left_transversals

source

def subgroup.left_transversals {G : Type u_1} [group G] (T : set G) :

set (set G)

The set of left-complements of T : set G

Equations

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

Instances for ↥subgroup.left_transversals

source

def subgroup.right_transversals {G : Type u_1} [group G] (S : set G) :

set (set G)

The set of right-complements of S : set G

Equations

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

Instances for ↥subgroup.right_transversals

subgroup.right_transversals.inhabited

source

def add_subgroup.right_transversals {G : Type u_1} [add_group G] (S : set G) :

set (set G)

The set of right-complements of S : set G

Equations

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

Instances for ↥add_subgroup.right_transversals

add_subgroup.right_transversals.inhabited

source

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

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

source

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

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

source

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

add_subgroup.is_complement S T ↔ ∀ (g : G), ∃! (x : ↥S × ↥T), x.fst.val + x.snd.val = g

source

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

subgroup.is_complement S T ↔ ∀ (g : G), ∃! (x : ↥S × ↥T), x.fst.val * x.snd.val = g

source

theorem subgroup.is_complement.exists_unique {G : Type u_1} [group G] {S T : set G} (h : subgroup.is_complement S T) (g : G) :

∃! (x : ↥S × ↥T), x.fst.val * x.snd.val = g

source

theorem add_subgroup.is_complement.exists_unique {G : Type u_1} [add_group G] {S T : set G} (h : add_subgroup.is_complement S T) (g : G) :

∃! (x : ↥S × ↥T), x.fst.val + x.snd.val = g

source

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

K.is_complement' H

source

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

K.is_complement' H

source

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

H.is_complement' K ↔ K.is_complement' H

source

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

H.is_complement' K ↔ K.is_complement' H

source

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

subgroup.is_complement ⊤ {g}

source

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

add_subgroup.is_complement ⊤ {g}

source

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

subgroup.is_complement {g} ⊤

source

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

add_subgroup.is_complement {g} ⊤

source

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

subgroup.is_complement {g} S ↔ S = ⊤

source

theorem add_subgroup.is_complement_singleton_left {G : Type u_1} [add_group G] {S : set G} {g : G} :

add_subgroup.is_complement {g} S ↔ S = ⊤

source

theorem add_subgroup.is_complement_singleton_right {G : Type u_1} [add_group G] {S : set G} {g : G} :

add_subgroup.is_complement S {g} ↔ S = ⊤

source

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

subgroup.is_complement S {g} ↔ S = ⊤

source

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

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

source

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

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

source

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

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

source

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

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

source

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

⊤.is_complement' ⊥

source

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

⊤.is_complement' ⊥

source

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

⊥.is_complement' ⊤

source

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

⊥.is_complement' ⊤

source

@[simp]

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

⊥.is_complement' H ↔ H = ⊤

source

@[simp]

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

⊥.is_complement' H ↔ H = ⊤

source

@[simp]

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

H.is_complement' ⊥ ↔ H = ⊤

source

@[simp]

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

H.is_complement' ⊥ ↔ H = ⊤

source

@[simp]

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

⊤.is_complement' H ↔ H = ⊥

source

@[simp]

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

⊤.is_complement' H ↔ H = ⊥

source

@[simp]

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

H.is_complement' ⊤ ↔ H = ⊥

source

@[simp]

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

H.is_complement' ⊤ ↔ H = ⊥

source

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

S ∈ subgroup.left_transversals T ↔ ∀ (g : G), ∃! (s : ↥S), (↑s)⁻¹ * g ∈ T

source

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

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

source

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

S ∈ subgroup.right_transversals T ↔ ∀ (g : G), ∃! (s : ↥S), g * (↑s)⁻¹ ∈ T

source

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

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

source

theorem add_subgroup.mem_left_transversals_iff_exists_unique_quotient_mk'_eq {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} :

S ∈ add_subgroup.left_transversals ↑H ↔ ∀ (q : quotient (quotient_add_group.left_rel H)), ∃! (s : ↥S), quotient.mk' s.val = q

source

theorem subgroup.mem_left_transversals_iff_exists_unique_quotient_mk'_eq {G : Type u_1} [group G] {H : subgroup G} {S : set G} :

S ∈ subgroup.left_transversals ↑H ↔ ∀ (q : quotient (quotient_group.left_rel H)), ∃! (s : ↥S), quotient.mk' s.val = q

source

theorem subgroup.mem_right_transversals_iff_exists_unique_quotient_mk'_eq {G : Type u_1} [group G] {H : subgroup G} {S : set G} :

S ∈ subgroup.right_transversals ↑H ↔ ∀ (q : quotient (quotient_group.right_rel H)), ∃! (s : ↥S), quotient.mk' s.val = q

source

theorem add_subgroup.mem_right_transversals_iff_exists_unique_quotient_mk'_eq {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} :

S ∈ add_subgroup.right_transversals ↑H ↔ ∀ (q : quotient (quotient_add_group.right_rel H)), ∃! (s : ↥S), quotient.mk' s.val = q

source

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

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

source

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

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

source

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

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

source

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

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

source

theorem subgroup.range_mem_left_transversals {G : Type u_1} [group G] {H : subgroup G} {f : G ⧸ H → G} (hf : ∀ (q : G ⧸ H), ↑(f q) = q) :

set.range f ∈ subgroup.left_transversals ↑H

source

theorem add_subgroup.range_mem_left_transversals {G : Type u_1} [add_group G] {H : add_subgroup G} {f : G ⧸ H → G} (hf : ∀ (q : G ⧸ H), ↑(f q) = q) :

set.range f ∈ add_subgroup.left_transversals ↑H

source

theorem add_subgroup.range_mem_right_transversals {G : Type u_1} [add_group G] {H : add_subgroup G} {f : quotient (quotient_add_group.right_rel H) → G} (hf : ∀ (q : quotient (quotient_add_group.right_rel H)), quotient.mk' (f q) = q) :

set.range f ∈ add_subgroup.right_transversals ↑H

source

theorem subgroup.range_mem_right_transversals {G : Type u_1} [group G] {H : subgroup G} {f : quotient (quotient_group.right_rel H) → G} (hf : ∀ (q : quotient (quotient_group.right_rel H)), quotient.mk' (f q) = q) :

set.range f ∈ subgroup.right_transversals ↑H

source

theorem add_subgroup.exists_left_transversal {G : Type u_1} [add_group G] {H : add_subgroup G} (g : G) :

∃ (S : set G) (H : S ∈ add_subgroup.left_transversals ↑H), g ∈ S

source

theorem subgroup.exists_left_transversal {G : Type u_1} [group G] {H : subgroup G} (g : G) :

∃ (S : set G) (H : S ∈ subgroup.left_transversals ↑H), g ∈ S

source

theorem add_subgroup.exists_right_transversal {G : Type u_1} [add_group G] {H : add_subgroup G} (g : G) :

∃ (S : set G) (H : S ∈ add_subgroup.right_transversals ↑H), g ∈ S

source

theorem subgroup.exists_right_transversal {G : Type u_1} [group G] {H : subgroup G} (g : G) :

∃ (S : set G) (H : S ∈ subgroup.right_transversals ↑H), g ∈ S

source

noncomputable def subgroup.mem_left_transversals.to_equiv {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ∈ subgroup.left_transversals ↑H) :

G ⧸ H ≃ ↥S

A left transversal is in bijection with left cosets.

Equations

subgroup.mem_left_transversals.to_equiv hS = (equiv.of_bijective (S.restrict quotient.mk') _).symm

source

noncomputable def add_subgroup.mem_left_transversals.to_equiv {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ∈ add_subgroup.left_transversals ↑H) :

G ⧸ H ≃ ↥S

A left transversal is in bijection with left cosets.

Equations

add_subgroup.mem_left_transversals.to_equiv hS = (equiv.of_bijective (S.restrict quotient.mk') _).symm

source

theorem subgroup.mem_left_transversals.mk'_to_equiv {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ∈ subgroup.left_transversals ↑H) (q : G ⧸ H) :

quotient.mk' ↑(⇑(subgroup.mem_left_transversals.to_equiv hS) q) = q

source

theorem add_subgroup.mem_left_transversals.mk'_to_equiv {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ∈ add_subgroup.left_transversals ↑H) (q : G ⧸ H) :

quotient.mk' ↑(⇑(add_subgroup.mem_left_transversals.to_equiv hS) q) = q

source

theorem add_subgroup.mem_left_transversals.to_equiv_apply {G : Type u_1} [add_group G] {H : add_subgroup G} {f : G ⧸ H → G} (hf : ∀ (q : G ⧸ H), ↑(f q) = q) (q : G ⧸ H) :

↑(⇑(add_subgroup.mem_left_transversals.to_equiv _) q) = f q

source

theorem subgroup.mem_left_transversals.to_equiv_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.mem_left_transversals.to_equiv _) q) = f q

source

noncomputable def subgroup.mem_left_transversals.to_fun {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ∈ subgroup.left_transversals ↑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.mem_left_transversals.to_fun hS = ⇑(subgroup.mem_left_transversals.to_equiv hS) ∘ quotient.mk'

source

noncomputable def add_subgroup.mem_left_transversals.to_fun {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ∈ add_subgroup.left_transversals ↑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

add_subgroup.mem_left_transversals.to_fun hS = ⇑(add_subgroup.mem_left_transversals.to_equiv hS) ∘ quotient.mk'

source

theorem add_subgroup.mem_left_transversals.neg_to_fun_add_mem {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ∈ add_subgroup.left_transversals ↑H) (g : G) :

-↑(add_subgroup.mem_left_transversals.to_fun hS g) + g ∈ H

source

theorem subgroup.mem_left_transversals.inv_to_fun_mul_mem {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ∈ subgroup.left_transversals ↑H) (g : G) :

(↑(subgroup.mem_left_transversals.to_fun hS g))⁻¹ * g ∈ H

source

theorem subgroup.mem_left_transversals.inv_mul_to_fun_mem {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ∈ subgroup.left_transversals ↑H) (g : G) :

g⁻¹ * ↑(subgroup.mem_left_transversals.to_fun hS g) ∈ H

source

theorem add_subgroup.mem_left_transversals.neg_add_to_fun_mem {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ∈ add_subgroup.left_transversals ↑H) (g : G) :

-g + ↑(add_subgroup.mem_left_transversals.to_fun hS g) ∈ H

source

noncomputable def add_subgroup.mem_right_transversals.to_equiv {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ∈ add_subgroup.right_transversals ↑H) :

quotient (quotient_add_group.right_rel H) ≃ ↥S

A right transversal is in bijection with right cosets.

Equations

add_subgroup.mem_right_transversals.to_equiv hS = (equiv.of_bijective (S.restrict quotient.mk') _).symm

source

noncomputable def subgroup.mem_right_transversals.to_equiv {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ∈ subgroup.right_transversals ↑H) :

quotient (quotient_group.right_rel H) ≃ ↥S

A right transversal is in bijection with right cosets.

Equations

subgroup.mem_right_transversals.to_equiv hS = (equiv.of_bijective (S.restrict quotient.mk') _).symm

source

theorem add_subgroup.mem_right_transversals.mk'_to_equiv {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ∈ add_subgroup.right_transversals ↑H) (q : quotient (quotient_add_group.right_rel H)) :

quotient.mk' ↑(⇑(add_subgroup.mem_right_transversals.to_equiv hS) q) = q

source

theorem subgroup.mem_right_transversals.mk'_to_equiv {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ∈ subgroup.right_transversals ↑H) (q : quotient (quotient_group.right_rel H)) :

quotient.mk' ↑(⇑(subgroup.mem_right_transversals.to_equiv hS) q) = q

source

theorem subgroup.mem_right_transversals.to_equiv_apply {G : Type u_1} [group G] {H : subgroup G} {f : quotient (quotient_group.right_rel H) → G} (hf : ∀ (q : quotient (quotient_group.right_rel H)), quotient.mk' (f q) = q) (q : quotient (quotient_group.right_rel H)) :

↑(⇑(subgroup.mem_right_transversals.to_equiv _) q) = f q

source

theorem add_subgroup.mem_right_transversals.to_equiv_apply {G : Type u_1} [add_group G] {H : add_subgroup G} {f : quotient (quotient_add_group.right_rel H) → G} (hf : ∀ (q : quotient (quotient_add_group.right_rel H)), quotient.mk' (f q) = q) (q : quotient (quotient_add_group.right_rel H)) :

↑(⇑(add_subgroup.mem_right_transversals.to_equiv _) q) = f q

source

noncomputable def add_subgroup.mem_right_transversals.to_fun {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ∈ add_subgroup.right_transversals ↑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

add_subgroup.mem_right_transversals.to_fun hS = ⇑(add_subgroup.mem_right_transversals.to_equiv hS) ∘ quotient.mk'

source

noncomputable def subgroup.mem_right_transversals.to_fun {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ∈ subgroup.right_transversals ↑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.mem_right_transversals.to_fun hS = ⇑(subgroup.mem_right_transversals.to_equiv hS) ∘ quotient.mk'

source

theorem add_subgroup.mem_right_transversals.add_neg_to_fun_mem {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ∈ add_subgroup.right_transversals ↑H) (g : G) :

g + -↑(add_subgroup.mem_right_transversals.to_fun hS g) ∈ H

source

theorem subgroup.mem_right_transversals.mul_inv_to_fun_mem {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ∈ subgroup.right_transversals ↑H) (g : G) :

g * (↑(subgroup.mem_right_transversals.to_fun hS g))⁻¹ ∈ H

source

theorem subgroup.mem_right_transversals.to_fun_mul_inv_mem {G : Type u_1} [group G] {H : subgroup G} {S : set G} (hS : S ∈ subgroup.right_transversals ↑H) (g : G) :

↑(subgroup.mem_right_transversals.to_fun hS g) * g⁻¹ ∈ H

source

theorem add_subgroup.mem_right_transversals.to_fun_add_neg_mem {G : Type u_1} [add_group G] {H : add_subgroup G} {S : set G} (hS : S ∈ add_subgroup.right_transversals ↑H) (g : G) :

↑(add_subgroup.mem_right_transversals.to_fun hS g) + -g ∈ H

source

@[protected, instance]

def add_subgroup.left_transversals.add_action {G : Type u_1} [add_group G] {H : add_subgroup G} {F : Type u_2} [add_group F] [add_action F G] [add_action.quotient_action F H] :

add_action F ↥(add_subgroup.left_transversals ↑H)

Equations

add_subgroup.left_transversals.add_action = {to_has_vadd := {vadd := λ (f : F) (T : ↥(add_subgroup.left_transversals ↑H)), ⟨f +ᵥ ↑T, _⟩}, zero_vadd := _, add_vadd := _}

source

@[protected, instance]

def subgroup.left_transversals.mul_action {G : Type u_1} [group G] {H : subgroup G} {F : Type u_2} [group F] [mul_action F G] [mul_action.quotient_action F H] :

mul_action F ↥(subgroup.left_transversals ↑H)

Equations

subgroup.left_transversals.mul_action = {to_has_smul := {smul := λ (f : F) (T : ↥(subgroup.left_transversals ↑H)), ⟨f • ↑T, _⟩}, one_smul := _, mul_smul := _}

source

theorem subgroup.smul_to_fun {G : Type u_1} [group G] {H : subgroup G} {F : Type u_2} [group F] [mul_action F G] [mul_action.quotient_action F H] (f : F) (T : ↥(subgroup.left_transversals ↑H)) (g : G) :

f • ↑(subgroup.mem_left_transversals.to_fun _ g) = ↑(subgroup.mem_left_transversals.to_fun _ (f • g))

source

theorem add_subgroup.vadd_to_fun {G : Type u_1} [add_group G] {H : add_subgroup G} {F : Type u_2} [add_group F] [add_action F G] [add_action.quotient_action F H] (f : F) (T : ↥(add_subgroup.left_transversals ↑H)) (g : G) :

f +ᵥ ↑(add_subgroup.mem_left_transversals.to_fun _ g) = ↑(add_subgroup.mem_left_transversals.to_fun _ (f +ᵥ g))

source

theorem subgroup.smul_to_equiv {G : Type u_1} [group G] {H : subgroup G} {F : Type u_2} [group F] [mul_action F G] [mul_action.quotient_action F H] (f : F) (T : ↥(subgroup.left_transversals ↑H)) (q : G ⧸ H) :

f • ↑(⇑(subgroup.mem_left_transversals.to_equiv _) q) = ↑(⇑(subgroup.mem_left_transversals.to_equiv _) (f • q))

source

theorem add_subgroup.vadd_to_equiv {G : Type u_1} [add_group G] {H : add_subgroup G} {F : Type u_2} [add_group F] [add_action F G] [add_action.quotient_action F H] (f : F) (T : ↥(add_subgroup.left_transversals ↑H)) (q : G ⧸ H) :

f +ᵥ ↑(⇑(add_subgroup.mem_left_transversals.to_equiv _) q) = ↑(⇑(add_subgroup.mem_left_transversals.to_equiv _) (f +ᵥ q))

source

theorem add_subgroup.vadd_apply_eq_vadd_apply_neg_vadd {G : Type u_1} [add_group G] {H : add_subgroup G} {F : Type u_2} [add_group F] [add_action F G] [add_action.quotient_action F H] (f : F) (T : ↥(add_subgroup.left_transversals ↑H)) (q : G ⧸ H) :

↑(⇑(add_subgroup.mem_left_transversals.to_equiv _) q) = f +ᵥ ↑(⇑(add_subgroup.mem_left_transversals.to_equiv _) (-f +ᵥ q))

source

theorem subgroup.smul_apply_eq_smul_apply_inv_smul {G : Type u_1} [group G] {H : subgroup G} {F : Type u_2} [group F] [mul_action F G] [mul_action.quotient_action F H] (f : F) (T : ↥(subgroup.left_transversals ↑H)) (q : G ⧸ H) :

↑(⇑(subgroup.mem_left_transversals.to_equiv _) q) = f • ↑(⇑(subgroup.mem_left_transversals.to_equiv _) (f⁻¹ • q))

source

@[protected, instance]

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

inhabited ↥(add_subgroup.left_transversals ↑H)

Equations

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

source

@[protected, instance]

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

inhabited ↥(subgroup.left_transversals ↑H)

Equations

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

source

@[protected, instance]

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

inhabited ↥(subgroup.right_transversals ↑H)

Equations

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

source

@[protected, instance]

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

inhabited ↥(add_subgroup.right_transversals ↑H)

Equations

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

source

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

is_compl H K

source

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

H ⊔ K = ⊤

source

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

disjoint H K

source

theorem subgroup.is_complement.card_mul {G : Type u_1} [group G] {S T : set G} [fintype G] [fintype ↥S] [fintype ↥T] (h : subgroup.is_complement S T) :

fintype.card ↥S * fintype.card ↥T = fintype.card G

source

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

fintype.card ↥H * fintype.card ↥K = fintype.card G

source

theorem subgroup.is_complement'_of_card_mul_and_disjoint {G : Type u_1} [group G] {H K : subgroup G} [fintype G] [fintype ↥H] [fintype ↥K] (h1 : fintype.card ↥H * fintype.card ↥K = fintype.card G) (h2 : disjoint H K) :

H.is_complement' K

source

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

H.is_complement' K ↔ fintype.card ↥H * fintype.card ↥K = fintype.card G ∧ disjoint H K

source

theorem subgroup.is_complement'_of_coprime {G : Type u_1} [group G] {H K : subgroup G} [fintype G] [fintype ↥H] [fintype ↥K] (h1 : fintype.card ↥H * fintype.card ↥K = fintype.card G) (h2 : (fintype.card ↥H).coprime (fintype.card ↥K)) :

H.is_complement' K

source

theorem subgroup.is_complement'_stabilizer {G : Type u_1} [group G] {H : subgroup G} {α : Type u_2} [mul_action G α] (a : α) (h1 : ∀ (h : ↥H), h • a = a → h = 1) (h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a) :

H.is_complement' (mul_action.stabilizer G a)

source

noncomputable def subgroup.quotient_equiv_sigma_zmod {G : Type u} [group G] (H : subgroup G) (g : G) :

G ⧸ H ≃ Σ (q : mul_action.orbit_rel.quotient ↥(subgroup.zpowers g) (G ⧸ H)), zmod (function.minimal_period (has_smul.smul g) (quotient.out' q))

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

Equations

H.quotient_equiv_sigma_zmod g = (mul_action.self_equiv_sigma_orbits ↥(subgroup.zpowers g) (G ⧸ H)).trans (equiv.sigma_congr_right (λ (q : mul_action.orbit_rel.quotient ↥(subgroup.zpowers g) (G ⧸ H)), mul_action.orbit_zpowers_equiv g (quotient.out' q)))

source

theorem subgroup.quotient_equiv_sigma_zmod_symm_apply {G : Type u} [group G] (H : subgroup G) (g : G) (q : mul_action.orbit_rel.quotient ↥(subgroup.zpowers g) (G ⧸ H)) (k : zmod (function.minimal_period (has_smul.smul g) (quotient.out' q))) :

⇑((H.quotient_equiv_sigma_zmod g).symm) ⟨q, k⟩ = g ^ ↑k • quotient.out' q

source

theorem subgroup.quotient_equiv_sigma_zmod_apply {G : Type u} [group G] (H : subgroup G) (g : G) (q : mul_action.orbit_rel.quotient ↥(subgroup.zpowers g) (G ⧸ H)) (k : ℤ) :

⇑(H.quotient_equiv_sigma_zmod g) (g ^ k • quotient.out' q) = ⟨q, ↑k⟩

source

noncomputable def subgroup.transfer_function {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.transfer_function g = λ (q : G ⧸ H), g ^ ↑((⇑(H.quotient_equiv_sigma_zmod g) q).snd) * quotient.out' (quotient.out' (⇑(H.quotient_equiv_sigma_zmod g) q).fst)

source

theorem subgroup.transfer_function_apply {G : Type u} [group G] (H : subgroup G) (g : G) (q : G ⧸ H) :

H.transfer_function g q = g ^ ↑((⇑(H.quotient_equiv_sigma_zmod g) q).snd) * quotient.out' (quotient.out' (⇑(H.quotient_equiv_sigma_zmod g) q).fst)

source

theorem subgroup.coe_transfer_function {G : Type u} [group G] (H : subgroup G) (g : G) (q : G ⧸ H) :

↑(H.transfer_function g q) = q

source

def subgroup.transfer_set {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.transfer_set g = set.range (H.transfer_function g)

source

theorem subgroup.mem_transfer_set {G : Type u} [group G] (H : subgroup G) (g : G) (q : G ⧸ H) :

H.transfer_function g q ∈ H.transfer_set g

source

def subgroup.transfer_transversal {G : Type u} [group G] (H : subgroup G) (g : G) :

↥(subgroup.left_transversals ↑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.transfer_transversal g = ⟨H.transfer_set g, _⟩

source

theorem subgroup.transfer_transversal_apply {G : Type u} [group G] (H : subgroup G) (g : G) (q : G ⧸ H) :

↑(⇑(subgroup.mem_left_transversals.to_equiv _) q) = H.transfer_function g q

source

theorem subgroup.transfer_transversal_apply' {G : Type u} [group G] (H : subgroup G) (g : G) (q : mul_action.orbit_rel.quotient ↥(subgroup.zpowers g) (G ⧸ H)) (k : zmod (function.minimal_period (has_smul.smul g) (quotient.out' q))) :

↑(⇑(subgroup.mem_left_transversals.to_equiv _) (g ^ ↑k • quotient.out' q)) = g ^ ↑k * quotient.out' (quotient.out' q)

source

theorem subgroup.transfer_transversal_apply'' {G : Type u} [group G] (H : subgroup G) (g : G) (q : mul_action.orbit_rel.quotient ↥(subgroup.zpowers g) (G ⧸ H)) (k : zmod (function.minimal_period (has_smul.smul g) (quotient.out' q))) :

↑(⇑(subgroup.mem_left_transversals.to_equiv _) (g ^ ↑k • quotient.out' q)) = ite (k = 0) (g ^ function.minimal_period (has_smul.smul g) (quotient.out' q) * quotient.out' (quotient.out' q)) (g ^ ↑k * quotient.out' (quotient.out' q))

mathlib documentation

Complements #

Main definitions #

Main results #