feat(group_theory): simple lemmas for Wedderburn (#18862)

ericrbg · ericrbg · commit d30d31261cdb · 2023-06-22T12:28:45.000Z
These lemmas are a bit disparate, but they are all useful for Wedderburn's little theorem.



Co-authored-by: Eric Rodriguez &lt;37984851+ericrbg@users.noreply.github.com&gt;
diff --git a/src/group_theory/group_action/basic.lean b/src/group_theory/group_action/basic.lean
@@ -192,6 +192,9 @@ local attribute [instance] orbit_rel
 
 variables {α} {β}
 
+@[to_additive]
+lemma orbit_rel_apply {x y : β} : (orbit_rel α β).rel x y ↔ x ∈ orbit α y := iff.rfl
+
 /-- When you take a set `U` in `β`, push it down to the quotient, and pull back, you get the union
 of the orbit of `U` under `α`. -/
 @[to_additive "When you take a set `U` in `β`, push it down to the quotient, and pull back, you get
diff --git a/src/group_theory/group_action/conj_act.lean b/src/group_theory/group_action/conj_act.lean
@@ -187,6 +187,12 @@ begin
   simp [mem_center_iff, smul_def, mul_inv_eq_iff_eq_mul]
 end
 
+@[simp] lemma mem_orbit_conj_act {g h : G} : g ∈ orbit (conj_act G) h ↔ is_conj g h :=
+by { rw [is_conj_comm, is_conj_iff, mem_orbit_iff], refl }
+
+lemma orbit_rel_conj_act : (orbit_rel (conj_act G) G).rel = is_conj :=
+funext₂ $ λ g h, by rw [orbit_rel_apply, mem_orbit_conj_act]
+
 lemma stabilizer_eq_centralizer (g : G) : stabilizer (conj_act G) g = (zpowers g).centralizer :=
 le_antisymm (le_centralizer_iff.mp (zpowers_le.mpr (λ x, mul_inv_eq_iff_eq_mul.mp)))
   (λ x h, mul_inv_eq_of_eq_mul (h g (mem_zpowers g)).symm)
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
@@ -2676,6 +2676,16 @@ begin
   exact subset_normal_closure (set.mem_singleton _),
 end
 
+variables {M : Type*} [monoid M]
+
+lemma eq_of_left_mem_center {g h : M} (H : is_conj g h) (Hg : g ∈ set.center M) :
+  g = h :=
+by { rcases H with ⟨u, hu⟩, rwa [← u.mul_left_inj, ← Hg u], }
+
+lemma eq_of_right_mem_center {g h : M} (H : is_conj g h) (Hh : h ∈ set.center M) :
+  g = h :=
+(H.symm.eq_of_left_mem_center Hh).symm
+
 end is_conj
 
 assert_not_exists multiset
