Mathlib.GroupTheory.GroupAction.ConjAct

ConjAct definition

: Type _

Full source

/-- A type alias for a group `G`. `ConjAct G` acts on `G` by conjugation -/
def ConjAct : Type _ :=
  G

Conjugation action of a group on itself

Informal description

The type alias `ConjAct G` represents a group `G` equipped with the conjugation action of `G` on itself. That is, for any group `G`, the elements of `ConjAct G` act on `G` via conjugation: $ g \cdot h = g h g^{-1} $.

ConjAct.instGroup instance

[Group G] : Group (ConjAct G)

Full source

instance [Group G] : Group (ConjAct G) := ‹Group G›

Group Structure on Conjugation Action

Informal description

For any group $G$, the conjugation action $\text{ConjAct}\, G$ forms a group under the same operations as $G$.

ConjAct.instDivInvMonoid instance

[DivInvMonoid G] : DivInvMonoid (ConjAct G)

Full source

instance [DivInvMonoid G] : DivInvMonoid (ConjAct G) := ‹DivInvMonoid G›

Division and Inversion Monoid Structure on Conjugation Action

Informal description

For any group $G$ with a division and inversion operation, the conjugation action $\text{ConjAct}\, G$ inherits a division and inversion monoid structure from $G$.

ConjAct.instFintype instance

[Fintype G] : Fintype (ConjAct G)

Full source

instance [Fintype G] : Fintype (ConjAct G) := ‹Fintype G›

Finiteness of the Conjugation Action

Informal description

For any finite group $G$, the conjugation action $\text{ConjAct}\, G$ is also finite.

ConjAct.card theorem

[Fintype G] : Fintype.card (ConjAct G) = Fintype.card G

Full source

@[simp]
theorem card [Fintype G] : Fintype.card (ConjAct G) = Fintype.card G :=
  rfl

Cardinality of Conjugation Action Equals Cardinality of Group

Informal description

For any finite group $G$, the cardinality of the conjugation action $\text{ConjAct}\, G$ is equal to the cardinality of $G$.

ConjAct.instInhabited instance

: Inhabited (ConjAct G)

Full source

instance : Inhabited (ConjAct G) :=
  ⟨1⟩

Inhabitedness of the Conjugation Action

Informal description

For any group $G$, the conjugation action $\text{ConjAct}\, G$ is inhabited.

ConjAct.ofConjAct definition

: ConjAct G ≃* G

Full source

/-- Reinterpret `g : ConjAct G` as an element of `G`. -/
def ofConjAct : ConjActConjAct G ≃* G where
  toFun := id
  invFun := id
  left_inv := fun _ => rfl
  right_inv := fun _ => rfl
  map_mul' := fun _ _ => rfl

Conversion from conjugation action to group element

Informal description

The function maps an element $ g $ of the conjugation action type `ConjAct G` back to the corresponding element in the original group $ G $. This is a multiplicative equivalence (i.e., it preserves the group structure) between `ConjAct G` and $ G $, where both the forward and inverse maps are the identity function.

ConjAct.toConjAct definition

: G ≃* ConjAct G

Full source

/-- Reinterpret `g : G` as an element of `ConjAct G`. -/
def toConjAct : G ≃* ConjAct G :=
  ofConjAct.symm

Conversion from group element to conjugation action

Informal description

The function maps an element $ g $ of a group $ G $ to the corresponding element in the conjugation action type `ConjAct G`. This is a multiplicative equivalence (i.e., it preserves the group structure) between $ G $ and `ConjAct G`, where both the forward and inverse maps are the identity function.

ConjAct.rec definition

{C : ConjAct G → Sort*} (h : ∀ g, C (toConjAct g)) : ∀ g, C g

Full source

/-- A recursor for `ConjAct`, for use as `induction x` when `x : ConjAct G`. -/
@[elab_as_elim, cases_eliminator, induction_eliminator]
protected def rec {C : ConjAct G → Sort*} (h : ∀ g, C (toConjAct g)) : ∀ g, C g :=
  h

Recursor for conjugation action

Informal description

The recursion principle for `ConjAct G`, stating that to define a function on all elements of `ConjAct G`, it suffices to define it on elements of the form `toConjAct g` for `g : G`.

ConjAct.forall theorem

(p : ConjAct G → Prop) : (∀ x : ConjAct G, p x) ↔ ∀ x : G, p (toConjAct x)

Full source

