Mathlib.Algebra.Group.Conj

IsConj definition

(a b : α)

Full source

/-- We say that `a` is conjugate to `b` if for some unit `c` we have `c * a * c⁻¹ = b`. -/
def IsConj (a b : α) :=
  ∃ c : αˣ, SemiconjBy (↑c) a b

Conjugacy of group elements

Informal description

Two elements $ a $ and $ b $ in a monoid $ \alpha $ are said to be conjugate if there exists a unit $ c $ in $ \alpha $ such that $ c \cdot a \cdot c^{-1} = b $.

IsConj.refl theorem

(a : α) : IsConj a a

Full source

@[refl]
theorem IsConj.refl (a : α) : IsConj a a :=
  ⟨1, SemiconjBy.one_left a⟩

Reflexivity of Group Element Conjugacy

Informal description

For any element $a$ in a monoid $\alpha$, $a$ is conjugate to itself.

IsConj.symm theorem

{a b : α} : IsConj a b → IsConj b a

Full source

@[symm]
theorem IsConj.symm {a b : α} : IsConj a b → IsConj b a
  | ⟨c, hc⟩ => ⟨c⁻¹, hc.units_inv_symm_left⟩

Symmetry of Conjugacy Relation in Monoids

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, if $a$ is conjugate to $b$, then $b$ is conjugate to $a$. In other words, the conjugacy relation is symmetric.

isConj_comm theorem

{g h : α} : IsConj g h ↔ IsConj h g

Full source

theorem isConj_comm {g h : α} : IsConjIsConj g h ↔ IsConj h g :=
  ⟨IsConj.symm, IsConj.symm⟩

Commutativity of Conjugacy Relation in Monoids

Informal description

For any elements $g$ and $h$ in a monoid $\alpha$, $g$ is conjugate to $h$ if and only if $h$ is conjugate to $g$.

IsConj.trans theorem

{a b c : α} : IsConj a b → IsConj b c → IsConj a c

Full source

@[trans]
theorem IsConj.trans {a b c : α} : IsConj a b → IsConj b c → IsConj a c
  | ⟨c₁, hc₁⟩, ⟨c₂, hc₂⟩ => ⟨c₂ * c₁, hc₂.mul_left hc₁⟩

Transitivity of Conjugacy in Monoids

Informal description

For any elements $a$, $b$, and $c$ in a monoid $\alpha$, if $a$ is conjugate to $b$ and $b$ is conjugate to $c$, then $a$ is conjugate to $c$.

IsConj.pow theorem

{a b : α} (n : ℕ) : IsConj a b → IsConj (a ^ n) (b ^ n)

Full source

theorem IsConj.pow {a b : α} (n : ℕ) : IsConj a b → IsConj (a^n) (b^n)
  | ⟨c, hc⟩ => ⟨c, hc.pow_right n⟩

Conjugacy is preserved under taking powers: $a \sim b \implies a^n \sim b^n$

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, if $a$ and $b$ are conjugate (i.e., there exists a unit $c \in \alpha$ such that $c \cdot a \cdot c^{-1} = b$), then for any natural number $n$, the powers $a^n$ and $b^n$ are also conjugate.

isConj_iff_eq theorem

{α : Type*} [CommMonoid α] {a b : α} : IsConj a b ↔ a = b

Full source

@[simp]
theorem isConj_iff_eq {α : Type*} [CommMonoid α] {a b : α} : IsConjIsConj a b ↔ a = b :=
  ⟨fun ⟨c, hc⟩ => by
    rw [SemiconjBy, mul_comm, ← Units.mul_inv_eq_iff_eq_mul, mul_assoc, c.mul_inv, mul_one] at hc
    exact hc, fun h => by rw [h]⟩

Conjugacy in Commutative Monoids is Equality: $a \sim b \leftrightarrow a = b$

Informal description

Let $\alpha$ be a commutative monoid. For any two elements $a, b \in \alpha$, $a$ is conjugate to $b$ if and only if $a = b$.

MonoidHom.map_isConj theorem

(f : α →* β) {a b : α} : IsConj a b → IsConj (f a) (f b)

Full source

protected theorem MonoidHom.map_isConj (f : α →* β) {a b : α} : IsConj a b → IsConj (f a) (f b)
  | ⟨c, hc⟩ => ⟨Units.map f c, by rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]⟩

Monoid homomorphisms preserve conjugacy: $a \sim b \implies f(a) \sim f(b)$

