Documentation

Mathlib.Analysis.NormedSpace.Star.Multiplier

Multiplier Algebra of a C⋆-algebra #

Define the multiplier algebra of a C⋆-algebra as the algebra (over π•œ) of double centralizers, for which we provide the localized notation π“œ(π•œ, A). A double centralizer is a pair of continuous linear maps L R : A β†’L[π•œ] A satisfying the intertwining condition R x * y = x * L y.

There is a natural embedding A β†’ π“œ(π•œ, A) which sends a : A to the continuous linear maps L R : A β†’L[π•œ] A given by left and right multiplication by a, and we provide this map as a coercion.

The multiplier algebra corresponds to a non-commutative Stoneβ€“ΔŒech compactification in the sense that when the algebra A is commutative, it can be identified with Cβ‚€(X, β„‚) for some locally compact Hausdorff space X, and in that case π“œ(π•œ, A) can be identified with C(Ξ² X, β„‚).

Implementation notes #

We make the hypotheses on π•œ as weak as possible so that, in particular, this construction works for both π•œ = ℝ and π•œ = β„‚.

The reader familiar with C⋆-algebra theory may recognize that one only needs L and R to be functions instead of continuous linear maps, at least when A is a C⋆-algebra. Our intention is simply to eventually provide a constructor for this situation.

We pull back the NormedAlgebra structure (and everything contained therein) through the ring (even algebra) homomorphism DoubleCentralizer.toProdMulOppositeHom : π“œ(π•œ, A) β†’+* (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A)ᡐᡒᡖ which sends a : π“œ(π•œ, A) to (a.fst, MulOpposite.op a.snd). The star structure is provided separately.

References #

TODO #

structure DoubleCentralizer (π•œ : Type u) (A : Type v) [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] extends Prod :

The type of double centralizers, also known as the multiplier algebra and denoted by π“œ(π•œ, A), of a non-unital normed algebra.

If x : π“œ(π•œ, A), then x.fst and x.snd are what is usually referred to as $L$ and $R$.

  • fst : A β†’L[π•œ] A
  • snd : A β†’L[π•œ] A
  • central : βˆ€ (x y : A), self.toProd.2 x * y = x * self.toProd.1 y

    The centrality condition that the maps linear maps intertwine one another.

