Documentation

Mathlib.Algebra.Group.Conj

Conjugacy of group elements #

See also MulAut.conj and Quandle.conj.

source
ink
def IsConj {α : Type u} [inst : Monoid α] (a : α) (b : α) :
Prop

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

Equations
source
ink
theorem IsConj.refl {α : Type u} [inst : Monoid α] (a : α) :
IsConj a a
source
ink
theorem IsConj.symm {α : Type u} [inst : Monoid α] {a : α} {b : α} :
IsConj a b → IsConj b a
source
ink
theorem isConj_comm {α : Type u} [inst : Monoid α] {g : α} {h : α} :
IsConj g h ↔ IsConj h g
source
ink
theorem IsConj.trans {α : Type u} [inst : Monoid α] {a : α} {b : α} {c : α} :
IsConj a b → IsConj b c → IsConj a c
source
ink
@[simp]
theorem isConj_iff_eq {α : Type u_1} [inst : CommMonoid α] {a : α} {b : α} :
IsConj a b ↔ a = b
source
ink
theorem MonoidHom.map_isConj {α : Type u} {β : Type v} [inst : Monoid α] [inst : Monoid β] (f : α →* β) {a : α} {b : α} :
IsConj a b → IsConj (↑f a) (↑f b)
source
ink
@[simp]
theorem isConj_one_right {α : Type u} [inst : CancelMonoid α] {a : α} :
IsConj 1 a ↔ a = 1
source
ink
@[simp]
theorem isConj_one_left {α : Type u} [inst : CancelMonoid α] {a : α} :
IsConj a 1 ↔ a = 1
source
ink
@[simp]
theorem isConj_iff {α : Type u} [inst : Group α] {a : α} {b : α} :
IsConj a b ↔ ∃ c, c * a * c⁻¹ = b
source
ink
theorem conj_inv {α : Type u} [inst : Group α] {a : α} {b : α} :
(b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹
source
ink
@[simp]
theorem conj_mul {α : Type u} [inst : Group α] {a : α} {b : α} {c : α} :
b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹
source
ink
@[simp]
theorem conj_pow {α : Type u} [inst : Group α] {i : ℕ} {a : α} {b : α} :
(a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
source
ink
@[simp]
theorem conj_zpow {α : Type u} [inst : Group α] {i : ℤ} {a : α} {b : α} :
(a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
source
ink
theorem conj_injective {α : Type u} [inst : Group α] {x : α} :
Function.Injective fun g => x * g * x⁻¹
source
ink
@[simp]
theorem isConj_iff₀ {α : Type u} [inst : GroupWithZero α] {a : α} {b : α} :
IsConj a b ↔ ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b
source
ink
def IsConj.setoid (α : Type u_1) [inst : Monoid α] :
Setoid α

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

Equations
source
ink
def ConjClasses (α : Type u_1) [inst : Monoid α] :
Type u_1

The quotient type of conjugacy classes of a group.

Equations
source
ink
def ConjClasses.mk {α : Type u_1} [inst : Monoid α] (a : α) :
ConjClasses α

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

Equations
source
ink
instance ConjClasses.instInhabitedConjClasses {α : Type u} [inst : Monoid α] :
Inhabited (ConjClasses α)
Equations
source
ink
theorem ConjClasses.mk_eq_mk_iff_isConj {α : Type u} [inst : Monoid α] {a : α} {b : α} :
ConjClasses.mk a = ConjClasses.mk b ↔ IsConj a b
source
ink
theorem ConjClasses.quotient_mk_eq_mk {α : Type u} [inst : Monoid α] (a : α) :
Quotient.mk (IsConj.setoid α) a = ConjClasses.mk a
source
ink
theorem ConjClasses.quot_mk_eq_mk {α : Type u} [inst : Monoid α] (a : α) :
Quot.mk Setoid.r a = ConjClasses.mk a
source
ink
theorem ConjClasses.forall_isConj {α : Type u} [inst : Monoid α] {p : ConjClasses α → Prop} :
((a : ConjClasses α) → p a) ↔ (a : α) → p (ConjClasses.mk a)
source
ink
theorem ConjClasses.mk_surjective {α : Type u} [inst : Monoid α] :
Function.Surjective ConjClasses.mk
source
ink
instance ConjClasses.instOneConjClasses {α : Type u} [inst : Monoid α] :
One (ConjClasses α)
Equations
source
ink
theorem ConjClasses.one_eq_mk_one {α : Type u} [inst : Monoid α] :
1 = ConjClasses.mk 1
source
ink
theorem ConjClasses.exists_rep {α : Type u} [inst : Monoid α] (a : ConjClasses α) :
∃ a0, ConjClasses.mk a0 = a
source
ink
def ConjClasses.map {α : Type u} {β : Type v} [inst : Monoid α] [inst : Monoid β] (f : α →* β) :
ConjClasses α → ConjClasses β

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

Equations
source
ink
theorem ConjClasses.map_surjective {α : Type u} {β : Type v} [inst : Monoid α] [inst : Monoid β] {f : α →* β} (hf : Function.Surjective ↑f) :
Function.Surjective (ConjClasses.map f)
source
ink
instance ConjClasses.instDecidableEqConjClasses {α : Type u} [inst : Monoid α] [inst : DecidableRel IsConj] :
DecidableEq (ConjClasses α)
Equations
  • ConjClasses.instDecidableEqConjClasses = instDecidableEqQuotient
source
ink
theorem ConjClasses.mk_injective {α : Type u} [inst : CommMonoid α] :
Function.Injective ConjClasses.mk
source
ink
theorem ConjClasses.mk_bijective {α : Type u} [inst : CommMonoid α] :
Function.Bijective ConjClasses.mk
source
ink
def ConjClasses.mkEquiv {α : Type u} [inst : CommMonoid α] :
α ≃ ConjClasses α

The bijection between a CommGroup and its ConjClasses.

Equations
  • One or more equations did not get rendered due to their size.
source
ink
def conjugatesOf {α : Type u} [inst : Monoid α] (a : α) :
Set α

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

Equations
source
ink
theorem mem_conjugatesOf_self {α : Type u} [inst : Monoid α] {a : α} :
a ∈ conjugatesOf a
source
ink
theorem IsConj.conjugatesOf_eq {α : Type u} [inst : Monoid α] {a : α} {b : α} (ab : IsConj a b) :
conjugatesOf a = conjugatesOf b
source
ink
theorem isConj_iff_conjugatesOf_eq {α : Type u} [inst : Monoid α] {a : α} {b : α} :
IsConj a b ↔ conjugatesOf a = conjugatesOf b
source
ink
def ConjClasses.carrier {α : Type u} [inst : Monoid α] :
ConjClasses α → Set α

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

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