doc-next-gen

Mathlib.GroupTheory.Subgroup.Centralizer

Module docstring

{"# Centralizers of subgroups "}

Subgroup.centralizer definition
(s : Set G) : Subgroup G
Full source 
/-- The `centralizer` of `s` is the subgroup of `g : G` commuting with every `h : s`. -/
@[to_additive
      "The `centralizer` of `s` is the additive subgroup of `g : G` commuting with every `h : s`."]
def centralizer (s : Set G) : Subgroup G :=
  { Submonoid.centralizer s with
    carrier := Set.centralizer s
    inv_mem' := Set.inv_mem_centralizer }
Centralizer of a subset in a group
Informal description
The centralizer of a subset \( s \) of a group \( G \) is the subgroup consisting of all elements \( g \in G \) that commute with every element \( h \in s \), i.e., \( h * g = g * h \) for all \( h \in s \).
Subgroup.mem_centralizer_iff theorem
{g : G} {s : Set G} : g ∈ centralizer s ↔ ∀ h ∈ s, h * g = g * h
Full source 
@[to_additive]
theorem mem_centralizer_iff {g : G} {s : Set G} : g ∈ centralizer sg ∈ centralizer s ↔ ∀ h ∈ s, h * g = g * h :=
  Iff.rfl
Characterization of Centralizer Membership via Commutation
Informal description
For any element $g$ in a group $G$ and any subset $s$ of $G$, $g$ belongs to the centralizer of $s$ if and only if $g$ commutes with every element $h$ in $s$, i.e., $h * g = g * h$ for all $h \in s$.
Subgroup.mem_centralizer_iff_commutator_eq_one theorem
{g : G} {s : Set G} : g ∈ centralizer s ↔ ∀ h ∈ s, h * g * h⁻¹ * g⁻¹ = 1
Full source 
@[to_additive]
theorem mem_centralizer_iff_commutator_eq_one {g : G} {s : Set G} :
    g ∈ centralizer sg ∈ centralizer s ↔ ∀ h ∈ s, h * g * h⁻¹ * g⁻¹ = 1 := by
  simp only [mem_centralizer_iff, mul_inv_eq_iff_eq_mul, one_mul]
Characterization of Centralizer via Commutator Identity
Informal description
For any group $G$, an element $g \in G$ belongs to the centralizer of a subset $s \subseteq G$ if and only if for every $h \in s$, the commutator $h g h^{-1} g^{-1}$ equals the identity element $1$.
Subgroup.mem_centralizer_singleton_iff theorem
{g k : G} : k ∈ Subgroup.centralizer { g } ↔ k * g = g * k
Full source 
@[to_additive]
lemma mem_centralizer_singleton_iff {g k : G} :
    k ∈ Subgroup.centralizer {g}k ∈ Subgroup.centralizer {g} ↔ k * g = g * k := by
  simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq]
  exact eq_comm
Characterization of Centralizer Elements for Singleton Sets in a Group
Informal description
For any elements $g$ and $k$ in a group $G$, the element $k$ belongs to the centralizer of the singleton set $\{g\}$ if and only if $k$ commutes with $g$, i.e., $k * g = g * k$.
Subgroup.centralizer_univ theorem
: centralizer Set.univ = center G
Full source 
@[to_additive]
theorem centralizer_univ : centralizer Set.univ = center G :=
  SetLike.ext' (Set.centralizer_univ G)
Centralizer of Entire Group Equals Its Center
Informal description
For any group $G$, the centralizer of the universal set (the set of all elements of $G$) is equal to the center of $G$, i.e., $\text{centralizer}(G) = \text{center}(G)$.
Subgroup.center_le_centralizer theorem
(s) : center G ≤ centralizer s
Full source 
@[to_additive]
theorem center_le_centralizer (s) : center G ≤ centralizer s :=
  Set.center_subset_centralizer s
Center is Contained in Centralizer of Any Subset in a Group
Informal description
For any subset $s$ of a group $G$, the center of $G$ is contained in the centralizer of $s$, i.e., $\text{center}(G) \leq \text{centralizer}(s)$.
Subgroup.centralizer_le theorem
{s t : Set G} (h : s ⊆ t) : centralizer t ≤ centralizer s
Full source 
@[to_additive]
theorem centralizer_le {s t : Set G} (h : s ⊆ t) : centralizer t ≤ centralizer s :=
  Submonoid.centralizer_le h