Instances For
    theorem DoubleCentralizer.central {π•œ : Type u} {A : Type v} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (self : DoubleCentralizer π•œ A) (x : A) (y : A) :
    self.toProd.2 x * y = x * self.toProd.1 y

    The centrality condition that the maps linear maps intertwine one another.

    The type of double centralizers, also known as the multiplier algebra and denoted by π“œ(π•œ, A), of a non-unital normed algebra.

    If x : π“œ(π•œ, A), then x.fst and x.snd are what is usually referred to as $L$ and $R$.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem DoubleCentralizer.ext (π•œ : Type u) (A : Type v) [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) (b : DoubleCentralizer π•œ A) (h : a.toProd = b.toProd) :
      a = b

      Algebraic structure #

      Because the multiplier algebra is defined as the algebra of double centralizers, there is a natural injection DoubleCentralizer.toProdMulOpposite : π“œ(π•œ, A) β†’ (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A)ᡐᡒᡖ defined by fun a ↦ (a.fst, MulOpposite.op a.snd). We use this map to pull back the ring, module and algebra structure from (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A)ᡐᡒᡖ to π“œ(π•œ, A).

      theorem DoubleCentralizer.range_toProd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      Set.range DoubleCentralizer.toProd = {lr : (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A) | βˆ€ (x y : A), lr.2 x * y = x * lr.1 y}
      instance DoubleCentralizer.instAdd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      Add (DoubleCentralizer π•œ A)
      Equations
      • DoubleCentralizer.instAdd = { add := fun (a b : DoubleCentralizer π•œ A) => { toProd := a.toProd + b.toProd, central := β‹― } }
      instance DoubleCentralizer.instZero {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      Zero (DoubleCentralizer π•œ A)
      Equations
      • DoubleCentralizer.instZero = { zero := { toProd := 0, central := β‹― } }
      instance DoubleCentralizer.instNeg {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      Neg (DoubleCentralizer π•œ A)
      Equations
      • DoubleCentralizer.instNeg = { neg := fun (a : DoubleCentralizer π•œ A) => { toProd := -a.toProd, central := β‹― } }
      instance DoubleCentralizer.instSub {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      Sub (DoubleCentralizer π•œ A)
      Equations
      • DoubleCentralizer.instSub = { sub := fun (a b : DoubleCentralizer π•œ A) => { toProd := a.toProd - b.toProd, central := β‹― } }
      instance DoubleCentralizer.instSMul {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] {S : Type u_3} [Monoid S] [DistribMulAction S A] [SMulCommClass π•œ S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] :
      SMul S (DoubleCentralizer π•œ A)
      Equations
      • DoubleCentralizer.instSMul = { smul := fun (s : S) (a : DoubleCentralizer π•œ A) => { toProd := s β€’ a.toProd, central := β‹― } }
      @[simp]
      theorem DoubleCentralizer.smul_toProd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] {S : Type u_3} [Monoid S] [DistribMulAction S A] [SMulCommClass π•œ S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] (s : S) (a : DoubleCentralizer π•œ A) :
      (s β€’ a).toProd = s β€’ a.toProd
      theorem DoubleCentralizer.smul_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] {S : Type u_3} [Monoid S] [DistribMulAction S A] [SMulCommClass π•œ S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] (s : S) (a : DoubleCentralizer π•œ A) :
      (s β€’ a).toProd.1 = s β€’ a.toProd.1
      theorem DoubleCentralizer.smul_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] {S : Type u_3} [Monoid S] [DistribMulAction S A] [SMulCommClass π•œ S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] (s : S) (a : DoubleCentralizer π•œ A) :
      (s β€’ a).toProd.2 = s β€’ a.toProd.2
      instance DoubleCentralizer.instIsScalarTower {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] {S : Type u_3} [Monoid S] [DistribMulAction S A] [SMulCommClass π•œ S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] {T : Type u_4} [Monoid T] [DistribMulAction T A] [SMulCommClass π•œ T A] [ContinuousConstSMul T A] [IsScalarTower T A A] [SMulCommClass T A A] [SMul S T] [IsScalarTower S T A] :
      Equations
      • β‹― = β‹―
      instance DoubleCentralizer.instSMulCommClass {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] {S : Type u_3} [Monoid S] [DistribMulAction S A] [SMulCommClass π•œ S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] {T : Type u_4} [Monoid T] [DistribMulAction T A] [SMulCommClass π•œ T A] [ContinuousConstSMul T A] [IsScalarTower T A A] [SMulCommClass T A A] [SMulCommClass S T A] :
      Equations
      • β‹― = β‹―
      instance DoubleCentralizer.instIsCentralScalar {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] {R : Type u_5} [Semiring R] [Module R A] [SMulCommClass π•œ R A] [ContinuousConstSMul R A] [IsScalarTower R A A] [SMulCommClass R A A] [Module Rᡐᡒᡖ A] [IsCentralScalar R A] :
      Equations
      • β‹― = β‹―
      instance DoubleCentralizer.instOne {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      One (DoubleCentralizer π•œ A)
      Equations
      • DoubleCentralizer.instOne = { one := { toProd := 1, central := β‹― } }
      instance DoubleCentralizer.instMul {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      Mul (DoubleCentralizer π•œ A)
      Equations
      • DoubleCentralizer.instMul = { mul := fun (a b : DoubleCentralizer π•œ A) => { toProd := (a.toProd.1.comp b.toProd.1, b.toProd.2.comp a.toProd.2), central := β‹― } }
      instance DoubleCentralizer.instNatCast {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      Equations
      • DoubleCentralizer.instNatCast = { natCast := fun (n : β„•) => { toProd := ↑n, central := β‹― } }
      instance DoubleCentralizer.instIntCast {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      Equations
      • DoubleCentralizer.instIntCast = { intCast := fun (n : β„€) => { toProd := ↑n, central := β‹― } }
      instance DoubleCentralizer.instPow {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      Equations
      • DoubleCentralizer.instPow = { pow := fun (a : DoubleCentralizer π•œ A) (n : β„•) => { toProd := a.toProd ^ n, central := β‹― } }
      instance DoubleCentralizer.instInhabited {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      Equations
      • DoubleCentralizer.instInhabited = { default := 0 }
      @[simp]
      theorem DoubleCentralizer.add_toProd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) (b : DoubleCentralizer π•œ A) :
      (a + b).toProd = a.toProd + b.toProd
      @[simp]
      theorem DoubleCentralizer.zero_toProd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      @[simp]
      theorem DoubleCentralizer.neg_toProd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) :
      (-a).toProd = -a.toProd
      @[simp]
      theorem DoubleCentralizer.sub_toProd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) (b : DoubleCentralizer π•œ A) :
      (a - b).toProd = a.toProd - b.toProd
      @[simp]
      theorem DoubleCentralizer.one_toProd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      @[simp]
      theorem DoubleCentralizer.natCast_toProd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„•) :
      (↑n).toProd = ↑n
      @[deprecated DoubleCentralizer.natCast_toProd]
      theorem DoubleCentralizer.nat_cast_toProd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„•) :
      (↑n).toProd = ↑n

      Alias of DoubleCentralizer.natCast_toProd.

      @[simp]
      theorem DoubleCentralizer.intCast_toProd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„€) :
      (↑n).toProd = ↑n
      @[deprecated DoubleCentralizer.intCast_toProd]
      theorem DoubleCentralizer.int_cast_toProd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„€) :
      (↑n).toProd = ↑n

      Alias of DoubleCentralizer.intCast_toProd.

      @[simp]
      theorem DoubleCentralizer.pow_toProd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„•) (a : DoubleCentralizer π•œ A) :
      (a ^ n).toProd = a.toProd ^ n
      theorem DoubleCentralizer.add_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) (b : DoubleCentralizer π•œ A) :
      (a + b).toProd.1 = a.toProd.1 + b.toProd.1
      theorem DoubleCentralizer.add_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) (b : DoubleCentralizer π•œ A) :
      (a + b).toProd.2 = a.toProd.2 + b.toProd.2
      theorem DoubleCentralizer.zero_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      theorem DoubleCentralizer.zero_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      theorem DoubleCentralizer.neg_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) :
      (-a).toProd.1 = -a.toProd.1
      theorem DoubleCentralizer.neg_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) :
      (-a).toProd.2 = -a.toProd.2
      theorem DoubleCentralizer.sub_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) (b : DoubleCentralizer π•œ A) :
      (a - b).toProd.1 = a.toProd.1 - b.toProd.1
      theorem DoubleCentralizer.sub_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) (b : DoubleCentralizer π•œ A) :
      (a - b).toProd.2 = a.toProd.2 - b.toProd.2
      theorem DoubleCentralizer.one_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      theorem DoubleCentralizer.one_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      @[simp]
      theorem DoubleCentralizer.mul_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) (b : DoubleCentralizer π•œ A) :
      (a * b).toProd.1 = a.toProd.1 * b.toProd.1
      @[simp]
      theorem DoubleCentralizer.mul_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) (b : DoubleCentralizer π•œ A) :
      (a * b).toProd.2 = b.toProd.2 * a.toProd.2
      theorem DoubleCentralizer.natCast_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„•) :
      (↑n).toProd.1 = ↑n
      @[deprecated DoubleCentralizer.natCast_fst]
      theorem DoubleCentralizer.nat_cast_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„•) :
      (↑n).toProd.1 = ↑n

      Alias of DoubleCentralizer.natCast_fst.

      theorem DoubleCentralizer.natCast_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„•) :
      (↑n).toProd.2 = ↑n
      @[deprecated DoubleCentralizer.natCast_snd]
      theorem DoubleCentralizer.nat_cast_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„•) :
      (↑n).toProd.2 = ↑n

      Alias of DoubleCentralizer.natCast_snd.

      theorem DoubleCentralizer.intCast_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„€) :
      (↑n).toProd.1 = ↑n
      @[deprecated DoubleCentralizer.intCast_fst]
      theorem DoubleCentralizer.int_cast_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„€) :
      (↑n).toProd.1 = ↑n

      Alias of DoubleCentralizer.intCast_fst.

      theorem DoubleCentralizer.intCast_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„€) :
      (↑n).toProd.2 = ↑n
      @[deprecated DoubleCentralizer.intCast_snd]
      theorem DoubleCentralizer.int_cast_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„€) :
      (↑n).toProd.2 = ↑n

      Alias of DoubleCentralizer.intCast_snd.

      theorem DoubleCentralizer.pow_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„•) (a : DoubleCentralizer π•œ A) :
      (a ^ n).toProd.1 = a.toProd.1 ^ n
      theorem DoubleCentralizer.pow_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (n : β„•) (a : DoubleCentralizer π•œ A) :
      (a ^ n).toProd.2 = a.toProd.2 ^ n
      def DoubleCentralizer.toProdMulOpposite {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
      DoubleCentralizer π•œ A β†’ (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A)ᡐᡒᡖ

      The natural injection from DoubleCentralizer.toProd except the second coordinate inherits MulOpposite.op. The ring structure on π“œ(π•œ, A) is the pullback under this map.

      Equations
      Instances For
        theorem DoubleCentralizer.toProdMulOpposite_injective {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
        Function.Injective DoubleCentralizer.toProdMulOpposite
        theorem DoubleCentralizer.range_toProdMulOpposite {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
        Set.range DoubleCentralizer.toProdMulOpposite = {lr : (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A)ᡐᡒᡖ | βˆ€ (x y : A), lr.2.unop x * y = x * lr.1 y}
        instance DoubleCentralizer.instRing {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
        Ring (DoubleCentralizer π•œ A)

        The ring structure is inherited as the pullback under the injective map DoubleCentralizer.toProdMulOpposite : π“œ(π•œ, A) β†’ (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A)ᡐᡒᡖ

        Equations
        • DoubleCentralizer.instRing = Function.Injective.ring DoubleCentralizer.toProdMulOpposite β‹― β‹― β‹― β‹― β‹― β‹― β‹― β‹― β‹― β‹― β‹― β‹―
        @[simp]
        theorem DoubleCentralizer.toProdHom_apply {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (self : DoubleCentralizer π•œ A) :
        DoubleCentralizer.toProdHom self = self.toProd
        def DoubleCentralizer.toProdHom {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
        DoubleCentralizer π•œ A β†’+ (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A)

        The canonical map DoubleCentralizer.toProd as an additive group homomorphism.

        Equations
        • DoubleCentralizer.toProdHom = { toFun := DoubleCentralizer.toProd, map_zero' := β‹―, map_add' := β‹― }
        Instances For
          @[simp]
          theorem DoubleCentralizer.toProdMulOppositeHom_apply {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
          βˆ€ (a : DoubleCentralizer π•œ A), DoubleCentralizer.toProdMulOppositeHom a = a.toProdMulOpposite
          def DoubleCentralizer.toProdMulOppositeHom {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :

          The canonical map DoubleCentralizer.toProdMulOpposite as a ring homomorphism.

          Equations
          • DoubleCentralizer.toProdMulOppositeHom = { toFun := DoubleCentralizer.toProdMulOpposite, map_one' := β‹―, map_mul' := β‹―, map_zero' := β‹―, map_add' := β‹― }
          Instances For
            instance DoubleCentralizer.instModule {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] {S : Type u_3} [Semiring S] [Module S A] [SMulCommClass π•œ S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] :
            Module S (DoubleCentralizer π•œ A)

            The module structure is inherited as the pullback under the additive group monomorphism DoubleCentralizer.toProd : π“œ(π•œ, A) β†’+ (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A)

            Equations
            instance DoubleCentralizer.instAlgebra {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
            Algebra π•œ (DoubleCentralizer π•œ A)
            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem DoubleCentralizer.algebraMap_toProd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (k : π•œ) :
            ((algebraMap π•œ (DoubleCentralizer π•œ A)) k).toProd = (algebraMap π•œ ((A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A))) k
            theorem DoubleCentralizer.algebraMap_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (k : π•œ) :
            ((algebraMap π•œ (DoubleCentralizer π•œ A)) k).toProd.1 = (algebraMap π•œ (A β†’L[π•œ] A)) k
            theorem DoubleCentralizer.algebraMap_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (k : π•œ) :
            ((algebraMap π•œ (DoubleCentralizer π•œ A)) k).toProd.2 = (algebraMap π•œ (A β†’L[π•œ] A)) k

            Star structure #

            instance DoubleCentralizer.instStar {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing π•œ] [StarRing A] [StarModule π•œ A] [NormedStarGroup A] :
            Star (DoubleCentralizer π•œ A)

            The star operation on a : π“œ(π•œ, A) is given by (star a).toProd = (star ∘ a.snd ∘ star, star ∘ a.fst ∘ star).

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem DoubleCentralizer.star_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing π•œ] [StarRing A] [StarModule π•œ A] [NormedStarGroup A] (a : DoubleCentralizer π•œ A) (b : A) :
            (star a).toProd.1 b = star (a.toProd.2 (star b))
            @[simp]
            theorem DoubleCentralizer.star_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing π•œ] [StarRing A] [StarModule π•œ A] [NormedStarGroup A] (a : DoubleCentralizer π•œ A) (b : A) :
            (star a).toProd.2 b = star (a.toProd.1 (star b))
            instance DoubleCentralizer.instStarAddMonoid {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing π•œ] [StarRing A] [StarModule π•œ A] [NormedStarGroup A] :
            Equations
            • DoubleCentralizer.instStarAddMonoid = let __src := DoubleCentralizer.instStar; StarAddMonoid.mk β‹―
            instance DoubleCentralizer.instStarRing {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing π•œ] [StarRing A] [StarModule π•œ A] [NormedStarGroup A] :
            Equations
            • DoubleCentralizer.instStarRing = let __src := DoubleCentralizer.instStarAddMonoid; StarRing.mk β‹―
            instance DoubleCentralizer.instStarModule {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing π•œ] [StarRing A] [StarModule π•œ A] [NormedStarGroup A] :
            StarModule π•œ (DoubleCentralizer π•œ A)
            Equations
            • β‹― = β‹―

            Coercion from an algebra into its multiplier algebra #

            noncomputable def DoubleCentralizer.coe (π•œ : Type u_1) {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : A) :

            The natural coercion of A into π“œ(π•œ, A) given by sending a : A to the pair of linear maps Lₐ Rₐ : A β†’L[π•œ] A given by left- and right-multiplication by a, respectively.

            Warning: if A = π•œ, then this is a coercion which is not definitionally equal to the algebraMap π•œ π“œ(π•œ, π•œ) coercion, but these are propositionally equal. See DoubleCentralizer.coe_eq_algebraMap below.

            Equations
            Instances For
              noncomputable instance DoubleCentralizer.instCoeTC {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
              CoeTC A (DoubleCentralizer π•œ A)

              The natural coercion of A into π“œ(π•œ, A) given by sending a : A to the pair of linear maps Lₐ Rₐ : A β†’L[π•œ] A given by left- and right-multiplication by a, respectively.

              Warning: if A = π•œ, then this is a coercion which is not definitionally equal to the algebraMap π•œ π“œ(π•œ, π•œ) coercion, but these are propositionally equal. See DoubleCentralizer.coe_eq_algebraMap below.

              Equations
              • DoubleCentralizer.instCoeTC = { coe := β†‘π•œ }
              @[simp]
              theorem DoubleCentralizer.coe_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : A) :
              (β†‘π•œ a).toProd.1 = (ContinuousLinearMap.mul π•œ A) a
              @[simp]
              theorem DoubleCentralizer.coe_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : A) :
              (β†‘π•œ a).toProd.2 = (ContinuousLinearMap.mul π•œ A).flip a
              theorem DoubleCentralizer.coe_eq_algebraMap {π•œ : Type u_1} [NontriviallyNormedField π•œ] :
              β†‘π•œ = ⇑(algebraMap π•œ (DoubleCentralizer π•œ π•œ))
              @[simp]
              theorem DoubleCentralizer.coeHom_apply {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing π•œ] [StarRing A] [StarModule π•œ A] [NormedStarGroup A] (a : A) :
              DoubleCentralizer.coeHom a = β†‘π•œ a
              noncomputable def DoubleCentralizer.coeHom {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing π•œ] [StarRing A] [StarModule π•œ A] [NormedStarGroup A] :

              The coercion of an algebra into its multiplier algebra as a non-unital star algebra homomorphism.

              Equations
              • DoubleCentralizer.coeHom = { toFun := fun (a : A) => β†‘π•œ a, map_smul' := β‹―, map_zero' := β‹―, map_add' := β‹―, map_mul' := β‹―, map_star' := β‹― }
              Instances For

                Norm structures #

                We define the norm structure on π“œ(π•œ, A) as the pullback under DoubleCentralizer.toProdMulOppositeHom : π“œ(π•œ, A) β†’+* (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A)ᡐᡒᡖ, which provides a definitional isometric embedding. Consequently, completeness of π“œ(π•œ, A) is obtained by proving that the range of this map is closed.

                In addition, we prove that π“œ(π•œ, A) is a normed algebra, and, when A is a C⋆-algebra, we show that π“œ(π•œ, A) is also a C⋆-algebra. Moreover, in this case, for a : π“œ(π•œ, A), β€–aβ€– = β€–a.fstβ€– = β€–a.sndβ€–.

                noncomputable instance DoubleCentralizer.instNormedRing {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :

                The normed group structure is inherited as the pullback under the ring monomorphism DoubleCentralizer.toProdMulOppositeHom : π“œ(π•œ, A) β†’+* (A β†’L[π•œ] A) Γ— (A β†’L[π•œ] A)ᡐᡒᡖ.

                Equations
                theorem DoubleCentralizer.norm_def {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) :
                β€–aβ€– = β€–DoubleCentralizer.toProdHom aβ€–
                theorem DoubleCentralizer.nnnorm_def {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) :
                β€–aβ€–β‚Š = β€–DoubleCentralizer.toProdHom aβ€–β‚Š
                theorem DoubleCentralizer.norm_def' {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) :
                β€–aβ€– = β€–DoubleCentralizer.toProdMulOppositeHom aβ€–
                theorem DoubleCentralizer.nnnorm_def' {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] (a : DoubleCentralizer π•œ A) :
                β€–aβ€–β‚Š = β€–DoubleCentralizer.toProdMulOppositeHom aβ€–β‚Š
                instance DoubleCentralizer.instNormedSpace {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
                NormedSpace π•œ (DoubleCentralizer π•œ A)
                Equations
                • DoubleCentralizer.instNormedSpace = let __src := DoubleCentralizer.instModule; NormedSpace.mk β‹―
                instance DoubleCentralizer.instNormedAlgebra {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
                NormedAlgebra π•œ (DoubleCentralizer π•œ A)
                Equations
                • DoubleCentralizer.instNormedAlgebra = let __src := DoubleCentralizer.instAlgebra; let __src_1 := DoubleCentralizer.instNormedSpace; NormedAlgebra.mk β‹―
                theorem DoubleCentralizer.uniformEmbedding_toProdMulOpposite {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] :
                UniformEmbedding DoubleCentralizer.toProdMulOpposite
                instance DoubleCentralizer.instCompleteSpace {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [CompleteSpace A] :
                Equations
                • β‹― = β‹―
                theorem DoubleCentralizer.norm_fst_eq_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing A] [CstarRing A] (a : DoubleCentralizer π•œ A) :
                β€–a.toProd.1β€– = β€–a.toProd.2β€–

                For a : π“œ(π•œ, A), the norms of a.fst and a.snd coincide, and hence these also coincide with β€–aβ€– which is max (β€–a.fstβ€–) (β€–a.sndβ€–).

                theorem DoubleCentralizer.nnnorm_fst_eq_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing A] [CstarRing A] (a : DoubleCentralizer π•œ A) :
                @[simp]
                theorem DoubleCentralizer.norm_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing A] [CstarRing A] (a : DoubleCentralizer π•œ A) :
                @[simp]
                theorem DoubleCentralizer.norm_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing A] [CstarRing A] (a : DoubleCentralizer π•œ A) :
                @[simp]
                theorem DoubleCentralizer.nnnorm_fst {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing A] [CstarRing A] (a : DoubleCentralizer π•œ A) :
                @[simp]
                theorem DoubleCentralizer.nnnorm_snd {π•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField π•œ] [NonUnitalNormedRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarRing A] [CstarRing A] (a : DoubleCentralizer π•œ A) :
                instance DoubleCentralizer.instCstarRing {π•œ : Type u_1} {A : Type u_2} [DenselyNormedField π•œ] [StarRing π•œ] [NonUnitalNormedRing A] [StarRing A] [CstarRing A] [NormedSpace π•œ A] [SMulCommClass π•œ A A] [IsScalarTower π•œ A A] [StarModule π•œ A] :
                Equations
                • β‹― = β‹―