Mathlib.Algebra.GroupWithZero.Center

Set.zero_mem_center theorem

: (0 : M₀) ∈ center M₀

Full source

@[simp] lemma zero_mem_center : (0 : M₀) ∈ center M₀ where
  comm _ := by rw [zero_mul, mul_zero]
  left_assoc _ _ := by rw [zero_mul, zero_mul, zero_mul]
  mid_assoc _ _ := by rw [mul_zero, zero_mul, mul_zero]
  right_assoc _ _ := by rw [mul_zero, mul_zero, mul_zero]

Zero is Central in a Magma with Zero

Informal description

For any magma with zero $M_0$, the zero element $0$ belongs to the center of $M_0$, i.e., $0 \in Z(M_0)$ where $Z(M_0)$ denotes the set of elements that commute with every element of $M_0$.

Set.zero_mem_centralizer theorem

: (0 : M₀) ∈ centralizer s

Full source

@[simp] lemma zero_mem_centralizer : (0 : M₀) ∈ centralizer s := by simp [mem_centralizer_iff]

Zero Element is in the Centralizer of Any Subset

Informal description

For any magma with zero $M₀$ and any subset $s \subseteq M₀$, the zero element $0$ belongs to the centralizer of $s$, i.e., $0 \in \text{centralizer}(s)$.

Set.center_units_subset theorem

: center G₀ˣ ⊆ ((↑) : G₀ˣ → G₀) ⁻¹' center G₀

Full source

lemma center_units_subset : centercenter G₀ˣ ⊆ ((↑) : G₀ˣ → G₀) ⁻¹' center G₀ := by
  simp_rw [subset_def, mem_preimage, _root_.Semigroup.mem_center_iff]
  intro u hu a
  obtain rfl | ha := eq_or_ne a 0
  · rw [zero_mul, mul_zero]
  · exact congr_arg Units.val <| hu <| Units.mk0 a ha

Inclusion of Units' Center in Group with Zero Center

Informal description

For a group with zero $G_0$, the center of its group of units $G_0^\times$ is a subset of the preimage of the center of $G_0$ under the canonical inclusion map $(\cdot)^\times \hookrightarrow G_0$. In other words, if $z \in Z(G_0^\times)$, then $z \in Z(G_0)$ when considered as an element of $G_0$.

Set.center_units_eq theorem

: center G₀ˣ = ((↑) : G₀ˣ → G₀) ⁻¹' center G₀

Full source

/-- In a group with zero, the center of the units is the preimage of the center. -/
lemma center_units_eq : center G₀ˣ = ((↑) : G₀ˣ → G₀) ⁻¹' center G₀ :=
  center_units_subset.antisymm subset_center_units

Equality of Units' Center and Preimage of Group Center in a Group with Zero

Informal description

For a group with zero $G_0$, the center of its group of units $G_0^\times$ is equal to the preimage of the center of $G_0$ under the canonical inclusion map $(\cdot)^\times \hookrightarrow G_0$. In other words, an element $u \in G_0^\times$ is in the center of $G_0^\times$ if and only if its image in $G_0$ is in the center of $G_0$.

Set.inv_mem_centralizer₀ theorem

(ha : a ∈ centralizer s) : a⁻¹ ∈ centralizer s

Full source

@[simp] lemma inv_mem_centralizer₀ (ha : a ∈ centralizer s) : a⁻¹a⁻¹ ∈ centralizer s := by
  obtain rfl | ha₀ := eq_or_ne a 0
  · rw [inv_zero]
    exact zero_mem_centralizer
  · rintro c hc
    rw [mul_inv_eq_iff_eq_mul₀ ha₀, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha₀, ha c hc]

Inverse of Centralizer Element in Group with Zero

Informal description

For any element $a$ in the centralizer of a subset $s$ of a group with zero $G₀$, the inverse $a^{-1}$ also belongs to the centralizer of $s$.

Set.div_mem_centralizer₀ theorem

(ha : a ∈ centralizer s) (hb : b ∈ centralizer s) : a / b ∈ centralizer s

Full source

@[simp] lemma div_mem_centralizer₀ (ha : a ∈ centralizer s) (hb : b ∈ centralizer s) :
    a / b ∈ centralizer s := by
  simpa only [div_eq_mul_inv] using mul_mem_centralizer ha (inv_mem_centralizer₀ hb)

Division of Centralizer Elements in Group with Zero

Informal description

For any elements $a$ and $b$ in the centralizer of a subset $s$ of a group with zero $G₀$, the division $a / b$ also belongs to the centralizer of $s$.