Monotonicity of Centralizer with Respect to Subset Inclusion
Informal description
For any subsets $s$ and $t$ of a group $G$, if $s \subseteq t$, then the centralizer of $t$ is contained in the centralizer of $s$, i.e., $\text{centralizer}(t) \leq \text{centralizer}(s)$.
Subgroup.centralizer_eq_top_iff_subset theorem
{s : Set G} : centralizer s = ⊤ ↔ s ⊆ center G
Full source 
@[to_additive (attr := simp)]
theorem centralizer_eq_top_iff_subset {s : Set G} : centralizercentralizer s = ⊤ ↔ s ⊆ center G :=
  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset
Centralizer is Entire Group iff Subset is Central
Informal description
For any subset $s$ of a group $G$, the centralizer of $s$ equals the entire group $G$ if and only if $s$ is contained in the center of $G$. In other words: \[ \text{centralizer}(s) = G \leftrightarrow s \subseteq \text{center}(G). \]
Subgroup.map_centralizer_le_centralizer_image theorem
(s : Set G) (f : G →* G') : (Subgroup.centralizer s).map f ≤ Subgroup.centralizer (f '' s)
Full source 
@[to_additive]
theorem map_centralizer_le_centralizer_image (s : Set G) (f : G →* G') :
    (Subgroup.centralizer s).map f ≤ Subgroup.centralizer (f '' s) := by
  rintro - ⟨g, hg, rfl⟩ - ⟨h, hh, rfl⟩
  rw [← map_mul, ← map_mul, hg h hh]
Image of Centralizer is Contained in Centralizer of Image
Informal description
Let $G$ and $G'$ be groups, $s \subseteq G$ a subset, and $f \colon G \to G'$ a group homomorphism. Then the image of the centralizer of $s$ under $f$ is contained in the centralizer of the image of $s$ under $f$, i.e., \[ f(\{g \in G \mid \forall h \in s, gh = hg\}) \subseteq \{g' \in G' \mid \forall h' \in f(s), g'h' = h'g'\}. \]
Subgroup.Centralizer.characteristic instance
[hH : H.Characteristic] : (centralizer (H : Set G)).Characteristic
Full source 
@[to_additive]
instance Centralizer.characteristic [hH : H.Characteristic] :
    (centralizer (H : Set G)).Characteristic := by
  refine Subgroup.characteristic_iff_comap_le.mpr fun ϕ g hg h hh => ϕ.injective ?_
  rw [map_mul, map_mul]
  exact hg (ϕ h) (Subgroup.characteristic_iff_le_comap.mp hH ϕ hh)
Centralizer of a Characteristic Subgroup is Characteristic
Informal description
For any characteristic subgroup $H$ of a group $G$, the centralizer of $H$ in $G$ is also a characteristic subgroup.
Subgroup.le_centralizer_iff_isMulCommutative theorem
: K ≤ centralizer K ↔ IsMulCommutative K
Full source 
@[to_additive]
theorem le_centralizer_iff_isMulCommutative : K ≤ centralizer K ↔ IsMulCommutative K :=
  ⟨fun h => ⟨⟨fun x y => Subtype.ext (h y.2 x x.2)⟩⟩,
    fun h x hx y hy => congr_arg Subtype.val (h.1.1 ⟨y, hy⟩ ⟨x, hx⟩)⟩
Subgroup Contained in Its Centralizer iff Commutative
Informal description
A subgroup $K$ of a group $G$ is contained in its own centralizer if and only if the multiplication in $K$ is commutative, i.e., for all $k_1, k_2 \in K$, we have $k_1 \cdot k_2 = k_2 \cdot k_1$.
Subgroup.le_centralizer theorem
[h : IsMulCommutative H] : H ≤ centralizer H
Full source 
@[to_additive]
theorem le_centralizer [h : IsMulCommutative H] : H ≤ centralizer H :=
  le_centralizer_iff_isMulCommutative.mpr h
Commutative Subgroup is Contained in Its Centralizer
Informal description
Let $H$ be a subgroup of a group $G$. If the multiplication in $H$ is commutative (i.e., $h_1 h_2 = h_2 h_1$ for all $h_1, h_2 \in H$), then $H$ is contained in its own centralizer, i.e., $H \leq \text{centralizer}(H)$.
Subgroup.closure_le_centralizer_centralizer theorem
(s : Set G) : closure s ≤ centralizer (centralizer s)
Full source 
@[to_additive]
lemma closure_le_centralizer_centralizer (s : Set G) :
    closure s ≤ centralizer (centralizer s) :=
  closure_le _ |>.mpr Set.subset_centralizer_centralizer
Subgroup Generated by a Set is Contained in its Double Centralizer
Informal description
For any subset $s$ of a group $G$, the subgroup generated by $s$ is contained in the centralizer of the centralizer of $s$, i.e., $\langle s \rangle \leq \text{centralizer}(\text{centralizer}(s))$.
Subgroup.closureCommGroupOfComm abbrev
{k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x) : CommGroup (closure k)
Full source 
/-- If all the elements of a set `s` commute, then `closure s` is a commutative group. -/
@[to_additive
      "If all the elements of a set `s` commute, then `closure s` is an additive
      commutative group."]
abbrev closureCommGroupOfComm {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x) :
    CommGroup (closure k) :=
  { (closure k).toGroup with
    mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
      have := closure_le_centralizer_centralizer k
      Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }
Commutative Group Structure on the Closure of a Commuting Set
Informal description
For any subset $k$ of a group $G$, if all pairs of elements in $k$ commute (i.e., for all $x, y \in k$, $x * y = y * x$), then the subgroup generated by $k$ is a commutative group.
Subgroup.instMulDistribMulActionSubtypeMemNormalizer instance
: MulDistribMulAction H.normalizer H
Full source 
/-- The conjugation action of N(H) on H. -/
@[simps]
instance : MulDistribMulAction H.normalizer H where
  smul g h := ⟨g * h * g⁻¹, (g.2 h).mp h.2⟩
  one_smul g := by simp [HSMul.hSMul]
  mul_smul := by simp [HSMul.hSMul, mul_assoc]
  smul_one := by simp [HSMul.hSMul]
  smul_mul := by simp [HSMul.hSMul]
Distributive Multiplication Action of Normalizer on Subgroup
Informal description
For any subgroup $H$ of a group $G$, the normalizer $N(H)$ acts on $H$ by multiplication in a way that distributes over the group operation. This means that for any $n \in N(H)$ and $h_1, h_2 \in H$, we have $n \cdot (h_1 h_2) = (n \cdot h_1)(n \cdot h_2)$.
Subgroup.normalizerMonoidHom definition
: H.normalizer →* MulAut H
Full source 
/-- The homomorphism N(H) → Aut(H) with kernel C(H). -/
@[simps!]
def normalizerMonoidHom : H.normalizer →* MulAut H :=
  MulDistribMulAction.toMulAut H.normalizer H
Group homomorphism from normalizer to automorphisms of a subgroup
Informal description
The group homomorphism from the normalizer \( N(H) \) of a subgroup \( H \) to the group of multiplicative automorphisms of \( H \), where each element \( n \in N(H) \) is mapped to the automorphism \( h \mapsto n h n^{-1} \) of \( H \).
Subgroup.normalizerMonoidHom_ker theorem
: H.normalizerMonoidHom.ker = (Subgroup.centralizer H).subgroupOf H.normalizer
Full source 
theorem normalizerMonoidHom_ker :
    H.normalizerMonoidHom.ker = (Subgroup.centralizer H).subgroupOf H.normalizer := by
  simp [Subgroup.ext_iff, DFunLike.ext_iff, Subtype.ext_iff,
    mem_subgroupOf, mem_centralizer_iff, eq_mul_inv_iff_mul_eq, eq_comm]
Kernel of Normalizer-to-Automorphism Homomorphism Equals Centralizer in Normalizer
Informal description
The kernel of the group homomorphism from the normalizer $N(H)$ of a subgroup $H$ to the group of multiplicative automorphisms of $H$ is equal to the centralizer of $H$ considered as a subgroup of $N(H)$. In other words, $\ker(\text{normalizerMonoidHom}) = \text{centralizer}(H) \cap N(H)$.