Continuous functions as a star-ordered ring

The type class ContinuousSqrt gives a sufficient condition on R to make C(α, R) and C(α, R)₀ into a StarOrderedRing for any topological space α, thereby providing a means by which we can ensure C(α, R) has this property. This condition is satisfied by ℝ≥0, ℝ, and ℂ, and the instances can be found in the file Mathlib/Topology/ContinuousMap/ContinuousSqrt.lean.

Implementation notes

Instead of asking for a well-behaved square root on {x : R | 0 ≤ x} in the obvious way, we instead require that, for every x y : R such that x ≤ y, there exist some s such that x + s*s = y. This is because we need this type class to work for ℝ≥0 for the continuous functional calculus. We could instead assume [OrderedSub R] [ContinuousSub R], but that would lead to a proliferation of type class assumptions in the general case of the continuous functional calculus, which we want to avoid because there is already a proliferation of type classes there. At the moment, we only expect this class to be used in that context so this is a reasonable compromise.

The field ContinuousSqrt.sqrt is data, which means that, if we implement an instance of the class for a generic C⋆-algebra, we'll get a non-defeq diamond for the case R := ℂ. This shouldn't really be a problem since the only purpose is to obtain the instance StarOrderedRing C(α, R), which is a Prop, but we note it for future reference.

class ContinuousSqrt (R : Type u_1) [LE R] [NonUnitalSemiring R] [TopologicalSpace R] : Type u_1

A type class encoding the property that there is a continuous square root function on nonnegative elements. This holds for ℝ≥0, ℝ and ℂ (as well as any C⋆-algebra), and this allows us to derive an instance of StarOrderedRing C(α, R) under appropriate hypotheses. In order for this to work on ℝ≥0, we actually must force our square root function to be defined on and well-behaved for pairs x : R × R with x.1 ≤ x.2.

• sqrt : R × R → R

  sqrt (a, b) returns a value s such that b = a + s * s when a ≤ b.

• continuousOn_sqrt : ContinuousOn ContinuousSqrt.sqrt {x : R × R | x.1 ≤ x.2}
• sqrt_nonneg (x : R × R) : x.1 ≤ x.2 → 0 ≤ ContinuousSqrt.sqrt x
• sqrt_mul_sqrt (x : R × R) : x.1 ≤ x.2 → x.2 = x.1 + ContinuousSqrt.sqrt x * ContinuousSqrt.sqrt x

instance ContinuousMap.instStarOrderedRingOfContinuousSqrt {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [PartialOrder R] [NonUnitalSemiring R] [StarRing R] [StarOrderedRing R] [TopologicalSpace R] [ContinuousStar R] [IsTopologicalSemiring R] [ContinuousSqrt R] : StarOrderedRing C(α, R)

instance ContinuousMapZero.instStarOrderedRing {α : Type u_1} [TopologicalSpace α] [Zero α] {R : Type u_2} [TopologicalSpace R] [CommSemiring R] [PartialOrder R] [NoZeroDivisors R] [StarRing R] [StarOrderedRing R] [IsTopologicalSemiring R] [ContinuousStar R] [StarOrderedRing C(α, R)] : StarOrderedRing (ContinuousMapZero α R)