# Documentation

Mathlib.Algebra.Group.Conj

# Conjugacy of group elements #

See also MulAut.conj and Quandle.conj.

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

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

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

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

Equations
def ConjClasses (α : Type u_1) [inst : ] :
Type u_1

The quotient type of conjugacy classes of a group.

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

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

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

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

Equations
theorem ConjClasses.map_surjective {α : Type u} {β : Type v} [inst : ] [inst : ] {f : α →* β} (hf : ) :
instance ConjClasses.instDecidableEqConjClasses {α : Type u} [inst : ] [inst : DecidableRel IsConj] :
Equations
• ConjClasses.instDecidableEqConjClasses = instDecidableEqQuotient
theorem ConjClasses.mk_injective {α : Type u} [inst : ] :
Function.Injective ConjClasses.mk
theorem ConjClasses.mk_bijective {α : Type u} [inst : ] :
Function.Bijective ConjClasses.mk
def ConjClasses.mkEquiv {α : Type u} [inst : ] :
α

The bijection between a CommGroup and its ConjClasses.

Equations
• One or more equations did not get rendered due to their size.
def conjugatesOf {α : Type u} [inst : ] (a : α) :
Set α

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

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

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

Equations
• ConjClasses.carrier = Quotient.lift conjugatesOf (_ : ∀ (x x_1 : α), x x_1)
theorem ConjClasses.mem_carrier_mk {α : Type u} [inst : ] {a : α} :
theorem ConjClasses.mem_carrier_iff_mk_eq {α : Type u} [inst : ] {a : α} {b : } :
theorem ConjClasses.carrier_eq_preimage_mk {α : Type u} [inst : ] {a : } :
= ConjClasses.mk ⁻¹' {a}