Informal description

Let $f \colon \alpha \to \beta$ be a monoid homomorphism between monoids $\alpha$ and $\beta$. For any elements $a, b \in \alpha$ that are conjugate in $\alpha$, their images $f(a)$ and $f(b)$ are conjugate in $\beta$.

isConj_one_right theorem

{a : α} : IsConj 1 a ↔ a = 1

Full source

@[simp]
theorem isConj_one_right {a : α} : IsConjIsConj 1 a ↔ a = 1 := by
  refine ⟨fun ⟨c, h⟩ => ?_, fun h => by rw [h]⟩
  rw [SemiconjBy, mul_one] at h
  exact c.isUnit.mul_eq_right.mp h.symm

Conjugacy of Identity: $1 \sim a \leftrightarrow a = 1$

Informal description

For any element $a$ in a monoid $\alpha$, the multiplicative identity $1$ is conjugate to $a$ if and only if $a = 1$.

isConj_one_left theorem

{a : α} : IsConj a 1 ↔ a = 1

Full source

@[simp]
theorem isConj_one_left {a : α} : IsConjIsConj a 1 ↔ a = 1 :=
  calc
    IsConj a 1 ↔ IsConj 1 a := ⟨IsConj.symm, IsConj.symm⟩
    _ ↔ a = 1 := isConj_one_right

Conjugacy of Identity: $a \sim 1 \leftrightarrow a = 1$

Informal description

For any element $a$ in a monoid $\alpha$, $a$ is conjugate to the multiplicative identity $1$ if and only if $a = 1$.

isConj_iff theorem

{a b : α} : IsConj a b ↔ ∃ c : α, c * a * c⁻¹ = b

Full source

@[simp]
theorem isConj_iff {a b : α} : IsConjIsConj a b ↔ ∃ c : α, c * a * c⁻¹ = b :=
  ⟨fun ⟨c, hc⟩ => ⟨c, mul_inv_eq_iff_eq_mul.2 hc⟩, fun ⟨c, hc⟩ =>
    ⟨⟨c, c⁻¹, mul_inv_cancel c, inv_mul_cancel c⟩, mul_inv_eq_iff_eq_mul.1 hc⟩⟩

Characterization of Conjugate Elements: $a \sim b \iff \exists c, c a c^{-1} = b$

Informal description

Two elements $a$ and $b$ in a monoid $\alpha$ are conjugate if and only if there exists an element $c \in \alpha$ such that $c \cdot a \cdot c^{-1} = b$.

conj_inv theorem

