English
Let R be a commutative semiring and A a topological nonunital star algebra with a subset s of A. Then the closed subalgebra generated by s sits inside the double centralizer of s; that is, every element in the topological closure of adjoin_R(s) commutes with every element that commutes with s.
Русский
Пусть R — коммутативное полуребро, A — топологическая небезъядерная звездная алгебра над R, и S—множество в A. Замыкание по топологии подалгебры, порожденной S, содержится во втором центральизаторе S, то есть каждый элемент замыкания адьоина коммутирует с любым, кто коммутирует с S.
LaTeX
$$$\\overline{\\operatorname{adjoin}_R(S)} \\\\le \\operatorname{centralizer}_R\\bigl(\\operatorname{centralizer}_R(S)\\bigr).$$$
Lean4
theorem topologicalClosure_adjoin_le_centralizer_centralizer (R : Type*) {A : Type*} [CommSemiring R] [StarRing R]
[TopologicalSpace A] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsTopologicalSemiring A] [ContinuousStar A]
[ContinuousConstSMul R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [T2Space A] (s : Set A) :
(adjoin R s).topologicalClosure ≤ centralizer R (centralizer R s) :=
topologicalClosure_minimal _ (adjoin_le_centralizer_centralizer R s) (Set.isClosed_centralizer _)