@[simp]
theorem «forall» (p : ConjAct G → Prop) : (∀ x : ConjAct G, p x) ↔ ∀ x : G, p (toConjAct x) :=
  id Iff.rfl

Universal Quantification over Conjugation Action via Group Elements

Informal description

For any predicate $p$ on the conjugation action type $\text{ConjAct}\, G$, the statement that $p$ holds for all elements of $\text{ConjAct}\, G$ is equivalent to the statement that $p$ holds for all elements of $G$ under the canonical map $\text{toConjAct} : G \to \text{ConjAct}\, G$. In other words: \[ (\forall x \in \text{ConjAct}\, G, p(x)) \leftrightarrow (\forall x \in G, p(\text{toConjAct}(x))). \]

ConjAct.of_mul_symm_eq theorem

: (@ofConjAct G _).symm = toConjAct

Full source

@[simp]
theorem of_mul_symm_eq : (@ofConjAct G _).symm = toConjAct :=
  rfl

Inverse of Conjugation Action Conversion Equals Forward Conversion

Informal description

The inverse of the multiplicative equivalence `ofConjAct` from `ConjAct G` to $G$ is equal to the multiplicative equivalence `toConjAct` from $G$ to `ConjAct G`.

ConjAct.to_mul_symm_eq theorem

: (@toConjAct G _).symm = ofConjAct

Full source

@[simp]
theorem to_mul_symm_eq : (@toConjAct G _).symm = ofConjAct :=
  rfl

Inverse of Group-to-Conjugation-Action Equals Conjugation-Action-to-Group Map

Informal description

The inverse of the multiplicative equivalence `toConjAct` from a group $G$ to its conjugation action type `ConjAct G` is equal to the multiplicative equivalence `ofConjAct` from `ConjAct G` back to $G$.

ConjAct.toConjAct_ofConjAct theorem

(x : ConjAct G) : toConjAct (ofConjAct x) = x

Full source

@[simp]
theorem toConjAct_ofConjAct (x : ConjAct G) : toConjAct (ofConjAct x) = x :=
  rfl

Inverse Property of Conjugation Action Conversion: $\text{toConjAct} \circ \text{ofConjAct} = \text{id}$

Informal description

For any element $x$ in the conjugation action type $\text{ConjAct}\, G$, applying the conversion function $\text{toConjAct}$ to the result of $\text{ofConjAct}(x)$ yields $x$ itself, i.e., $\text{toConjAct}(\text{ofConjAct}(x)) = x$.

ConjAct.ofConjAct_toConjAct theorem

(x : G) : ofConjAct (toConjAct x) = x

Full source

@[simp]
theorem ofConjAct_toConjAct (x : G) : ofConjAct (toConjAct x) = x :=
  rfl

Inverse Property of Conjugation Action Conversion: $\text{ofConjAct} \circ \text{toConjAct} = \text{id}$

Informal description

For any element $x$ in a group $G$, applying the conjugation action conversion function $\text{ofConjAct}$ to the result of $\text{toConjAct}(x)$ yields $x$ itself, i.e., $\text{ofConjAct}(\text{toConjAct}(x)) = x$.

ConjAct.ofConjAct_one theorem

: ofConjAct (1 : ConjAct G) = 1

Full source

theorem ofConjAct_one : ofConjAct (1 : ConjAct G) = 1 :=
  rfl

Identity Preservation in Conjugation Action: $\text{ofConjAct}(1) = 1$

Informal description

The multiplicative identity element in the conjugation action type $\text{ConjAct}\, G$ corresponds to the multiplicative identity element in the original group $G$, i.e., $\text{ofConjAct}(1) = 1$.

ConjAct.toConjAct_one theorem

: toConjAct (1 : G) = 1

Full source

theorem toConjAct_one : toConjAct (1 : G) = 1 :=
  rfl

Identity Preservation under Conjugation Action: $\text{toConjAct}(1) = 1$

Informal description

The multiplicative identity element $1$ in a group $G$ is preserved under the conjugation action, i.e., $\text{toConjAct}(1) = 1$ in $\text{ConjAct}\, G$.

ConjAct.ofConjAct_inv theorem

(x : ConjAct G) : ofConjAct x⁻¹ = (ofConjAct x)⁻¹

Full source

@[simp]
theorem ofConjAct_inv (x : ConjAct G) : ofConjAct x⁻¹ = (ofConjAct x)⁻¹ :=
  rfl

