!4#4871 positive elements in a star ordered ring

Stream: maths

[Jireh Loreaux]

Note: this is a new feature PR, not a porting PR. I couldn't help myself. This is what I want to use as the primary definition of positive elements @Frédéric Dupuis, @Heather Macbeth, @Eric Wieser (ping whoever else you wish to see this) in a C⋆-algebra (unital or non-unital) and for bounded linear operators on a Hilbert space. Of course, one can define whatever ≤ they want on a type.

def positive (R : Type u) [NonUnitalSemiring R] [PartialOrder R] [StarOrderedRing R] :
    AddSubmonoid R :=
  AddSubmonoid.closure (Set.range fun s : R => star s * s)

[Eric Wieser]

!4#4871 for mobile

[Jireh Loreaux]

@Moritz Doll , @Anatole Dedecker

[Eric Wieser]

Is there a reason not to define it with the carrier defeq to 0 ≤ x?

[Eric Wieser]

That way it doesn't need to assume a star structure at all

[Eric Wieser]

And surely it should be nonneg not positive!

[Eric Wieser]

I guess it holds more generally for whenever docs#add_nonneg does

[Anatole Dedecker]

Eric Wieser said:

Is there a reason not to define it with the carrier defeq to 0 ≤ x?

The point is that in this context you go the other way around: you define a \le b as 0 \le b - a
EDIT: I had missed the StarOrderedRing assumption

[Eric Wieser]

Right, but the two are equivalent anyway with star_ordered_ring; but my suggestion holds much more generally

[Jireh Loreaux]

Eric, you would still need CovariantClass to make it an AddSubmonoid.

[Jireh Loreaux]

And see my note about the naming in the PR comment.

[Eric Wieser]

The current definition doesn't use StarOrderedRing at all, right? Star alone would be enough.

[Eric Wieser]

Maybe docs#add_submonoid.nonneg already exists?

[Notification Bot]

This topic was moved here from #mathlib4 > !4#4871 positive elements in a star ordered ring by Heather Macbeth.

[Jireh Loreaux]

Sure, for the current definition Star is enough.

[Eric Wieser]

Independent of your motivation, I think we should have:

def add_submonoid.nonneg (M) [ordered_add_comm_monoid M] : submonoid M :=
{ carrier := { m | 0 ≤ m },
  add_mem := add_nonneg,
  zero_mem := le_rfl }

[Eric Wieser]

And then the question is "do we need a propositionally equal special case?"

[Eric Wieser]

Heck, we already have most of this in the stuff we use to set up nnreal

[Eric Wieser]

(docs#nonneg.semiring?)

[Jireh Loreaux]

I don't care much what the carrier is definitionally, so 0 \le x is fine.

[Jireh Loreaux]

This is what you want: docs#nonneg.ordered_add_comm_monoid

[Jireh Loreaux]

Okay, I could use that as the definition.

[Moritz Doll]

We should definitively only use Star, reason being that the unbounded operators only satisfy Star and not much else (StarModule also is true), but nevertheless the self-adjoint elements E →.ₗ[R] E are exactly the self-adjoint elements in Star (E →.ₗ[R] E), therefore we can get away with one positivity condition in all cases.

[Moritz Doll]

ah crap, this still does not work because we probably don't have NonUnitalSemiring (we haven't defined addition and multiplication, but there are sensible candidates by restricting the domains so that everything is defined)

[Moritz Doll]

for instance 0 * a = 0 is not true because the domain of a is in general not the whole space

[Moritz Doll]

so we definitively need both IsPositive and positive (and the later is only useful for bounded operators/C^* stuff)

[Jireh Loreaux]

Moritz, you could get away with having an 'OrderedAddCommGroup` though right?

[Jireh Loreaux]

We can avoid multiplication in the definition that way.

[Damiano Testa]

Regarding naming, related to Hilbert's 17th problem, there is a coincidence of sums of squares and totally positive elements. However, searching with Google "totally positive" suggests that this is something that is not so widespread as a concept.

[Jireh Loreaux]

I've pushed some changes, including a refactor to make the carrier { x : R | 0 ≤ x } and weakening the type class assumptions (@Eric Wieser). I generalized a few lemmas about Nat.cast so that they apply to StarOrderedRings, as well as the selfAdjoint and positive parts thereof. Now, for example, with [Ring R] [StarOrderedRing R] [PartialOrder R] we get strictMono (Nat.cast ℕ → positive R) from Nat.strictMono_cast for free.

[Yaël Dillies]

Eric Wieser said:

Independent of your motivation, I think we should have:

def add_submonoid.nonneg (M) [ordered_add_comm_monoid M] : submonoid M :=
{ carrier := { m | 0 ≤ m },
  add_mem := add_nonneg,
  zero_mem := le_rfl }

Has this ever been added?

[Jireh Loreaux]

It's in the PR, but that PR is not merged.