mathlib3 documentation

algebra.group.conj

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 : α) :

Prop

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

Equations

is_conj a b = ∃ (c : αˣ), semiconj_by ↑c a b

@[refl]

theorem is_conj.refl {α : Type u} [monoid α] (a : α) :

@[symm]

theorem is_conj.symm {α : Type u} [monoid α] {a b : α} :

is_conj a b → is_conj b a

theorem is_conj_comm {α : Type u} [monoid α] {g h : α} :

is_conj g h ↔ is_conj h g

@[trans]

theorem is_conj.trans {α : Type u} [monoid α] {a b c : α} :

is_conj a b → is_conj b c → is_conj a c

@[simp]

theorem is_conj_iff_eq {α : Type u_1} [comm_monoid α] {a b : α} :

is_conj a b ↔ a = b

@[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)

@[simp]

theorem is_conj_one_right {α : Type u} [cancel_monoid α] {a : α} :

is_conj 1 a ↔ a = 1

@[simp]

theorem is_conj_one_left {α : Type u} [cancel_monoid α] {a : α} :

is_conj a 1 ↔ a = 1

@[simp]

theorem is_conj_iff {α : Type u} [group α] {a b : α} :

is_conj a b ↔ ∃ (c : α), c * a * c⁻¹ = b

@[simp]

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

@[simp]

theorem is_conj_iff₀ {α : Type u} [group_with_zero α] {a b : α} :

is_conj a b ↔ ∃ (c : α), c ≠ 0 ∧ c * a * c⁻¹ = b

@[protected]

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

Equations

is_conj.setoid α = {r := is_conj _inst_1, iseqv := _}

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

Type u_1

The quotient type of conjugacy classes of a group.

Equations

conj_classes α = quotient (is_conj.setoid α)

Instances for conj_classes

@[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

conj_classes.mk a = ⟦a⟧

@[protected, instance]

def conj_classes.inhabited {α : Type u} [monoid α] :

inhabited (conj_classes α)

Equations

conj_classes.inhabited = {default := ⟦1⟧}

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

theorem conj_classes.quotient_mk_eq_mk {α : Type u} [monoid α] (a : α) :

⟦a⟧ = conj_classes.mk a

theorem conj_classes.quot_mk_eq_mk {α : Type u} [monoid α] (a : α) :

quot.mk setoid.r a = conj_classes.mk a

theorem conj_classes.forall_is_conj {α : Type u} [monoid α] {p : conj_classes α → Prop} :

(∀ (a : conj_classes α), p a) ↔ ∀ (a : α), p (conj_classes.mk a)

theorem conj_classes.mk_surjective {α : Type u} [monoid α] :

function.surjective conj_classes.mk

@[protected, instance]

def conj_classes.has_one {α : Type u} [monoid α] :

has_one (conj_classes α)

Equations

conj_classes.has_one = {one := ⟦1⟧}

theorem conj_classes.one_eq_mk_one {α : Type u} [monoid α] :

1 = conj_classes.mk 1

theorem conj_classes.exists_rep {α : Type u} [monoid α] (a : conj_classes α) :

∃ (a0 : α), conj_classes.mk a0 = a

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

conj_classes.map f = quotient.lift (conj_classes.mk ∘ ⇑f) _

theorem conj_classes.map_surjective {α : Type u} {β : Type v} [monoid α] [monoid β] {f : α →* β} (hf : function.surjective ⇑f) :

function.surjective (conj_classes.map f)

def library_note.slow-failing instance priority :

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

@[protected, instance]

def conj_classes.decidable_eq {α : Type u} [monoid α] [decidable_rel is_conj] :

decidable_eq (conj_classes α)

Equations

conj_classes.decidable_eq = quotient.decidable_eq

theorem conj_classes.mk_injective {α : Type u} [comm_monoid α] :

function.injective conj_classes.mk

theorem conj_classes.mk_bijective {α : Type u} [comm_monoid α] :

function.bijective conj_classes.mk

def conj_classes.mk_equiv {α : Type u} [comm_monoid α] :

α ≃ conj_classes α

The bijection between a comm_group and its conj_classes.

Equations

conj_classes.mk_equiv = {to_fun := conj_classes.mk (comm_monoid.to_monoid α), inv_fun := quotient.lift id conj_classes.mk_equiv._proof_1, left_inv := _, right_inv := _}

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

set α

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

Equations

conjugates_of a = {b : α | is_conj a b}

theorem mem_conjugates_of_self {α : Type u} [monoid α] {a : α} :

a ∈ conjugates_of a

theorem is_conj.conjugates_of_eq {α : Type u} [monoid α] {a b : α} (ab : is_conj a b) :

conjugates_of a = conjugates_of b

theorem is_conj_iff_conjugates_of_eq {α : Type u} [monoid α] {a b : α} :

is_conj a b ↔ conjugates_of a = conjugates_of b

def conj_classes.carrier {α : Type u} [monoid α] :

conj_classes α → set α

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

Equations

conj_classes.carrier = quotient.lift conjugates_of conj_classes.carrier._proof_1

theorem conj_classes.mem_carrier_mk {α : Type u} [monoid α] {a : α} :

a ∈ (conj_classes.mk a).carrier

theorem conj_classes.mem_carrier_iff_mk_eq {α : Type u} [monoid α] {a : α} {b : conj_classes α} :

a ∈ b.carrier ↔ conj_classes.mk a = b

theorem conj_classes.carrier_eq_preimage_mk {α : Type u} [monoid α] {a : conj_classes α} :

a.carrier = conj_classes.mk ⁻¹' {a}