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
Instances for is_conj
source
@[refl]
theorem is_conj.refl {α : Type u} [monoid α] (a : α) :
is_conj a a
source
@[symm]
theorem is_conj.symm {α : Type u} [monoid α] {a b : α} :
is_conj a b → is_conj b a
source
theorem is_conj_comm {α : Type u} [monoid α] {g h : α} :
is_conj g h ↔ is_conj h g
source
@[trans]
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
Instances for conj_classes
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
def library_note.slow-failing instance priority  :
unit

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

source
@[protected, instance]
def conj_classes.decidable_eq {α : Type u} [monoid α] [decidable_rel is_conj] :
decidable_eq (conj_classes α)
Equations
source
@[protected, instance]
def conj_classes.is_conj.decidable_rel {α : Type u} [monoid α] [decidable_eq α] [fintype α] :
decidable_rel is_conj
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
Instances for ↥conjugates_of
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
@[protected, instance]
def conjugates_of.fintype {α : Type u} [monoid α] [fintype α] [decidable_rel is_conj] {a : α} :
fintype ↥(conjugates_of a)
Equations
source
def conj_classes.carrier {α : Type u} [monoid α] :
conj_classes α → set α

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

Equations
Instances for ↥conj_classes.carrier
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}
source
@[protected, instance]
def conj_classes.carrier.fintype {α : Type u} [monoid α] [fintype α] [decidable_rel is_conj] {x : conj_classes α} :
fintype ↥(x.carrier)
Equations