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

@[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} [CancelMonoid α] {a : α} : IsConj 1 a ↔ a = 1

@[simp]

theorem isConj_one_left {α : Type u} [CancelMonoid α] {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 (ConjClasses.map f)

@[instance 900]

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}