Conjugacy of group elements #
See also MulAut.conj
and Quandle.conj
.
@[simp]
The quotient type of conjugacy classes of a group.
Instances For
The canonical quotient map from a monoid α
into the ConjClasses
of α
Instances For
theorem
ConjClasses.mk_eq_mk_iff_isConj
{α : Type u}
[Monoid α]
{a : α}
{b : α}
:
ConjClasses.mk a = ConjClasses.mk b ↔ IsConj a b
theorem
ConjClasses.quotient_mk_eq_mk
{α : Type u}
[Monoid α]
(a : α)
:
Quotient.mk (IsConj.setoid α) a = ConjClasses.mk a
theorem
ConjClasses.quot_mk_eq_mk
{α : Type u}
[Monoid α]
(a : α)
:
Quot.mk Setoid.r a = ConjClasses.mk a
theorem
ConjClasses.forall_isConj
{α : Type u}
[Monoid α]
{p : ConjClasses α → Prop}
:
((a : ConjClasses α) → p a) ↔ (a : α) → p (ConjClasses.mk a)
theorem
ConjClasses.exists_rep
{α : Type u}
[Monoid α]
(a : ConjClasses α)
:
∃ a0, ConjClasses.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.
Instances For
theorem
ConjClasses.map_surjective
{α : Type u}
{β : Type v}
[Monoid α]
[Monoid β]
{f : α →* β}
(hf : Function.Surjective ↑f)
:
The bijection between a CommGroup
and its ConjClasses
.
Instances For
Given an element a
, conjugatesOf a
is the set of conjugates.
Instances For
theorem
isConj_iff_conjugatesOf_eq
{α : Type u}
[Monoid α]
{a : α}
{b : α}
:
IsConj a b ↔ conjugatesOf a = conjugatesOf b
Given a conjugacy class a
, carrier a
is the set it represents.
Instances For
theorem
ConjClasses.mem_carrier_iff_mk_eq
{α : Type u}
[Monoid α]
{a : α}
{b : ConjClasses α}
:
a ∈ ConjClasses.carrier b ↔ ConjClasses.mk a = b
theorem
ConjClasses.carrier_eq_preimage_mk
{α : Type u}
[Monoid α]
{a : ConjClasses α}
:
ConjClasses.carrier a = ConjClasses.mk ⁻¹' {a}