mathlib documentation

algebra.group.conj

Conjugacy of group elements #

See also mul_aut.conj and quandle.conj.

source
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
source
theorem is_conj.refl {α : Type u} [monoid α] (a : α) :
is_conj a a
source
theorem is_conj.symm {α : Type u} [monoid α] {a b : α} :
is_conj a b → is_conj b a
source
theorem is_conj.trans {α : Type u} [monoid α] {a b c : α} :
is_conj a b → is_conj b c → is_conj a c
source
@[simp]
theorem is_conj_iff_eq {α : Type u_1} [comm_monoid α] {a b : α} :
is_conj a b ↔ a = b
source
@[protected]
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)
source
@[simp]
theorem is_conj_one_right {α : Type u} [cancel_monoid α] {a : α} :
is_conj 1 a ↔ a = 1
source
@[simp]
theorem is_conj_one_left {α : Type u} [cancel_monoid α] {a : α} :
is_conj a 1 ↔ a = 1
source
@[simp]
theorem is_conj_iff {α : Type u} [group α] {a b : α} :
is_conj a b ↔ ∃ (c : α), (c * a) * c⁻¹ = b
source
@[simp]
theorem conj_inv {α : Type u} [group α] {a b : α} :
((b * a) * b⁻¹)⁻¹ = (b * a⁻¹) * b⁻¹
source
@[simp]
theorem conj_mul {α : Type u} [group α] {a b c : α} :
((b * a) * b⁻¹) * (b * c) * b⁻¹ = (b * a * c) * b⁻¹
source
@[simp]
theorem conj_pow {α : Type u} [group α] {i : ℕ} {a b : α} :
((a * b) * a⁻¹) ^ i = (a * b ^ i) * a⁻¹
source
@[simp]
theorem conj_zpow {α : Type u} [group α] {i : ℤ} {a b : α} :
((a * b) * a⁻¹) ^ i = (a * b ^ i) * a⁻¹
source
theorem conj_injective {α : Type u} [group α] {x : α} :
function.injective (λ (g : α), (x * g) * x⁻¹)
source
@[simp]
theorem is_conj_iff₀ {α : Type u} [group_with_zero α] {a b : α} :
is_conj a b ↔ ∃ (c : α), c ≠ 0 ∧ (c * a) * c⁻¹ = b
source
@[protected]
def is_conj.setoid (α : Type u_1) [monoid α] :
setoid α

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

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

The quotient type of conjugacy classes of a group.

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

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

Equations
source
@[protected, instance]
def conj_classes.inhabited {α : Type u} [monoid α] :
inhabited (conj_classes α)
Equations
source
theorem conj_classes.mk_eq_mk_iff_is_conj {α : Type u} [monoid α] {a b : α} :
conj_classes.mk a = conj_classes.mk b ↔ is_conj a b
source
theorem conj_classes.quotient_mk_eq_mk {α : Type u} [monoid α] (a : α) :
⟦a⟧ = conj_classes.mk a
source
theorem conj_classes.quot_mk_eq_mk {α : Type u} [monoid α] (a : α) :
quot.mk setoid.r a = conj_classes.mk a
source
theorem conj_classes.forall_is_conj {α : Type u} [monoid α] {p : conj_classes α → Prop} :
(∀ (a : conj_classes α), p a) ↔ ∀ (a : α), p (conj_classes.mk a)
source
theorem conj_classes.mk_surjective {α : Type u} [monoid α] :
function.surjective conj_classes.mk
source
@[protected, instance]
def conj_classes.has_one {α : Type u} [monoid α] :
has_one (conj_classes α)
Equations
source
theorem conj_classes.one_eq_mk_one {α : Type u} [monoid α] :
1 = conj_classes.mk 1
source
theorem conj_classes.exists_rep {α : Type u} [monoid α] (a : conj_classes α) :
∃ (a0 : α), conj_classes.mk a0 = a
source
def conj_classes.map {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α →* β) :
conj_classes α → conj_classes β

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

Equations
source
theorem conj_classes.map_surjective {α : Type u} {β : Type v} [monoid α] [monoid β] {f : α →* β} (hf : function.surjective ⇑f) :
function.surjective (conj_classes.map f)
source
@[protected, instance]
def conj_classes.fintype {α : Type u} [monoid α] [fintype α] [decidable_rel is_conj] :
fintype (conj_classes α)
Equations
source
theorem conj_classes.mk_injective {α : Type u} [comm_monoid α] :
function.injective conj_classes.mk
source
theorem conj_classes.mk_bijective {α : Type u} [comm_monoid α] :
function.bijective conj_classes.mk
source
def conj_classes.mk_equiv {α : Type u} [comm_monoid α] :
α ≃ conj_classes α

The bijection between a comm_group and its conj_classes.

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

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

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

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

Equations
source
theorem conj_classes.mem_carrier_mk {α : Type u} [monoid α] {a : α} :
a ∈ (conj_classes.mk a).carrier
source
theorem conj_classes.mem_carrier_iff_mk_eq {α : Type u} [monoid α] {a : α} {b : conj_classes α} :
a ∈ b.carrier ↔ conj_classes.mk a = b
source
theorem conj_classes.carrier_eq_preimage_mk {α : Type u} [monoid α] {a : conj_classes α} :
a.carrier = conj_classes.mk ⁻¹' {a}