Documentation

Mathlib.Algebra.Group.Conj

Conjugacy of group elements #

See also MulAut.conj and Quandle.conj.

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

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 : Monoid α] :
Type u_1

The quotient type of conjugacy classes of a group.

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

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

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

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

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

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 : Monoid α] (a : α) :
Set α

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

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

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

Equations
theorem ConjClasses.carrier_eq_preimage_mk {α : Type u} [inst : Monoid α] {a : ConjClasses α} :
ConjClasses.carrier a = ConjClasses.mk ⁻¹' {a}