Inverse Preservation in Conjugation Action: $\text{ofConjAct}(x^{-1}) = (\text{ofConjAct}\, x)^{-1}$

Informal description

For any element $x$ in the conjugation action type $\text{ConjAct}\, G$, the inverse of $x$ under the conjugation action corresponds to the inverse of $x$ in the original group $G$. That is, $\text{ofConjAct}(x^{-1}) = (\text{ofConjAct}\, x)^{-1}$.

ConjAct.toConjAct_inv theorem

(x : G) : toConjAct x⁻¹ = (toConjAct x)⁻¹

Full source

@[simp]
theorem toConjAct_inv (x : G) : toConjAct x⁻¹ = (toConjAct x)⁻¹ :=
  rfl

Inverse Preservation under Conjugation Action: $\text{toConjAct}(x^{-1}) = (\text{toConjAct}\, x)^{-1}$

Informal description

For any element $x$ in a group $G$, the conjugation action of the inverse $x^{-1}$ is equal to the inverse of the conjugation action of $x$, i.e., $\text{toConjAct}(x^{-1}) = (\text{toConjAct}\, x)^{-1}$.

ConjAct.ofConjAct_mul theorem

(x y : ConjAct G) : ofConjAct (x * y) = ofConjAct x * ofConjAct y

Full source

theorem ofConjAct_mul (x y : ConjAct G) : ofConjAct (x * y) = ofConjAct x * ofConjAct y :=
  rfl

Multiplicative Homomorphism Property of Conjugation Action: $\text{ofConjAct}(x \cdot y) = \text{ofConjAct}\, x \cdot \text{ofConjAct}\, y$

Informal description

For any elements $x$ and $y$ in the conjugation action type $\text{ConjAct}\, G$, the product $x \cdot y$ under the conjugation action corresponds to the product of $x$ and $y$ in the original group $G$. That is, $\text{ofConjAct}(x \cdot y) = \text{ofConjAct}\, x \cdot \text{ofConjAct}\, y$.

ConjAct.toConjAct_mul theorem

(x y : G) : toConjAct (x * y) = toConjAct x * toConjAct y

Full source

theorem toConjAct_mul (x y : G) : toConjAct (x * y) = toConjAct x * toConjAct y :=
  rfl

Multiplicative Homomorphism Property of Conjugation Action: $\text{toConjAct}(xy) = \text{toConjAct}(x)\text{toConjAct}(y)$

Informal description

For any elements $x$ and $y$ in a group $G$, the conjugation action of the product $x * y$ is equal to the product of the conjugation actions of $x$ and $y$, i.e., $\text{toConjAct}(x * y) = \text{toConjAct}(x) * \text{toConjAct}(y)$.

ConjAct.instSMul instance

: SMul (ConjAct G) G

Full source

instance : SMul (ConjAct G) G where smul g h := ofConjAct g * h * (ofConjAct g)⁻¹

Conjugation Action of a Group on Itself

Informal description

For any group $G$, the conjugation action $\text{ConjAct}\, G$ acts on $G$ via $g \cdot h = g h g^{-1}$ for $g \in \text{ConjAct}\, G$ and $h \in G$.

ConjAct.smul_def theorem

(g : ConjAct G) (h : G) : g • h = ofConjAct g * h * (ofConjAct g)⁻¹

Full source

theorem smul_def (g : ConjAct G) (h : G) : g • h = ofConjAct g * h * (ofConjAct g)⁻¹ :=
  rfl

Definition of Conjugation Action: $g \cdot h = g h g^{-1}$

Informal description

For any group $G$, the conjugation action of $g \in \text{ConjAct}\, G$ on $h \in G$ is given by $g \cdot h = g h g^{-1}$, where $g$ is identified with its corresponding element in $G$ via the map $\text{ofConjAct}$.

ConjAct.toConjAct_smul theorem

(g h : G) : toConjAct g • h = g * h * g⁻¹

Full source

theorem toConjAct_smul (g h : G) : toConjAct g • h = g * h * g⁻¹ :=
  rfl

Conjugation Action Formula: $\text{toConjAct}\, g \cdot h = g h g^{-1}$

Informal description

For any elements $g$ and $h$ in a group $G$, the conjugation action of $g$ (viewed as an element of $\text{ConjAct}\, G$) on $h$ is given by $g h g^{-1}$. That is, $\text{toConjAct}\, g \cdot h = g h g^{-1}$.

ConjAct.unitsScalar instance

