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

def IsAddConj {α : Type u} [AddMonoid α] (a b : α) : Prop

We say that a is additively conjugate to b if for some additive unit c we have c + a + -c = b.

Equations

• IsAddConj a b = ∃ (c : AddUnits α), AddSemiconjBy (↑c) a b

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

theorem IsAddConj.refl {α : Type u} [AddMonoid α] (a : α) : IsAddConj a a

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

theorem IsAddConj.symm {α : Type u} [AddMonoid α] {a b : α} : IsAddConj a b → IsAddConj b a

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

theorem isAddConj_comm {α : Type u} [AddMonoid α] {g h : α} : IsAddConj g h ↔ IsAddConj h g

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

theorem IsAddConj.trans {α : Type u} [AddMonoid α] {a b c : α} : IsAddConj a b → IsAddConj b c → IsAddConj a c

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

theorem IsAddConj.nsmul {α : Type u} [AddMonoid α] {a b : α} (n : ℕ) : IsAddConj a b → IsAddConj (n • a) (n • b)

@[simp]

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

@[simp]

theorem isAddConj_iff_eq {α : Type u_1} [AddCommMonoid α] {a b : α} : IsAddConj 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)

theorem AddMonoidHom.map_isAddConj {α : Type u} {β : Type v} [AddMonoid α] [AddMonoid β] (f : α →+ β) {a b : α} : IsAddConj a b → IsAddConj (f a) (f b)

@[simp]

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

@[simp]

theorem isAddConj_zero_right {α : Type u} [AddMonoid α] {a : α} : IsAddConj 0 a ↔ a = 0

@[simp]

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

@[simp]

theorem isAddConj_zero_left {α : Type u} [AddMonoid α] {a : α} : IsAddConj a 0 ↔ a = 0

@[simp]

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

@[simp]

theorem isAddConj_iff {α : Type u} [AddGroup α] {a b : α} : IsAddConj a b ↔ ∃ (c : α), c + a + -c = b

