# 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.

source
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

Instances

source
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)
source
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)