DoubleCentralizer.central
theorem DoubleCentralizer.central :
β {π : Type u} {A : Type v} [inst : NontriviallyNormedField π] [inst_1 : NonUnitalNormedRing A]
[inst_2 : NormedSpace π A] [inst_3 : SMulCommClass π A A] [inst_4 : IsScalarTower π A A]
(self : DoubleCentralizer π A) (x y : A), self.toProd.2 x * y = x * self.toProd.1 y
The theorem `DoubleCentralizer.central` states that, given any scalar field `π` and any non-unital normed ring `A` that forms a normed space over `π`, and given that scalar multiplication in `A` commutes and `A` forms a scalar tower over `π`, for any `DoubleCentralizer` instance `self` and any elements `x` and `y` of `A`, the second component of the product `self.toProd.2 x` when multiplied by `y` equals `x` multiplied by the first component of the product `self.toProd.1 y`.
In other words, this theorem establishes a centrality condition for the double centralizer: the two associated linear maps intertwine each other.
More concisely: Given a non-unital normed ring `A` over a scalar field `π`, where scalar multiplication commutes and `A` forms a scalar tower, the double centralizer maps commute, i.e., `self.toProd.1 (y * x) = self.toProd.2.1 y * x` for any `DoubleCentralizer` instance `self` and elements `x, y` in `A`.
|
DoubleCentralizer.norm_fst_eq_snd
theorem DoubleCentralizer.norm_fst_eq_snd :
β {π : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NonUnitalNormedRing A]
[inst_2 : NormedSpace π A] [inst_3 : SMulCommClass π A A] [inst_4 : IsScalarTower π A A] [inst_5 : StarRing A]
[inst_6 : CstarRing A] (a : DoubleCentralizer π A), βa.toProd.1β = βa.toProd.2β
This theorem states that for every `a`, which is an element of the double centralizer of `π` over `A`, the norms of the first and second components of `a` are equal. Here, `π` is a nontrivially normed field, `A` is a non-unital normed ring that is also a star ring and a C* ring, and it forms a normed space over `π`. Moreover, `π` and `A` have the scalar multiplication commutativity property and `π` is a scalar tower over `A`. The norm of `a` is defined as the maximum of the norms of its first and second components.
More concisely: For every element `a` in the double centralizer of a nontrivially normed field `π` over a non-unital normed ring `A` that is a star ring and C*, if `a` has first and second components, then the norms of these components are equal.
|