theorem conj_inv {α : Type u} [Group α] {a b : α} : (b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹

theorem addConj_neg {α : Type u} [AddGroup α] {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 addConj_add {α : Type u} [AddGroup α] {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 addConj_nsmul {α : Type u} [AddGroup α] {i : ℕ} {a b : α} : i • (a + b + -a) = a + i • b + -a

@[simp]

theorem conj_zpow {α : Type u} [Group α] {i : ℤ} {a b : α} : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

@[simp]

theorem addConj_zsmul {α : Type u} [AddGroup α] {i : ℤ} {a b : α} : i • (a + b + -a) = a + i • b + -a

theorem conj_injective {α : Type u} [Group α] {x : α} : Function.Injective fun (g : α) => x * g * x⁻¹

theorem addConj_injective {α : Type u} [AddGroup α] {x : α} : Function.Injective fun (g : α) => x + g + -x

@[implicit_reducible]

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 := ⋯ }

@[implicit_reducible]

def IsAddConj.setoid (α : Type u_1) [AddMonoid α] : Setoid α

The setoid of the relation IsAddConj iff there is an additive unit u such that u + x = y + u

Equations

• IsAddConj.setoid α = { r := IsAddConj, 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 AddConjClasses (α : Type u_1) [AddMonoid α] : Type u_1

The quotient type of additive conjugacy classes of an additive group.

Equations

• AddConjClasses α = Quotient (IsAddConj.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⟧

def AddConjClasses.mk {α : Type u_1} [AddMonoid α] (a : α) : AddConjClasses α

The canonical quotient map from an additive monoid α into the AddConjClasses of α

Equations

• AddConjClasses.mk a = ⟦a⟧

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance AddConjClasses.instInhabited {α : Type u} [AddMonoid α] : Inhabited (AddConjClasses α)

Equations

• AddConjClasses.instInhabited = { default := ⟦0⟧ }

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

theorem AddConjClasses.mk_eq_mk_iff_isAddConj {α : Type u} [AddMonoid α] {a b : α} : AddConjClasses.mk a = AddConjClasses.mk b ↔ IsAddConj a b

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

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

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

theorem AddConjClasses.quot_mk_eq_mk {α : Type u} [AddMonoid α] (a : α) : Quot.mk (⇑(IsAddConj.setoid α)) a = AddConjClasses.mk a

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

theorem AddConjClasses.forall_isAddConj {α : Type u} [AddMonoid α] {p : AddConjClasses α → Prop} : (∀ (a : AddConjClasses α), p a) ↔ ∀ (a : α), p (AddConjClasses.mk a)

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

theorem AddConjClasses.mk_surjective {α : Type u} [AddMonoid α] : Function.Surjective AddConjClasses.mk

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance AddConjClasses.instZero {α : Type u} [AddMonoid α] : Zero (AddConjClasses α)

Equations

• AddConjClasses.instZero = { zero := ⟦0⟧ }

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

theorem AddConjClasses.zero_eq_mk_zero {α : Type u} [AddMonoid α] : 0 = AddConjClasses.mk 0

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

theorem AddConjClasses.exists_rep {α : Type u} [AddMonoid α] (a : AddConjClasses α) : ∃ (a0 : α), AddConjClasses.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) ⋯

def AddConjClasses.map {α : Type u} {β : Type v} [AddMonoid α] [AddMonoid β] (f : α →+ β) : AddConjClasses α → AddConjClasses β

An AddMonoidHom maps additive conjugacy classes of one additive group to additive conjugacy classes of another.

Equations

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

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

theorem AddConjClasses.map_surjective {α : Type u} {β : Type v} [AddMonoid α] [AddMonoid β] {f : α →+ β} (hf : Function.Surjective ⇑f) : Function.Surjective (map f)

def LibraryNote.«slow-failing_instance_priority» : Batteries.Util.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

• LibraryNote.«slow-failing_instance_priority» = default

@[implicit_reducible]

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

Equations

• ConjClasses.instDecidableEqOfDecidableRelIsConj = ConjClasses.instDecidableEqOfDecidableRelIsConj._aux_1

@[implicit_reducible]

instance AddConjClasses.instDecidableEqOfDecidableRelIsAddConj {α : Type u} [AddMonoid α] [DecidableRel IsAddConj] : DecidableEq (AddConjClasses α)

Equations

• AddConjClasses.instDecidableEqOfDecidableRelIsAddConj = AddConjClasses.instDecidableEqOfDecidableRelIsAddConj._aux_1

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

theorem AddConjClasses.mk_injective {α : Type u} [AddCommMonoid α] : Function.Injective AddConjClasses.mk

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

theorem AddConjClasses.mk_bijective {α : Type u} [AddCommMonoid α] : Function.Bijective AddConjClasses.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 AddConjClasses.mkEquiv {α : Type u} [AddCommMonoid α] : α ≃ AddConjClasses α

The bijection between an AddCommGroup and its AddConjClasses.

Equations

• AddConjClasses.mkEquiv = { toFun := AddConjClasses.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}

def addConjugatesOf {α : Type u} [AddMonoid α] (a : α) : Set α

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

Equations

• addConjugatesOf a = {b : α | IsAddConj a b}

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

theorem mem_addConjugatesOf_self {α : Type u} [AddMonoid α] {a : α} : a ∈ addConjugatesOf a

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

theorem IsAddConj.addConjugatesOf_eq {α : Type u} [AddMonoid α] {a b : α} (ab : IsAddConj a b) : addConjugatesOf a = addConjugatesOf b

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

theorem isAddConj_iff_addConjugatesOf_eq {α : Type u} [AddMonoid α] {a b : α} : IsAddConj a b ↔ addConjugatesOf a = addConjugatesOf 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 ⋯

def AddConjClasses.carrier {α : Type u} [AddMonoid α] : AddConjClasses α → Set α

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

Equations

• AddConjClasses.carrier = Quotient.lift addConjugatesOf ⋯

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

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

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

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

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

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