: SMul (ConjAct Mˣ) M

Full source

instance unitsScalar : SMul (ConjAct Mˣ) M where smul g h := ofConjAct g * h * ↑(ofConjAct g)⁻¹

Conjugation Action of Units on a Monoid

Informal description

For any monoid $M$, the group of units $\text{ConjAct}\, M^\times$ acts on $M$ via conjugation: $g \cdot h = g h g^{-1}$ for $g \in M^\times$ and $h \in M$.

ConjAct.units_smul_def theorem

(g : ConjAct Mˣ) (h : M) : g • h = ofConjAct g * h * ↑(ofConjAct g)⁻¹

Full source

theorem units_smul_def (g : ConjAct Mˣ) (h : M) : g • h = ofConjAct g * h * ↑(ofConjAct g)⁻¹ :=
  rfl

Conjugation Action Formula for Units on a Monoid

Informal description

For any monoid $M$, let $g$ be an element of the conjugation action $\text{ConjAct}\, M^\times$ and $h$ an element of $M$. The action of $g$ on $h$ is given by conjugation: \[ g \cdot h = g h g^{-1}, \] where $g$ is interpreted as an element of $M^\times$ via the canonical map $\text{ofConjAct}$.

ConjAct.unitsMulDistribMulAction instance

: MulDistribMulAction (ConjAct Mˣ) M

Full source

instance unitsMulDistribMulAction : MulDistribMulAction (ConjAct Mˣ) M where
  one_smul := by simp [units_smul_def]
  mul_smul := by simp [units_smul_def, mul_assoc]
  smul_mul := by simp [units_smul_def, mul_assoc]
  smul_one := by simp [units_smul_def]

Conjugation Action Preserves Monoid Multiplication

Informal description

For any monoid $M$, the conjugation action of the group of units $\text{ConjAct}\, M^\times$ on $M$ preserves the monoid structure. That is, for any $g \in \text{ConjAct}\, M^\times$ and $h_1, h_2 \in M$, we have: \[ g \cdot (h_1 h_2) = (g \cdot h_1)(g \cdot h_2). \]

ConjAct.unitsSMulCommClass instance

[SMul α M] [SMulCommClass α M M] [IsScalarTower α M M] : SMulCommClass α (ConjAct Mˣ) M

Full source

instance unitsSMulCommClass [SMul α M] [SMulCommClass α M M] [IsScalarTower α M M] :
    SMulCommClass α (ConjAct Mˣ) M where
  smul_comm a um m := by rw [units_smul_def, units_smul_def, mul_smul_comm, smul_mul_assoc]

Commutativity of Scalar Multiplication with Conjugation Action

Informal description

For any monoid $M$ with a scalar multiplication action $\alpha$ on $M$ that commutes with the multiplication in $M$ and satisfies the scalar tower condition, the scalar multiplication action $\alpha$ on $M$ also commutes with the conjugation action of the group of units $\text{ConjAct}\, M^\times$ on $M$.

ConjAct.unitsSMulCommClass' instance

[SMul α M] [SMulCommClass M α M] [IsScalarTower α M M] : SMulCommClass (ConjAct Mˣ) α M

Full source

instance unitsSMulCommClass' [SMul α M] [SMulCommClass M α M] [IsScalarTower α M M] :
    SMulCommClass (ConjAct Mˣ) α M :=
  haveI : SMulCommClass α M M := SMulCommClass.symm _ _ _
  SMulCommClass.symm _ _ _

Commutation of Conjugation and Scalar Actions on a Monoid

Informal description

For any monoid $M$ with a scalar multiplication action $\alpha$ on $M$ that commutes with the right multiplication in $M$ and satisfies the scalar tower condition, the conjugation action of the group of units $\text{ConjAct}\, M^\times$ on $M$ commutes with the scalar multiplication action $\alpha$ on $M$.

ConjAct.instMulDistribMulAction instance

: MulDistribMulAction (ConjAct G) G

Full source

instance : MulDistribMulAction (ConjAct G) G where
  smul_mul := by simp [smul_def]
  smul_one := by simp [smul_def]
  one_smul := by simp [smul_def]
  mul_smul := by simp [smul_def, mul_assoc]

Multiplicative Distributive Action via Conjugation

Informal description

For any group $G$, the conjugation action $\text{ConjAct}\, G$ acts on $G$ as a multiplicative distributive action, where the action is given by $g \cdot h = g h g^{-1}$ for $g \in \text{ConjAct}\, G$ and $h \in G$.

