centralizer_centralizer_centralizer

English

For any subset S of an algebra A over a commutative ring R, the centralizer of the centralizer of S is equal to the centralizer of S; i.e., C_R(C_R(S)) = C_R(S).

Русский

Для любого подмножества S подалгебры A над коммутативным кольцом R выполняется равенство центральизатора центральизатора S и центральизатора S: C_R(C_R(S)) = C_R(S).

LaTeX

$$$\operatorname{centralizer}_R\bigl(S^{\text{centralizer}}^{\text{centralizer}}\bigr) = \operatorname{centralizer}_R(S)$$$

Lean4

@[simp]
theorem centralizer_centralizer_centralizer {s : Set A} : centralizer R s.centralizer.centralizer = centralizer R s :=
  by
  apply SetLike.coe_injective
  simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]

Похожие утверждения