Theorems · Inductive type · functional analysis

NonUnitalContinuousFunctionalCalculus

(R : Type u_1) →
  (A : Type u_2) →
    outParam (A → Prop) →
      [inst : CommSemiring R] →
        [Nontrivial R] →
          [inst_2 : StarRing R] →
            [inst_3 : MetricSpace R] →
              [IsTopologicalSemiring R] →
                [ContinuousStar R] →
                  [inst_6 : NonUnitalRing A] →
                    [StarRing A] →
                      [TopologicalSpace A] →
                        [inst_9 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → Prop

A non-unital star R-algebra A has a continuous functional calculus for elements satisfying the property p : A → Prop if + for every such element a : A there is a non-unital star algebra homomorphism cfcₙHom : C(quasispectrum R a, R)₀ →⋆ₙₐ[R] A sending the (restriction of) the identity map to a. + cfcHom is continuous and injective and the quasispectrum of the image of function f is its range. + cfcₙHom preserves the property p. The property p is marked as an outParam so that the user need not specify it. In practice, + for R := ℂ, we choose p := IsStarNormal, + for R := ℝ, we choose p := IsSelfAdjoint, + for R := ℝ≥0, we choose p := (0 ≤ ·). Instead of directly providing the data we opt instead for a Prop class. In all relevant cases, the continuous functional calculus is uniquely determined, and utilizing this approach prevents diamonds or problems arising from multiple instances.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Cited by

275 results in Mathlib

Foundations

Depth 11 from the axioms, rests on 147 definitions · uses no axioms

Assumes

CommSemiringNontrivialStarRingMetricSpaceIsTopologicalSemiringContinuousStarNonUnitalRingStarRingTopologicalSpaceModuleIsScalarTowerSMulCommClass