{a b : α} : (b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹

Full source

theorem conj_inv {a b : α} : (b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹ :=
  (map_inv (MulAut.conj b) a).symm

Inverse of Conjugate Equals Conjugate of Inverse: $(b a b^{-1})^{-1} = b a^{-1} b^{-1}$

Informal description

For any elements $a$ and $b$ in a group $\alpha$, the inverse of the conjugate $b a b^{-1}$ is equal to the conjugate of the inverse $a^{-1}$ by $b$, i.e., $$ (b a b^{-1})^{-1} = b a^{-1} b^{-1}. $$

conj_mul theorem

{a b c : α} : b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹

Full source

@[simp]
theorem conj_mul {a b c : α} : b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹ :=
  (map_mul (MulAut.conj b) a c).symm

Conjugation Distributes over Group Multiplication

Informal description

For any elements $a, b, c$ in a group $\alpha$, the conjugate of the product $a * c$ by $b$ equals the product of the conjugates of $a$ and $c$ by $b$, i.e., $$ (b a b^{-1}) (b c b^{-1}) = b (a c) b^{-1}. $$

conj_pow theorem

{i : ℕ} {a b : α} : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

Full source

@[simp]
theorem conj_pow {i : ℕ} {a b : α} : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹ := by
  induction' i with i hi
  · simp
  · simp [pow_succ, hi]

Conjugation Commutes with Powers: $(a b a^{-1})^i = a b^i a^{-1}$

Informal description

For any natural number $i$ and elements $a, b$ in a group $\alpha$, the $i$-th power of the conjugate of $b$ by $a$ equals the conjugate of the $i$-th power of $b$ by $a$, i.e., $$ (a b a^{-1})^i = a b^i a^{-1}. $$

conj_zpow theorem

{i : ℤ} {a b : α} : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

Full source

@[simp]
theorem conj_zpow {i : ℤ} {a b : α} : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹ := by
  cases i
  · simp
  · simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]
    rw [mul_assoc]

Conjugation Commutes with Integer Powers: $(a b a^{-1})^i = a b^i a^{-1}$

Informal description

For any integer $i$ and elements $a, b$ in a group $\alpha$, the $i$-th power of the conjugate of $b$ by $a$ equals the conjugate of the $i$-th power of $b$ by $a$, i.e., $$ (a b a^{-1})^i = a b^i a^{-1}. $$

conj_injective theorem

{x : α} : Function.Injective fun g : α => x * g * x⁻¹

Full source

theorem conj_injective {x : α} : Function.Injective fun g : α => x * g * x⁻¹ :=
  (MulAut.conj x).injective

Injectivity of Conjugation in Groups

Informal description

For any element $x$ in a group $\alpha$, the conjugation map $g \mapsto x g x^{-1}$ is injective.

IsConj.setoid definition

(α : Type*) [Monoid α] : Setoid α

Full source

/-- The setoid of the relation `IsConj` iff there is a unit `u` such that `u * x = y * u` -/
protected def setoid (α : Type*) [Monoid α] : Setoid α where
  r := IsConj
  iseqv := ⟨IsConj.refl, IsConj.symm, IsConj.trans⟩

Conjugacy Setoid on a Monoid

Informal description

The setoid (set with an equivalence relation) on a monoid $\alpha$ where two elements are related if and only if they are conjugate, i.e., there exists a unit $u$ such that $u \cdot x = y \cdot u$. The equivalence relation is reflexive, symmetric, and transitive.

ConjClasses definition

(α : Type*) [Monoid α] : Type _

Full source

/-- The quotient type of conjugacy classes of a group. -/
def ConjClasses (α : Type*) [Monoid α] : Type _ :=
  Quotient (IsConj.setoid α)

Conjugacy classes of a monoid

Informal description

The type of conjugacy classes of a monoid $\alpha$, defined as the quotient of $\alpha$ by the equivalence relation of conjugacy. Two elements $x$ and $y$ are conjugate if there exists an element $g$ in $\alpha$ such that $g \cdot x \cdot g^{-1} = y$.

ConjClasses.mk definition

{α : Type*} [Monoid α] (a : α) : ConjClasses α

Full source

/-- The canonical quotient map from a monoid `α` into the `ConjClasses` of `α` -/
protected def mk {α : Type*} [Monoid α] (a : α) : ConjClasses α := ⟦a⟧

Conjugacy class of a monoid element

Informal description

The function maps an element $a$ of a monoid $\alpha$ to its conjugacy class in the quotient space $\text{ConjClasses}(\alpha)$, which consists of all elements conjugate to $a$.

ConjClasses.instInhabited instance

: Inhabited (ConjClasses α)

Full source

instance : Inhabited (ConjClasses α) := ⟨⟦1⟧⟩

Inhabitedness of Conjugacy Classes in a Monoid

Informal description

For any monoid $\alpha$, the type of conjugacy classes of $\alpha$ is inhabited.

ConjClasses.mk_eq_mk_iff_isConj theorem

{a b : α} : ConjClasses.mk a = ConjClasses.mk b ↔ IsConj a b

Full source

theorem mk_eq_mk_iff_isConj {a b : α} : ConjClasses.mkConjClasses.mk a = ConjClasses.mk b ↔ IsConj a b :=
  Iff.intro Quotient.exact Quot.sound

Equality of Conjugacy Classes iff Elements are Conjugate

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, the conjugacy classes of $a$ and $b$ are equal if and only if $a$ and $b$ are conjugate, i.e., there exists an element $g \in \alpha$ such that $g \cdot a \cdot g^{-1} = b$.

ConjClasses.quotient_mk_eq_mk theorem

(a : α) : ⟦a⟧ = ConjClasses.mk a

Full source

theorem quotient_mk_eq_mk (a : α) : ⟦a⟧ = ConjClasses.mk a :=
  rfl

Equivalence Class Equals Conjugacy Class in Monoid

Informal description

For any element $a$ in a monoid $\alpha$, the equivalence class of $a$ under the conjugacy relation is equal to the conjugacy class of $a$, i.e., $\llbracket a \rrbracket = \text{ConjClasses.mk}(a)$.

ConjClasses.quot_mk_eq_mk theorem

(a : α) : Quot.mk Setoid.r a = ConjClasses.mk a

Full source

theorem quot_mk_eq_mk (a : α) : Quot.mk Setoid.r a = ConjClasses.mk a :=
  rfl

Equivalence Class and Conjugacy Class Coincidence in Monoids

Informal description

For any element $a$ in a monoid $\alpha$, the equivalence class of $a$ under the conjugacy relation is equal to the conjugacy class of $a$, i.e., $\text{Quot.mk Setoid.r } a = \text{ConjClasses.mk } a$.

ConjClasses.forall_isConj theorem

{p : ConjClasses α → Prop} : (∀ a, p a) ↔ ∀ a, p (ConjClasses.mk a)

Full source

theorem forall_isConj {p : ConjClasses α → Prop} : (∀ a, p a) ↔ ∀ a, p (ConjClasses.mk a) :=
  Iff.intro (fun h _ => h _) fun h a => Quotient.inductionOn a h

Universal Quantification over Conjugacy Classes

Informal description

For any predicate $p$ on the conjugacy classes of a monoid $\alpha$, the statement that $p$ holds for all conjugacy classes is equivalent to the statement that $p$ holds for the conjugacy class of every element $a \in \alpha$.

ConjClasses.mk_surjective theorem

: Function.Surjective (@ConjClasses.mk α _)

Full source

theorem mk_surjective : Function.Surjective (@ConjClasses.mk α _) :=
  forall_isConj.2 fun a => ⟨a, rfl⟩

Surjectivity of the Conjugacy Class Mapping

Informal description

The function that maps each element $a$ of a monoid $\alpha$ to its conjugacy class $\text{ConjClasses.mk}(a)$ is surjective. That is, every conjugacy class in $\text{ConjClasses}(\alpha)$ is the image of some element $a \in \alpha$ under this mapping.

ConjClasses.instOne instance

: One (ConjClasses α)

Full source

instance : One (ConjClasses α) :=
  ⟨⟦1⟧⟩

Identity Conjugacy Class in a Monoid

Informal description

For any monoid $\alpha$, the type of conjugacy classes $\text{ConjClasses}(\alpha)$ has a distinguished element $1$, which is the conjugacy class of the identity element of $\alpha$.

ConjClasses.one_eq_mk_one theorem

: (1 : ConjClasses α) = ConjClasses.mk 1

Full source

theorem one_eq_mk_one : (1 : ConjClasses α) = ConjClasses.mk 1 :=
  rfl

Identity Conjugacy Class Equals Conjugacy Class of Identity

Informal description

In any monoid $\alpha$, the identity element $1$ in the type of conjugacy classes $\text{ConjClasses}(\alpha)$ is equal to the conjugacy class of the identity element $1$ in $\alpha$, i.e., $1 = \text{ConjClasses.mk}(1)$.

ConjClasses.exists_rep theorem

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

Full source

theorem exists_rep (a : ConjClasses α) : ∃ a0 : α, ConjClasses.mk a0 = a :=
  Quot.exists_rep a

Existence of Representative for Conjugacy Class

Informal description

For any conjugacy class $a$ in a monoid $\alpha$, there exists an element $a_0 \in \alpha$ such that the conjugacy class of $a_0$ equals $a$.

ConjClasses.map definition

(f : α →* β) : ConjClasses α → ConjClasses β

Full source

/-- A `MonoidHom` maps conjugacy classes of one group to conjugacy classes of another. -/
def map (f : α →* β) : ConjClasses α → ConjClasses β :=
  Quotient.lift (ConjClasses.mkConjClasses.mk ∘ f) fun _ _ ab => mk_eq_mk_iff_isConj.2 (f.map_isConj ab)

Image of conjugacy classes under a monoid homomorphism

Informal description

Given a monoid homomorphism $ f \colon \alpha \to \beta $, the function maps a conjugacy class $ C $ in $ \alpha $ to the conjugacy class in $ \beta $ containing the image of any representative of $ C $ under $ f $. This is well-defined because monoid homomorphisms preserve conjugacy relations.

ConjClasses.map_surjective theorem

{f : α →* β} (hf : Function.Surjective f) : Function.Surjective (ConjClasses.map f)

Full source

theorem map_surjective {f : α →* β} (hf : Function.Surjective f) :
    Function.Surjective (ConjClasses.map f) := by
  intro b
  obtain ⟨b, rfl⟩ := ConjClasses.mk_surjective b
  obtain ⟨a, rfl⟩ := hf b
  exact ⟨ConjClasses.mk a, rfl⟩

Surjectivity of Conjugacy Class Map Induced by a Surjective Monoid Homomorphism

Informal description

Given a monoid homomorphism $f \colon \alpha \to \beta$ that is surjective, the induced map on conjugacy classes $\text{ConjClasses.map}(f) \colon \text{ConjClasses}(\alpha) \to \text{ConjClasses}(\beta)$ is also surjective.

ConjClasses.instDecidableEqOfDecidableRelIsConj instance

[DecidableRel (IsConj : α → α → Prop)] : DecidableEq (ConjClasses α)

Full source

instance (priority := 900) [DecidableRel (IsConj : α → α → Prop)] : DecidableEq (ConjClasses α) :=
  inferInstanceAs <| DecidableEq <| Quotient (IsConj.setoid α)

Decidable Equality of Conjugacy Classes in Monoids with Decidable Conjugacy

Informal description

For any monoid $\alpha$ with a decidable conjugacy relation, the set of conjugacy classes of $\alpha$ has decidable equality.

ConjClasses.mk_injective theorem

: Function.Injective (@ConjClasses.mk α _)

Full source

theorem mk_injective : Function.Injective (@ConjClasses.mk α _) := fun _ _ =>
  (mk_eq_mk_iff_isConj.trans isConj_iff_eq).1

Injectivity of the Conjugacy Class Map

Informal description

The function that maps each element $a$ of a monoid $\alpha$ to its conjugacy class $\text{ConjClasses.mk}(a)$ is injective. In other words, if two elements $a$ and $b$ have the same conjugacy class, then $a = b$.

ConjClasses.mk_bijective theorem

: Function.Bijective (@ConjClasses.mk α _)

Full source

theorem mk_bijective : Function.Bijective (@ConjClasses.mk α _) :=
  ⟨mk_injective, mk_surjective⟩

Bijectivity of the Conjugacy Class Map in a Monoid

Informal description

The function that maps each element $a$ of a monoid $\alpha$ to its conjugacy class $\text{ConjClasses.mk}(a)$ is bijective, meaning it is both injective and surjective.

ConjClasses.mkEquiv definition

: α ≃ ConjClasses α

Full source

/-- The bijection between a `CommGroup` and its `ConjClasses`. -/
def mkEquiv : α ≃ ConjClasses α :=
  ⟨ConjClasses.mk, Quotient.lift id fun (_ : α) _ => isConj_iff_eq.1, Quotient.lift_mk _ _, by
    rw [Function.RightInverse, Function.LeftInverse, forall_isConj]
    intro x
    rw [← quotient_mk_eq_mk, ← quotient_mk_eq_mk, Quotient.lift_mk, id]⟩

Bijection between a commutative group and its conjugacy classes

Informal description

The bijection between a commutative group $\alpha$ and its conjugacy classes $\text{ConjClasses}(\alpha)$, mapping each element $a \in \alpha$ to its conjugacy class $\text{ConjClasses.mk}(a)$. The inverse map sends a conjugacy class back to any of its representatives.

conjugatesOf definition

(a : α) : Set α

Full source

/-- Given an element `a`, `conjugatesOf a` is the set of conjugates. -/
def conjugatesOf (a : α) : Set α :=
  { b | IsConj a b }

Set of conjugates of a group element

Informal description

Given an element $ a $ in a monoid $ \alpha $, the set $ \text{conjugatesOf}(a) $ consists of all elements $ b $ in $ \alpha $ that are conjugate to $ a $, i.e., there exists a unit $ c $ in $ \alpha $ such that $ c \cdot a \cdot c^{-1} = b $.

mem_conjugatesOf_self theorem

{a : α} : a ∈ conjugatesOf a

Full source

theorem mem_conjugatesOf_self {a : α} : a ∈ conjugatesOf a :=
  IsConj.refl _

Reflexivity of Conjugates: $a \in \text{conjugatesOf}(a)$

Informal description

For any element $a$ in a monoid $\alpha$, the element $a$ belongs to its own set of conjugates, i.e., $a \in \text{conjugatesOf}(a)$.

IsConj.conjugatesOf_eq theorem

{a b : α} (ab : IsConj a b) : conjugatesOf a = conjugatesOf b

Full source

theorem IsConj.conjugatesOf_eq {a b : α} (ab : IsConj a b) : conjugatesOf a = conjugatesOf b :=
  Set.ext fun _ => ⟨fun ag => ab.symm.trans ag, fun bg => ab.trans bg⟩

Conjugate Elements Have Equal Conjugate Sets

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, if $a$ is conjugate to $b$, then the set of conjugates of $a$ is equal to the set of conjugates of $b$, i.e., $\text{conjugatesOf}(a) = \text{conjugatesOf}(b)$.

isConj_iff_conjugatesOf_eq theorem

{a b : α} : IsConj a b ↔ conjugatesOf a = conjugatesOf b

Full source

theorem isConj_iff_conjugatesOf_eq {a b : α} : IsConjIsConj a b ↔ conjugatesOf a = conjugatesOf b :=
  ⟨IsConj.conjugatesOf_eq, fun h => by
    have ha := mem_conjugatesOf_self (a := b)
    rwa [← h] at ha⟩

Conjugacy Criterion via Conjugate Sets

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, $a$ is conjugate to $b$ if and only if the set of conjugates of $a$ is equal to the set of conjugates of $b$, i.e., $\text{IsConj}(a, b) \leftrightarrow \text{conjugatesOf}(a) = \text{conjugatesOf}(b)$.

ConjClasses.carrier definition

: ConjClasses α → Set α

Full source

/-- Given a conjugacy class `a`, `carrier a` is the set it represents. -/
def carrier : ConjClasses α → Set α :=
  Quotient.lift conjugatesOf fun (_ : α) _ ab => IsConj.conjugatesOf_eq ab

Set of conjugates in a conjugacy class

Informal description

Given a conjugacy class `a` in a monoid $\alpha$, the function maps `a` to the set of all elements in $\alpha$ that are conjugate to any representative of `a`. That is, if `a` is the conjugacy class of $x \in \alpha$, then $\text{carrier}(a) = \{ y \in \alpha \mid \exists g \in \alpha, y = g x g^{-1} \}$.

ConjClasses.mem_carrier_mk theorem

{a : α} : a ∈ carrier (ConjClasses.mk a)

Full source

theorem mem_carrier_mk {a : α} : a ∈ carrier (ConjClasses.mk a) :=
  IsConj.refl _

Element Belongs to Its Own Conjugacy Class

Informal description

For any element $a$ in a monoid $\alpha$, $a$ belongs to the set of conjugates of its own conjugacy class, i.e., $a \in \text{carrier}(\text{ConjClasses.mk}(a))$.

ConjClasses.mem_carrier_iff_mk_eq theorem

{a : α} {b : ConjClasses α} : a ∈ carrier b ↔ ConjClasses.mk a = b

Full source

theorem mem_carrier_iff_mk_eq {a : α} {b : ConjClasses α} :
    a ∈ carrier ba ∈ carrier b ↔ ConjClasses.mk a = b := by
  revert b
  rw [forall_isConj]
  intro b
  rw [carrier, eq_comm, mk_eq_mk_iff_isConj, ← quotient_mk_eq_mk, Quotient.lift_mk]
  rfl

Element in Conjugacy Class iff Class Equals Its Own

Informal description

For any element $a$ in a monoid $\alpha$ and any conjugacy class $b$ of $\alpha$, the element $a$ belongs to the set of conjugates of $b$ if and only if the conjugacy class of $a$ equals $b$. In other words: \[ a \in \text{carrier}(b) \leftrightarrow \text{ConjClasses.mk}(a) = b \]

ConjClasses.carrier_eq_preimage_mk theorem

{a : ConjClasses α} : a.carrier = ConjClasses.mk ⁻¹' { a }

Full source

theorem carrier_eq_preimage_mk {a : ConjClasses α} : a.carrier = ConjClasses.mkConjClasses.mk ⁻¹' {a} :=
  Set.ext fun _ => mem_carrier_iff_mk_eq

Conjugacy Class Carrier as Preimage of Singleton under Conjugacy Map

Informal description

For any conjugacy class $a$ in a monoid $\alpha$, the set of conjugates of $a$ is equal to the preimage of the singleton set $\{a\}$ under the conjugacy class map $\text{ConjClasses.mk} : \alpha \to \text{ConjClasses}(\alpha)$. In other words: \[ \text{carrier}(a) = \text{ConjClasses.mk}^{-1}(\{a\}) \]