Conjugacy of group elements

See also MulAut.conj and Quandle.conj.

def IsConj {α : 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

• IsConj a b = ∃ (c : αˣ), SemiconjBy (↑c) a b

theorem IsConj.refl {α : Type u} [Monoid α] (a : α) : IsConj a a

theorem IsConj.symm {α : Type u} [Monoid α] {a b : α} : IsConj a b → IsConj b a

theorem isConj_comm {α : Type u} [Monoid α] {g h : α} : IsConj g h ↔ IsConj h g

theorem IsConj.trans {α : Type u} [Monoid α] {a b c : α} : IsConj a b → IsConj b c → IsConj a c

theorem IsConj.pow {α : Type u} [Monoid α] {a b : α} (n : ℕ) : IsConj a b → IsConj (a ^ n) (b ^ n)

@[simp]

theorem isConj_iff_eq {α : Type u_1} [CommMonoid α] {a b : α} : IsConj a b ↔ a = b

theorem MonoidHom.map_isConj {α : Type u} {β : Type v} [Monoid α] [Monoid β] (f : α →* β) {a b : α} : IsConj a b → IsConj (f a) (f b)

@[simp]

theorem isConj_one_right {α : Type u} [Monoid α] {a : α} : IsConj 1 a ↔ a = 1

@[simp]

theorem isConj_one_left {α : Type u} [Monoid α] {a : α} : IsConj a 1 ↔ a = 1

@[simp]

theorem isConj_iff {α : Type u} [Group α] {a b : α} : IsConj a b ↔ ∃ (c : α), c * a * c⁻¹ = b

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 fun (g : α) => x * g * x⁻¹

def IsConj.setoid (α : Type u_1) [Monoid α] : Setoid α

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

Equations

• IsConj.setoid α = { r := IsConj, iseqv := ⋯ }

def ConjClasses (α : Type u_1) [Monoid α] : Type u_1

The quotient type of conjugacy classes of a group.

Equations

• ConjClasses α = Quotient (IsConj.setoid α)

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

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

Equations

• ConjClasses.mk a = ⟦a⟧

instance ConjClasses.instInhabited {α : Type u} [Monoid α] : Inhabited (ConjClasses α)

Equations

• ConjClasses.instInhabited = { default := ⟦1⟧ }

theorem ConjClasses.mk_eq_mk_iff_isConj {α : Type u} [Monoid α] {a b : α} : ConjClasses.mk a = ConjClasses.mk b ↔ IsConj a b

theorem ConjClasses.quotient_mk_eq_mk {α : Type u} [Monoid α] (a : α) : ⟦a⟧ = ConjClasses.mk a

theorem ConjClasses.quot_mk_eq_mk {α : Type u} [Monoid α] (a : α) : Quot.mk (⇑(IsConj.setoid α)) a = ConjClasses.mk a

theorem ConjClasses.forall_isConj {α : Type u} [Monoid α] {p : ConjClasses α → Prop} : (∀ (a : ConjClasses α), p a) ↔ ∀ (a : α), p (ConjClasses.mk a)

theorem ConjClasses.mk_surjective {α : Type u} [Monoid α] : Function.Surjective ConjClasses.mk

instance ConjClasses.instOne {α : Type u} [Monoid α] : One (ConjClasses α)

Equations

• ConjClasses.instOne = { one := ⟦1⟧ }

theorem ConjClasses.one_eq_mk_one {α : Type u} [Monoid α] : 1 = ConjClasses.mk 1

theorem ConjClasses.exists_rep {α : Type u} [Monoid α] (a : ConjClasses α) : ∃ (a0 : α), ConjClasses.mk a0 = a

def ConjClasses.map {α : Type u} {β : Type v} [Monoid α] [Monoid β] (f : α →* β) : ConjClasses α → ConjClasses β

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

Equations

• ConjClasses.map f = Quotient.lift (ConjClasses.mk ∘ ⇑f) ⋯

theorem ConjClasses.map_surjective {α : Type u} {β : Type v} [Monoid α] [Monoid β] {f : α →* β} (hf : Function.Surjective ⇑f) : Function.Surjective (map f)

def ConjClasses.Mathlib.LibraryNote.«slow-failing instance priority» : LibraryNote

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 reducible 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.

Note that there is no issue unless T and T' are reducibly equal to S, Otherwise the instance discrimination tree can distinguish them, and the note does not apply.

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].

Equations

• ConjClasses.Mathlib.LibraryNote.«slow-failing instance priority» = ()

instance ConjClasses.instDecidableEqOfDecidableRelIsConj {α : Type u} [Monoid α] [DecidableRel IsConj] : DecidableEq (ConjClasses α)

Equations

• ConjClasses.instDecidableEqOfDecidableRelIsConj = inferInstanceAs (DecidableEq (Quotient (IsConj.setoid α)))

theorem ConjClasses.mk_injective {α : Type u} [CommMonoid α] : Function.Injective ConjClasses.mk

theorem ConjClasses.mk_bijective {α : Type u} [CommMonoid α] : Function.Bijective ConjClasses.mk

def ConjClasses.mkEquiv {α : Type u} [CommMonoid α] : α ≃ ConjClasses α

The bijection between a CommGroup and its ConjClasses.

Equations

• ConjClasses.mkEquiv = { toFun := ConjClasses.mk, invFun := Quotient.lift id ⋯, left_inv := ⋯, right_inv := ⋯ }

def conjugatesOf {α : Type u} [Monoid α] (a : α) : Set α

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

Equations

• conjugatesOf a = {b : α | IsConj a b}

theorem mem_conjugatesOf_self {α : Type u} [Monoid α] {a : α} : a ∈ conjugatesOf a

theorem IsConj.conjugatesOf_eq {α : Type u} [Monoid α] {a b : α} (ab : IsConj a b) : conjugatesOf a = conjugatesOf b

theorem isConj_iff_conjugatesOf_eq {α : Type u} [Monoid α] {a b : α} : IsConj a b ↔ conjugatesOf a = conjugatesOf b

def ConjClasses.carrier {α : Type u} [Monoid α] : ConjClasses α → Set α

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

Equations

• ConjClasses.carrier = Quotient.lift conjugatesOf ⋯

theorem ConjClasses.mem_carrier_mk {α : Type u} [Monoid α] {a : α} : a ∈ (ConjClasses.mk a).carrier

theorem ConjClasses.mem_carrier_iff_mk_eq {α : Type u} [Monoid α] {a : α} {b : ConjClasses α} : a ∈ b.carrier ↔ ConjClasses.mk a = b

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