Commit 2023-06-07 16:34 31c24aa7

feat(algebra/star/basic): refactor star_ordered_ring to include add_submonoid.closure (#18854) Per Zulip, this refactors star_ordered_ring so that the condition star_ordered_ring.nonneg_iff is changed from ∀ r : R, 0 ≤ r ↔ ∃ s, r = star s * s to something morally equivalent to ∀ x : R, 0 ≤ x ↔ x ∈ add_submonoid.closure (set.range (λ s : R, star s * s)). In fact, we actually change the structure field nonneg_iff to le_iff, which characterizes · ≤ · instead of just 0 ≤ ·. When R is a non_unital_ring, there is effectively no change (see how we recover star_ordered_ring.nonneg_iff and also star_ordered_ring.of_nonneg_iff), but it gives a more useful and sensible condition when R is only a non_unital_semiring. For instance, now conjugate_le_conjugate holds for non_unital_semiring. There are essentially two reasons for this change.

1. It would be nice if things like ℚ could be star_ordered_rings. This is a minor reason, but it should be a nice convenience. This instance is added in this PR in a new file.
2. Much more importantly, we want to declare the positive elements in a star_ordered_ring as an add_submonoid, but to accomplish this with the previous definition requires much more stringent type class assumptions (e.g., C⋆-algebras) and sophisticated machinery (the continuous functional calculus) in order to show that the sum of positive elements is positive. This change essentially allows us to defer that proof obligation to the settings where it will matter that a positive element really does have the form star s * s. We remark that even for C⋆-algebras, the fact that the sum of positive elements (i.e., those of the form star s * s) is positive is a deep result which was first shown in 1952 by Fukamiya, and then again in 1953 by Kelley and Vaught. These proofs are in essence very similar, but the latter is more aesthetically pleasing, and it is this proof that appears in all the textbooks. I went looking and did not see another proof anywhere in the literature. We provide a few convenience constructors for star_ordered_ring in the form of reducible definitions which can apply when R is either a non_unital_ring (so we only need to characterize nonnegativity), and / or when positive elements have exactly the form star s * s. In this way, we can effectively maintain the status quo (see the instances for real and complex).