mathlib3 documentation

Conjugacy of group elements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

See also mul_aut.conj and quandle.conj.

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

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

Instances for is_conj
theorem is_conj.refl {α : Type u} [monoid α] (a : α) :
theorem is_conj.symm {α : Type u} [monoid α] {a b : α} :
theorem is_conj_comm {α : Type u} [monoid α] {g h : α} :
theorem is_conj.trans {α : Type u} [monoid α] {a b c : α} :
theorem is_conj_iff_eq {α : Type u_1} [comm_monoid α] {a b : α} :
is_conj a b a = b
theorem monoid_hom.map_is_conj {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α →* β) {a b : α} :
is_conj a b is_conj (f a) (f b)
theorem is_conj_one_right {α : Type u} [cancel_monoid α] {a : α} :
is_conj 1 a a = 1
theorem is_conj_one_left {α : Type u} [cancel_monoid α] {a : α} :
is_conj a 1 a = 1
theorem is_conj_iff {α : Type u} [group α] {a b : α} :
is_conj a b (c : α), c * a * c⁻¹ = b
theorem conj_inv {α : Type u} [group α] {a b : α} :
(b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹
theorem conj_mul {α : Type u} [group α] {a b c : α} :
b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹
theorem conj_pow {α : Type u} [group α] {i : } {a b : α} :
(a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
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⁻¹)
theorem is_conj_iff₀ {α : Type u} [group_with_zero α] {a b : α} :
is_conj a b (c : α), c 0 c * a * c⁻¹ = b
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

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

The quotient type of conjugacy classes of a group.

Instances for conj_classes
def {α : Type u_1} [monoid α] (a : α) :

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

@[protected, instance]
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 ( a)
@[protected, instance]
theorem conj_classes.exists_rep {α : Type u} [monoid α] (a : conj_classes α) :
(a0 : α), a0 = a
def {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α →* β) :

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


Certain instances trigger further searches when they are considered as candidate instances; these instances should be assigned a priority lower than the default of 1000 (for example, 900).

The conditions for this rule are as follows:

  • a class C has instances instT : C T and instT' : C T'
  • types T and T' are both specializations of another type S
  • the parameters supplied to S to produce T are not (fully) determined by instT, instead they have to be found by instance search If those conditions hold, the instance instT should be assigned lower priority.

For example, suppose the search for an instance of decidable_eq (multiset α) tries the candidate instance con.quotient.decidable_eq (c : con M) : decidable_eq c.quotient. Since multiset and con.quotient are both quotient types, unification will check that the relations list.perm and c.to_setoid.r unify. However, c.to_setoid depends on a has_mul M instance, so this unification triggers a search for has_mul (list α); this will traverse all subclasses of has_mul before failing. On the other hand, the search for an instance of decidable_eq (con.quotient c) for c : con M can quickly reject the candidate instance multiset.has_decidable_eq because the type of list.perm : list ?m_1 → list ?m_1 → Prop does not unify with M → M → Prop. Therefore, we should assign con.quotient.decidable_eq a lower priority because it fails slowly. (In terms of the rules above, C := decidable_eq, T := con.quotient, instT := con.quotient.decidable_eq, T' := multiset, instT' := multiset.has_decidable_eq, and S := quot.)

If the type involved is a free variable (rather than an instantiation of some type S), the instance priority should be even lower, see Note [lower instance priority].

The bijection between a comm_group and its conj_classes.

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

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

Instances for conjugates_of
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 α] :

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

Instances for conj_classes.carrier
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 α} :