ConjAct.smulCommClass instance

[SMul α G] [SMulCommClass α G G] [IsScalarTower α G G] : SMulCommClass α (ConjAct G) G

Full source

instance smulCommClass [SMul α G] [SMulCommClass α G G] [IsScalarTower α G G] :
    SMulCommClass α (ConjAct G) G where
  smul_comm a ug g := by rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]

Commutation of Scalar and Conjugation Actions on a Group

Informal description

For any group $G$ and any type $\alpha$ with a scalar multiplication action on $G$ that commutes with the group multiplication and forms a scalar tower, the actions of $\alpha$ and the conjugation action $\text{ConjAct}\, G$ on $G$ commute. That is, for all $a \in \alpha$, $g \in \text{ConjAct}\, G$, and $h \in G$, we have $a \cdot (g \cdot h) = g \cdot (a \cdot h)$.

ConjAct.smulCommClass' instance

[SMul α G] [SMulCommClass G α G] [IsScalarTower α G G] : SMulCommClass (ConjAct G) α G

Full source

instance smulCommClass' [SMul α G] [SMulCommClass G α G] [IsScalarTower α G G] :
    SMulCommClass (ConjAct G) α G :=
  haveI := SMulCommClass.symm G α G
  SMulCommClass.symm _ _ _

Commutation of Conjugation and Scalar Actions on a Group

Informal description

For any group $G$ and any type $\alpha$ with a scalar multiplication action on $G$ that commutes with the group multiplication and forms a scalar tower, the actions of the conjugation action $\text{ConjAct}\, G$ and $\alpha$ on $G$ commute. That is, for all $g \in \text{ConjAct}\, G$, $a \in \alpha$, and $h \in G$, we have $g \cdot (a \cdot h) = a \cdot (g \cdot h)$.

ConjAct.smul_eq_mulAut_conj theorem

(g : ConjAct G) (h : G) : g • h = MulAut.conj (ofConjAct g) h

Full source

theorem smul_eq_mulAut_conj (g : ConjAct G) (h : G) : g • h = MulAut.conj (ofConjAct g) h :=
  rfl

Conjugation Action Equals Inner Automorphism Action

Informal description

For any group $G$, the conjugation action of $g \in \text{ConjAct}\, G$ on $h \in G$ is given by $g \cdot h = \text{conj}(g) h$, where $\text{conj}(g)$ denotes the inner automorphism of $G$ induced by $g$.

ConjAct.fixedPoints_eq_center theorem

: fixedPoints (ConjAct G) G = center G

Full source

/-- The set of fixed points of the conjugation action of `G` on itself is the center of `G`. -/
theorem fixedPoints_eq_center : fixedPoints (ConjAct G) G = center G := by
  ext x
  simp [mem_center_iff, smul_def, mul_inv_eq_iff_eq_mul]

Fixed Points of Conjugation Action Equal the Center of the Group

Informal description

The set of fixed points of the conjugation action of a group $G$ on itself is equal to the center of $G$, i.e., \[ \{ h \in G \mid g h g^{-1} = h \text{ for all } g \in G \} = Z(G). \]

ConjAct.mem_orbit_conjAct theorem

{g h : G} : g ∈ orbit (ConjAct G) h ↔ IsConj g h

Full source

@[simp]
theorem mem_orbit_conjAct {g h : G} : g ∈ orbit (ConjAct G) hg ∈ orbit (ConjAct G) h ↔ IsConj g h := by
  rw [isConj_comm, isConj_iff, mem_orbit_iff]; rfl

Characterization of Orbit Membership via Conjugacy in a Group

Informal description

For any elements $g$ and $h$ in a group $G$, the element $g$ belongs to the orbit of $h$ under the conjugation action of $G$ on itself if and only if $g$ and $h$ are conjugate in $G$, i.e., there exists an element $x \in G$ such that $g = x h x^{-1}$.

ConjAct.orbitRel_conjAct theorem

: ⇑(orbitRel (ConjAct G) G) = IsConj

Full source

theorem orbitRel_conjAct : ⇑(orbitRel (ConjAct G) G) = IsConj :=
  funext₂ fun g h => by rw [orbitRel_apply, mem_orbit_conjAct]

Orbit Relation of Conjugation Action Equals Conjugacy Relation

Informal description

