From dd239aab74b4a4e91235ee28418cf21a8a1b7439 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 15 Jan 2025 05:29:40 +0000 Subject: [PATCH] GroupTheory.GroupAction.Quotient no field --- Mathlib/GroupTheory/Commutator/Basic.lean | 34 +++++++++++++++++++ Mathlib/GroupTheory/GroupAction/Quotient.lean | 33 ++---------------- 2 files changed, 36 insertions(+), 31 deletions(-) diff --git a/Mathlib/GroupTheory/Commutator/Basic.lean b/Mathlib/GroupTheory/Commutator/Basic.lean index 38ed41f97f06e4..3e9b2f49f4583d 100644 --- a/Mathlib/GroupTheory/Commutator/Basic.lean +++ b/Mathlib/GroupTheory/Commutator/Basic.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Jordan Brown, Thomas Browning, Patrick Lutz. All rights reser Released under Apache 2.0 license as described in the file LICENSE. Authors: Jordan Brown, Thomas Browning, Patrick Lutz -/ +import Mathlib.GroupTheory.GroupAction.Quotient import Mathlib.GroupTheory.Subgroup.Centralizer import Mathlib.Tactic.Group @@ -210,3 +211,36 @@ theorem mem_commutatorSet_iff : g ∈ commutatorSet G ↔ ∃ g₁ g₂ : G, ⁅ theorem commutator_mem_commutatorSet : ⁅g₁, g₂⁆ ∈ commutatorSet G := ⟨g₁, g₂, rfl⟩ + +namespace Subgroup + +open QuotientGroup + +/-- Cosets of the centralizer of an element embed into the set of commutators. -/ +noncomputable def quotientCentralizerEmbedding (g : G) : + G ⧸ centralizer (zpowers (g : G)) ↪ commutatorSet G := + ((MulAction.orbitEquivQuotientStabilizer (ConjAct G) g).trans + (quotientEquivOfEq (ConjAct.stabilizer_eq_centralizer g))).symm.toEmbedding.trans + ⟨fun x => + ⟨x * g⁻¹, + let ⟨_, x, rfl⟩ := x + ⟨x, g, rfl⟩⟩, + fun _ _ => Subtype.ext ∘ mul_right_cancel ∘ Subtype.ext_iff.mp⟩ + +theorem quotientCentralizerEmbedding_apply (g : G) (x : G) : + quotientCentralizerEmbedding g x = ⟨⁅x, g⁆, x, g, rfl⟩ := + rfl + +/-- If `G` is generated by `S`, then the quotient by the center embeds into `S`-indexed sequences +of commutators. -/ +noncomputable def quotientCenterEmbedding {S : Set G} (hS : closure S = ⊤) : + G ⧸ center G ↪ S → commutatorSet G := + (quotientEquivOfEq (center_eq_infi' S hS)).toEmbedding.trans + ((quotientiInfEmbedding _).trans + (Function.Embedding.piCongrRight fun g => quotientCentralizerEmbedding (g : G))) + +theorem quotientCenterEmbedding_apply {S : Set G} (hS : closure S = ⊤) (g : G) (s : S) : + quotientCenterEmbedding hS g s = ⟨⁅g, s⁆, g, s, rfl⟩ := + rfl + +end Subgroup diff --git a/Mathlib/GroupTheory/GroupAction/Quotient.lean b/Mathlib/GroupTheory/GroupAction/Quotient.lean index 22f50e36d4ce8b..4b1b36c7257365 100644 --- a/Mathlib/GroupTheory/GroupAction/Quotient.lean +++ b/Mathlib/GroupTheory/GroupAction/Quotient.lean @@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes, Thomas Browning -/ import Mathlib.Algebra.Group.Subgroup.Actions -import Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas import Mathlib.Data.Fintype.BigOperators import Mathlib.Dynamics.PeriodicPts.Lemmas -import Mathlib.GroupTheory.Commutator.Basic import Mathlib.GroupTheory.Coset.Basic import Mathlib.GroupTheory.GroupAction.Basic import Mathlib.GroupTheory.GroupAction.ConjAct @@ -24,6 +22,8 @@ This file proves properties of group actions which use the quotient group constr as well as their analogues for additive groups. -/ +assert_not_exists Field + universe u v w variable {α : Type u} {β : Type v} {γ : Type w} @@ -483,33 +483,4 @@ theorem normalCore_eq_ker : H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g] exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G)) -open QuotientGroup - -/-- Cosets of the centralizer of an element embed into the set of commutators. -/ -noncomputable def quotientCentralizerEmbedding (g : G) : - G ⧸ centralizer (zpowers (g : G)) ↪ commutatorSet G := - ((MulAction.orbitEquivQuotientStabilizer (ConjAct G) g).trans - (quotientEquivOfEq (ConjAct.stabilizer_eq_centralizer g))).symm.toEmbedding.trans - ⟨fun x => - ⟨x * g⁻¹, - let ⟨_, x, rfl⟩ := x - ⟨x, g, rfl⟩⟩, - fun _ _ => Subtype.ext ∘ mul_right_cancel ∘ Subtype.ext_iff.mp⟩ - -theorem quotientCentralizerEmbedding_apply (g : G) (x : G) : - quotientCentralizerEmbedding g x = ⟨⁅x, g⁆, x, g, rfl⟩ := - rfl - -/-- If `G` is generated by `S`, then the quotient by the center embeds into `S`-indexed sequences -of commutators. -/ -noncomputable def quotientCenterEmbedding {S : Set G} (hS : closure S = ⊤) : - G ⧸ center G ↪ S → commutatorSet G := - (quotientEquivOfEq (center_eq_infi' S hS)).toEmbedding.trans - ((quotientiInfEmbedding _).trans - (Function.Embedding.piCongrRight fun g => quotientCentralizerEmbedding (g : G))) - -theorem quotientCenterEmbedding_apply {S : Set G} (hS : closure S = ⊤) (g : G) (s : S) : - quotientCenterEmbedding hS g s = ⟨⁅g, s⁆, g, s, rfl⟩ := - rfl - end Subgroup