Simple(?) questions on group conjugations

Stream: new members

[Steven Herbert]

I am struggling with three simple questions on group conjugations.

1. have h2f : j * g * j⁻¹ ∈ conjugatesOf g := by (j, g are both in the same group) this is the definitive property of being a conjugate, but I'm a little stumped when poring through the documentation
2. I have hjh : ∀ (g_1 : G), g_1 * g = g * g_1 with goal ⊢ conjugatesOf g = {g}again feels like its pretty much true by definition, but I cannot seem to unpick how to close it.
3. Finally, I have hg : g ∈ conjugatesOf g with goal ⊢ ∃ a, g ∈ a.carrier. Basically I need to convert between the definition of conjugates and carrier, which is confusing me a little.

Any help much appreciated!

[Kevin Buzzard]

Can you rewrite your question as a #mwe in triple backticks with self-contained code (all imports etc) so that people are just one click away from being able to help you solve your problems, rather than several people all having to write the boilerplate themselves? You can then re-ask the questions as explicit sorrys in the code.

[Steven Herbert]

import Mathlib

open Finset
open Classical

namespace ConjClasses

variable (G : Type) [Group G] (g h j : G)
variable [Fintype G]
--Q1
example : j * g * j⁻¹ ∈ conjugatesOf g := by sorry
--Q2
example (h1 : ∀ (g_1 : G), g_1 * g  = g * g_1) : conjugatesOf g = {g} := by sorry
--Q3 (see below)
example [Fintype G] [Group G] : Fintype.card G = ∑ C : ConjClasses G, Fintype.card C.carrier := by
  have h : (Finset.univ : Finset G) =
      (Finset.univ : Finset (ConjClasses G)).biUnion (fun C ↦ C.carrier.toFinset) := by
    ext g
    simp only [Finset.mem_univ, Finset.mem_biUnion, Set.mem_toFinset, true_and, true_iff]
    have hg'' : g ∈ conjugatesOf g := by exact mem_conjugatesOf_self
    --its the goal at this point here that I'm struggling with
    sorry
  sorry -- don't worry about this sorry

[Aaron Liu]

import Mathlib

open Finset
open Classical

namespace ConjClasses

variable (G : Type) [Group G] (g h j : G)
-- variable [Fintype G]

--Q1
example : j * g * j⁻¹ ∈ conjugatesOf g := by
  have h : IsConj g (j * g * j⁻¹) := by simp
  rw [isConj_iff_conjugatesOf_eq.mp h]
  apply mem_conjugatesOf_self

--Q2
example (h1 : ∀ (g_1 : G), g_1 * g  = g * g_1) : conjugatesOf g = {g} := by
  have h : g ∈ Set.center G := Semigroup.mem_center_iff.mpr h1
  apply Set.eq_singleton_iff_unique_mem.mpr
  constructor
  · apply mem_conjugatesOf_self
  · intro x hx
    exact (hx.eq_of_left_mem_center h).symm

--Q3 (see below)
example [Fintype G] : Fintype.card G = ∑ C : ConjClasses G, Fintype.card C.carrier := by
  have h : (Finset.univ : Finset G) =
      (Finset.univ : Finset (ConjClasses G)).biUnion (fun C ↦ C.carrier.toFinset) := by
    ext g
    simp only [Finset.mem_univ, Finset.mem_biUnion, Set.mem_toFinset, true_and, true_iff]
    have hg'' : g ∈ conjugatesOf g := by exact mem_conjugatesOf_self
    --its the goal at this point here that I'm struggling with
    use ConjClasses.mk g
    exact hg''
  sorry -- don't worry about this sorry

[Steven Herbert]

That's terrific, thanks so much

[Kevin Buzzard]

@Steven Herbert for Q1 I'm a little surprised that mathlib has this definition conjugatesOf but not a lemma mem_conjugatesOf. You should PR it to mathlib! Using it, Q1 is easy:

import Mathlib

namespace ConjClasses

lemma mem_conjugatesOf {M : Type*} [Monoid M] (a b : M) : b ∈ conjugatesOf a ↔ IsConj a b := by
  -- this is the definition of `conjugatesOf`
  rfl

variable (G : Type) [Group G] (g j : G)
--Q1
example : j * g * j⁻¹ ∈ conjugatesOf g := by
  -- missing API
  rw [mem_conjugatesOf]
  -- but this is there
  rw [isConj_iff]
  -- ⊢ ∃ c, c * g * c⁻¹ = j * g * j⁻¹
  -- and now it's easy
  use j
  -- done