The orbit equivalence relation induced by the conjugation action of a group $G$ on itself coincides with the conjugacy relation $\text{IsConj}$. That is, for any elements $g, h \in G$, we have $g \sim h$ under the orbit relation if and only if $g$ and $h$ are conjugate in $G$.

ConjAct.orbit_eq_carrier_conjClasses theorem

(g : G) : orbit (ConjAct G) g = (ConjClasses.mk g).carrier

Full source

theorem orbit_eq_carrier_conjClasses (g : G) :
    orbit (ConjAct G) g = (ConjClasses.mk g).carrier := by
  ext h
  rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct]

Orbit under Conjugation Equals Conjugacy Class Carrier

Informal description

For any element $g$ in a group $G$, the orbit of $g$ under the conjugation action of $G$ on itself is equal to the carrier set of the conjugacy class of $g$. That is, the set $\{hgh^{-1} \mid h \in G\}$ is precisely the set of elements conjugate to $g$ in $G$.

ConjAct.stabilizer_eq_centralizer theorem

(g : G) : stabilizer (ConjAct G) g = centralizer (zpowers (toConjAct g) : Set (ConjAct G))

Full source

theorem stabilizer_eq_centralizer (g : G) :
    stabilizer (ConjAct G) g = centralizer (zpowers (toConjAct g) : Set (ConjAct G)) :=
  le_antisymm (le_centralizer_iff.mp (zpowers_le.mpr fun _ => mul_inv_eq_iff_eq_mul.mp)) fun _ h =>
    mul_inv_eq_of_eq_mul (h g (mem_zpowers g)).symm

Stabilizer under Conjugation Equals Centralizer of Cyclic Subgroup

Informal description

For any element $g$ in a group $G$, the stabilizer subgroup of $g$ under the conjugation action of $\text{ConjAct}\, G$ is equal to the centralizer of the cyclic subgroup generated by $g$ in $\text{ConjAct}\, G$. That is, the set of elements in $\text{ConjAct}\, G$ that fix $g$ under conjugation is precisely the set of elements that commute with all powers of $g$.

Subgroup.centralizer_eq_comap_stabilizer theorem

 (g : G) :
  Subgroup.centralizer { g } = Subgroup.comap ConjAct.toConjAct.toMonoidHom (MulAction.stabilizer (ConjAct G) g)

Full source

theorem _root_.Subgroup.centralizer_eq_comap_stabilizer (g : G) :
    Subgroup.centralizer {g} = Subgroup.comap ConjAct.toConjAct.toMonoidHom
      (MulAction.stabilizer (ConjAct G) g) := by
  ext k
-- NOTE: `Subgroup.mem_centralizer_iff` should probably be stated
-- with the equality in the other direction
  simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq, ConjAct.toConjAct_smul]
  rw [eq_comm]
  exact Iff.symm mul_inv_eq_iff_eq_mul

Centralizer as Preimage of Stabilizer under Conjugation Action

Informal description

For any element $g$ in a group $G$, the centralizer of the singleton set $\{g\}$ in $G$ is equal to the preimage under the conjugation action homomorphism of the stabilizer subgroup of $g$ in $\text{ConjAct}\, G$. That is, \[ \text{centralizer}(\{g\}) = \text{comap}(\text{ConjAct.toConjAct}) (\text{stabilizer}(\text{ConjAct}\, G, g)). \]

ConjAct.Subgroup.conjAction instance

{H : Subgroup G} [hH : H.Normal] : SMul (ConjAct G) H

Full source

/-- As normal subgroups are closed under conjugation, they inherit the conjugation action
  of the underlying group. -/
instance Subgroup.conjAction {H : Subgroup G} [hH : H.Normal] : SMul (ConjAct G) H :=
  ⟨fun g h => ⟨g • (h : G), hH.conj_mem h.1 h.2 (ofConjAct g)⟩⟩

Conjugation Action on Normal Subgroups

Informal description

For any normal subgroup $H$ of a group $G$, the conjugation action of $G$ on itself restricts to an action on $H$. That is, for any $g \in G$ and $h \in H$, the conjugate $g \cdot h = g h g^{-1}$ is also in $H$.

ConjAct.Subgroup.val_conj_smul theorem

{H : Subgroup G} [H.Normal] (g : ConjAct G) (h : H) : ↑(g • h) = g • (h : G)

Full source

theorem Subgroup.val_conj_smul {H : Subgroup G} [H.Normal] (g : ConjAct G) (h : H) :
    ↑(g • h) = g • (h : G) :=
  rfl

