mathlib documentation

algebra.group.conj

Conjugacy of group elements #

See also mul_aut.conj and quandle.conj.

def is_conj {α : Type u} [monoid α] (a b : α) :
Prop

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

Equations
theorem is_conj.refl {α : Type u} [monoid α] (a : α) :
theorem is_conj.symm {α : Type u} [monoid α] {a b : α} :
is_conj a bis_conj b a
theorem is_conj.trans {α : Type u} [monoid α] {a b c : α} :
is_conj a bis_conj b cis_conj a c
@[simp]
theorem is_conj_iff_eq {α : Type u_1} [comm_monoid α] {a b : α} :
is_conj a b a = b
@[protected]
theorem monoid_hom.map_is_conj {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α →* β) {a b : α} :
is_conj a bis_conj (f a) (f b)
@[simp]
theorem is_conj_iff {α : Type u} [group α] {a b : α} :
is_conj a b ∃ (c : α), (c * a) * c⁻¹ = b
@[simp]
theorem is_conj_one_right {α : Type u} [group α] {a : α} :
is_conj 1 a a = 1
@[simp]
theorem is_conj_one_left {α : Type u} [group α] {a : α} :
is_conj a 1 a = 1
@[simp]
theorem conj_inv {α : Type u} [group α] {a b : α} :
((b * a) * b⁻¹)⁻¹ = (b * a⁻¹) * b⁻¹
@[simp]
theorem conj_mul {α : Type u} [group α] {a b c : α} :
((b * a) * b⁻¹) * (b * c) * b⁻¹ = (b * a * c) * b⁻¹
@[simp]
theorem conj_pow {α : Type u} [group α] {i : } {a b : α} :
((a * b) * a⁻¹) ^ i = (a * b ^ i) * a⁻¹
@[simp]
theorem conj_zpow {α : Type u} [group α] {i : } {a b : α} :
((a * b) * a⁻¹) ^ i = (a * b ^ i) * a⁻¹
theorem conj_injective {α : Type u} [group α] {x : α} :
function.injective (λ (g : α), (x * g) * x⁻¹)
@[simp]
theorem is_conj_iff₀ {α : Type u} [group_with_zero α] {a b : α} :
is_conj a b ∃ (c : α), c 0 (c * a) * c⁻¹ = b
@[protected]
def is_conj.setoid (α : Type u_1) [monoid α] :

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

Equations
def conj_classes (α : Type u_1) [monoid α] :
Type u_1

The quotient type of conjugacy classes of a group.

Equations
@[protected]
def conj_classes.mk {α : Type u_1} [monoid α] (a : α) :

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

Equations
@[protected, instance]
def conj_classes.inhabited {α : Type u} [monoid α] :
Equations
theorem conj_classes.mk_eq_mk_iff_is_conj {α : Type u} [monoid α] {a b : α} :
theorem conj_classes.quotient_mk_eq_mk {α : Type u} [monoid α] (a : α) :
theorem conj_classes.quot_mk_eq_mk {α : Type u} [monoid α] (a : α) :
theorem conj_classes.forall_is_conj {α : Type u} [monoid α] {p : conj_classes α → Prop} :
(∀ (a : conj_classes α), p a) ∀ (a : α), p (conj_classes.mk a)
@[protected, instance]
def conj_classes.has_one {α : Type u} [monoid α] :
Equations
theorem conj_classes.one_eq_mk_one {α : Type u} [monoid α] :
theorem conj_classes.exists_rep {α : Type u} [monoid α] (a : conj_classes α) :
∃ (a0 : α), conj_classes.mk a0 = a
def conj_classes.map {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α →* β) :

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

Equations
@[protected, instance]
Equations
def conj_classes.mk_equiv {α : Type u} [comm_monoid α] :

The bijection between a comm_group and its conj_classes.

Equations
def conjugates_of {α : Type u} [monoid α] (a : α) :
set α

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

Equations
theorem mem_conjugates_of_self {α : Type u} [monoid α] {a : α} :
theorem is_conj.conjugates_of_eq {α : Type u} [monoid α] {a b : α} (ab : is_conj a b) :
theorem is_conj_iff_conjugates_of_eq {α : Type u} [monoid α] {a b : α} :
def conj_classes.carrier {α : Type u} [monoid α] :
conj_classes αset α

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

Equations
theorem conj_classes.mem_carrier_mk {α : Type u} [monoid α] {a : α} :
theorem conj_classes.mem_carrier_iff_mk_eq {α : Type u} [monoid α] {a : α} {b : conj_classes α} :