# Conjugacy of group elements #

See also MulAut.conj and Quandle.conj.

def IsConj {α : Type u} [] (a : α) (b : α) :

We say that a is conjugate to b if for some unit c we have c * a * c⁻¹ = b.

Equations
Instances For
theorem IsConj.refl {α : Type u} [] (a : α) :
IsConj a a
theorem IsConj.symm {α : Type u} [] {a : α} {b : α} :
IsConj a bIsConj b a
theorem isConj_comm {α : Type u} [] {g : α} {h : α} :
IsConj g h IsConj h g
theorem IsConj.trans {α : Type u} [] {a : α} {b : α} {c : α} :
IsConj a bIsConj b cIsConj a c
@[simp]
theorem isConj_iff_eq {α : Type u_1} [] {a : α} {b : α} :
IsConj a b a = b
theorem MonoidHom.map_isConj {α : Type u} {β : Type v} [] [] (f : α →* β) {a : α} {b : α} :
IsConj a bIsConj (f a) (f b)
@[simp]
theorem isConj_one_right {α : Type u} [] {a : α} :
IsConj 1 a a = 1
@[simp]
theorem isConj_one_left {α : Type u} [] {a : α} :
IsConj a 1 a = 1
@[simp]
theorem isConj_iff {α : Type u} [] {a : α} {b : α} :
IsConj a b ∃ (c : α), c * a * c⁻¹ = b
theorem conj_inv {α : Type u} [] {a : α} {b : α} :
(b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹
@[simp]
theorem conj_mul {α : Type u} [] {a : α} {b : α} {c : α} :
b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹
@[simp]
theorem conj_pow {α : Type u} [] {i : } {a : α} {b : α} :
(a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
@[simp]
theorem conj_zpow {α : Type u} [] {i : } {a : α} {b : α} :
(a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
theorem conj_injective {α : Type u} [] {x : α} :
Function.Injective fun (g : α) => x * g * x⁻¹
def IsConj.setoid (α : Type u_1) [] :

The setoid of the relation IsConj iff there is a unit u such that u * x = y * u

Equations
• = { r := IsConj, iseqv := }
Instances For
def ConjClasses (α : Type u_1) [] :
Type u_1

The quotient type of conjugacy classes of a group.

Equations
Instances For
def ConjClasses.mk {α : Type u_1} [] (a : α) :

The canonical quotient map from a monoid α into the ConjClasses of α

Equations
• = a
Instances For
instance ConjClasses.instInhabited {α : Type u} [] :
Equations
• ConjClasses.instInhabited = { default := 1 }
theorem ConjClasses.mk_eq_mk_iff_isConj {α : Type u} [] {a : α} {b : α} :
IsConj a b
theorem ConjClasses.quotient_mk_eq_mk {α : Type u} [] (a : α) :
a =
theorem ConjClasses.quot_mk_eq_mk {α : Type u} [] (a : α) :
Quot.mk Setoid.r a =
theorem ConjClasses.forall_isConj {α : Type u} [] {p : } :
(∀ (a : ), p a) ∀ (a : α), p ()
theorem ConjClasses.mk_surjective {α : Type u} [] :
Function.Surjective ConjClasses.mk
instance ConjClasses.instOne {α : Type u} [] :
One ()
Equations
• ConjClasses.instOne = { one := 1 }
theorem ConjClasses.exists_rep {α : Type u} [] (a : ) :
∃ (a0 : α), = a
def ConjClasses.map {α : Type u} {β : Type v} [] [] (f : α →* β) :

A MonoidHom maps conjugacy classes of one group to conjugacy classes of another.

Equations
Instances For
theorem ConjClasses.map_surjective {α : Type u} {β : Type v} [] [] {f : α →* β} (hf : ) :
@[instance 900]
Equations
• ConjClasses.instDecidableEqOfDecidableRelIsConj =
theorem ConjClasses.mk_injective {α : Type u} [] :
Function.Injective ConjClasses.mk
theorem ConjClasses.mk_bijective {α : Type u} [] :
Function.Bijective ConjClasses.mk
def ConjClasses.mkEquiv {α : Type u} [] :
α

The bijection between a CommGroup and its ConjClasses.

Equations
• ConjClasses.mkEquiv = { toFun := ConjClasses.mk, invFun := , left_inv := , right_inv := }
Instances For
def conjugatesOf {α : Type u} [] (a : α) :
Set α

Given an element a, conjugatesOf a is the set of conjugates.

Equations
Instances For
theorem mem_conjugatesOf_self {α : Type u} [] {a : α} :
theorem IsConj.conjugatesOf_eq {α : Type u} [] {a : α} {b : α} (ab : IsConj a b) :
theorem isConj_iff_conjugatesOf_eq {α : Type u} [] {a : α} {b : α} :
IsConj a b
def ConjClasses.carrier {α : Type u} [] :
Set α

Given a conjugacy class a, carrier a is the set it represents.

Equations
Instances For
theorem ConjClasses.mem_carrier_mk {α : Type u} [] {a : α} :
a ().carrier
theorem ConjClasses.mem_carrier_iff_mk_eq {α : Type u} [] {a : α} {b : } :
a b.carrier
theorem ConjClasses.carrier_eq_preimage_mk {α : Type u} [] {a : } :
a.carrier = ConjClasses.mk ⁻¹' {a}