Compatibility of Conjugation Action with Subgroup Inclusion

Informal description

Let $G$ be a group and $H$ a normal subgroup of $G$. For any $g \in \text{ConjAct}\, G$ and $h \in H$, the conjugation action satisfies $\overline{g \cdot h} = g \cdot \overline{h}$, where $\overline{\cdot}$ denotes the inclusion map from $H$ to $G$.

ConjAct.Subgroup.conjMulDistribMulAction instance

{H : Subgroup G} [H.Normal] : MulDistribMulAction (ConjAct G) H

Full source

instance Subgroup.conjMulDistribMulAction {H : Subgroup G} [H.Normal] :
    MulDistribMulAction (ConjAct G) H :=
  Subtype.coe_injective.mulDistribMulAction H.subtype Subgroup.val_conj_smul

Multiplicative Distributive Conjugation Action on Normal Subgroups

Informal description

For any normal subgroup $H$ of a group $G$, the conjugation action of $G$ on itself induces a multiplicative distributive action on $H$, where the action is given by $g \cdot h = g h g^{-1}$ for $g \in G$ and $h \in H$.

MulAut.conjNormal definition

{H : Subgroup G} [H.Normal] : G →* MulAut H

Full source

/-- Group conjugation on a normal subgroup. Analogous to `MulAut.conj`. -/
def _root_.MulAut.conjNormal {H : Subgroup G} [H.Normal] : G →* MulAut H :=
  (MulDistribMulAction.toMulAut (ConjAct G) H).comp toConjAct.toMonoidHom

Conjugation automorphism of a normal subgroup

Informal description

The function maps an element $ g $ of a group $ G $ to the automorphism of a normal subgroup $ H $ of $ G $ given by conjugation by $ g $. That is, for any $ h \in H $, the automorphism sends $ h $ to $ g h g^{-1} $.

MulAut.conjNormal_apply theorem

{H : Subgroup G} [H.Normal] (g : G) (h : H) : ↑(MulAut.conjNormal g h) = g * h * g⁻¹

Full source

@[simp]
theorem _root_.MulAut.conjNormal_apply {H : Subgroup G} [H.Normal] (g : G) (h : H) :
    ↑(MulAut.conjNormal g h) = g * h * g⁻¹ :=
  rfl

Conjugation Action Formula for Normal Subgroups: $g \cdot h \cdot g^{-1} = \text{conjNormal}(g)(h)$

Informal description

For any normal subgroup $H$ of a group $G$, given an element $g \in G$ and $h \in H$, the conjugation action of $g$ on $h$ satisfies $g \cdot h \cdot g^{-1} \in H$, and moreover, the image of $h$ under the conjugation automorphism $\text{conjNormal}(g)$ equals $g h g^{-1}$.

MulAut.conjNormal_symm_apply theorem

{H : Subgroup G} [H.Normal] (g : G) (h : H) : ↑((MulAut.conjNormal g).symm h) = g⁻¹ * h * g

Full source

@[simp]
theorem _root_.MulAut.conjNormal_symm_apply {H : Subgroup G} [H.Normal] (g : G) (h : H) :
    ↑((MulAut.conjNormal g).symm h) = g⁻¹ * h * g := by
  change _ * _⁻¹_⁻¹⁻¹ = _
  rw [inv_inv]
  rfl

Inverse Conjugation Automorphism Formula for Normal Subgroups

Informal description

For any normal subgroup $H$ of a group $G$, the inverse of the conjugation automorphism $\text{conjNormal}\, g$ applied to an element $h \in H$ satisfies $(\text{conjNormal}\, g)^{-1}(h) = g^{-1} h g$.

MulAut.conjNormal_inv_apply theorem

{H : Subgroup G} [H.Normal] (g : G) (h : H) : ↑((MulAut.conjNormal g)⁻¹ h) = g⁻¹ * h * g

Full source

@[simp]
theorem _root_.MulAut.conjNormal_inv_apply {H : Subgroup G} [H.Normal] (g : G) (h : H) :
    ↑((MulAut.conjNormal g)⁻¹ h) = g⁻¹ * h * g :=
  MulAut.conjNormal_symm_apply g h

Inverse Conjugation Formula for Normal Subgroups: $(\text{conjNormal}(g))^{-1}(h) = g^{-1} h g$

Informal description

For any normal subgroup $H$ of a group $G$, given an element $g \in G$ and $h \in H$, the inverse of the conjugation automorphism $\text{conjNormal}(g)$ applied to $h$ satisfies $(\text{conjNormal}(g))^{-1}(h) = g^{-1} h g$.

MulAut.conjNormal_val theorem

{H : Subgroup G} [H.Normal] {h : H} : MulAut.conjNormal ↑h = MulAut.conj h

Full source

theorem _root_.MulAut.conjNormal_val {H : Subgroup G} [H.Normal] {h : H} :
    MulAut.conjNormal ↑h = MulAut.conj h :=
  MulEquiv.ext fun _ => rfl

Equality of Conjugation Automorphism and Inner Automorphism for Normal Subgroup Elements

Informal description

For any normal subgroup $H$ of a group $G$ and any element $h \in H$, the conjugation automorphism of $H$ induced by $h$ (viewed as an element of $G$) is equal to the inner automorphism of $G$ induced by $h$. In other words, $\text{conjNormal}(h) = \text{conj}(h)$.

ConjAct.normal_of_characteristic_of_normal instance

{H : Subgroup G} [hH : H.Normal] {K : Subgroup H} [h : K.Characteristic] : (K.map H.subtype).Normal

Full source

instance normal_of_characteristic_of_normal {H : Subgroup G} [hH : H.Normal] {K : Subgroup H}
    [h : K.Characteristic] : (K.map H.subtype).Normal :=
  ⟨fun a ha b => by
    obtain ⟨a, ha, rfl⟩ := ha
    exact K.apply_coe_mem_map H.subtype
      ⟨_, (SetLike.ext_iff.mp (h.fixed (MulAut.conjNormal b)) a).mpr ha⟩⟩

Normality of Characteristic Subgroups in Normal Subgroups

Informal description

For any normal subgroup $H$ of a group $G$ and any characteristic subgroup $K$ of $H$, the image of $K$ under the inclusion map $H \hookrightarrow G$ is a normal subgroup of $G$.

unitsCentralizerEquiv definition

(x : Mˣ) : (Submonoid.centralizer ({↑x} : Set M))ˣ ≃* MulAction.stabilizer (ConjAct Mˣ) x

Full source

/-- The stabilizer of `Mˣ` acting on itself by conjugation at `x : Mˣ` is exactly the
units of the centralizer of `x : M`. -/
@[simps! apply_coe_val symm_apply_val_coe]
def unitsCentralizerEquiv (x : Mˣ) :
    (Submonoid.centralizer ({↑x} : Set M))ˣ(Submonoid.centralizer ({↑x} : Set M))ˣ ≃* MulAction.stabilizer (ConjAct Mˣ) x :=
  MulEquiv.symm
  { toFun := MonoidHom.toHomUnits <|
      { toFun := fun u ↦ ⟨↑(ConjAct.ofConjAct u.1 : Mˣ), by
          rintro x ⟨rfl⟩
          have : (u : ConjAct Mˣ) • x = x := u.2
          rwa [ConjAct.smul_def, mul_inv_eq_iff_eq_mul, Units.ext_iff, eq_comm] at this⟩,
        map_one' := rfl,
        map_mul' := fun _ _ ↦ rfl }
    invFun := fun u ↦
      ⟨ConjAct.toConjAct (Units.map (Submonoid.centralizer ({↑x} : Set M)).subtype u), by
      change _ • _ = _
      simp only [ConjAct.smul_def, ConjAct.ofConjAct_toConjAct, mul_inv_eq_iff_eq_mul]
      exact Units.ext <| (u.1.2 x <| Set.mem_singleton _).symm⟩
    left_inv := fun _ ↦ by ext; rfl
    right_inv := fun _ ↦ by ext; rfl
    map_mul' := map_mul _ }

Equivalence between centralizer units and conjugation stabilizer

Informal description

For any unit $ x $ in a monoid $ M $, there is a multiplicative equivalence between the units of the centralizer of $ x $ in $ M $ and the stabilizer subgroup of $ x $ under the conjugation action of the units of $ M $. More precisely, the stabilizer subgroup consists of all units $ u \in M^\times $ such that $ u x u^{-1} = x $, while the centralizer consists of all elements $ m \in M $ that commute with $ x $. The equivalence maps a unit $ u $ in the centralizer to the conjugation action $ u \cdot (-) = u (-) u^{-1} $ and vice versa.

Mathlib.GroupTheory.GroupAction.ConjAct

Main definitions

Implementation Notes