Normal elements of a star monoid: type class or not?

Stream: maths

[Frédéric Dupuis]

The PR #11991 defines normal elements of a star monoid, i.e. those elements x that commute with star x, and we are currently debating whether this should be a type class or not.

Right now in the PR it is written as the type class [is_star_normal x], loosely modelled after docs#filter.ne_bot and docs#invertible. While this approach is somewhat unusual for mathlib, I think it's the way to go: there are a lot of results that will need this condition, and carrying around a proof that an element is normal will be rather painful (for example, the continuous functional calculus, which lets us apply a function f : ℂ → ℂ to elements of a C⋆-algebra, only works for normal elements). Also, there is a relatively restricted set of instances that should be enough for most purposes: self-adjoint, unitary, and skew-adjoint elements are normal, zero and one are normal, and this already gets us pretty far.

However, this style is still relatively uncommon for mathlib and it would be nice to have some input here about this before going ahead. I think it would be nice in particular to hear from the authors of docs#filter.ne_bot (git blame tells me this might be @Yury G. Kudryashov or @Mario Carneiro ...?) Are there any issues with this type class?

[Mario Carneiro]

I'm not convinced. Your examples don't sound like structural operations (besides 0 and 1): are adjoint, unitary and skew-adjoint also typeclasses here? I don't really follow your example of the continuous functional calculus well enough to say how prevalent the assumption would be if you just had to pass it as a regular assumption (h : is_star_normal x). Another option is to have a sub-something of star-normal elements, like we do for the centralizer and other subgroups

[Yaël Dillies]

See for example docs#topological_space.nonempty_compacts and docs#emetric.nonempty_compacts.emetric_space

[Frédéric Dupuis]

Mario Carneiro said:

I don't really follow your example of the continuous functional calculus well enough to say how prevalent the assumption would be if you just had to pass it as a regular assumption (h : is_star_normal x).

Basically, suppose I have a unitary $U$ and I want to apply some function $f : ℂ → ℂ$, to it, I would really prefer to be able to write f U instead of f U.is_star_normal U. The other option I could see would be to define f U to be some garbage value if U is not normal, but this would make most lemmas require an extra parameter as well.

Another option is to have a sub-something of star-normal elements, like we do for the centralizer and other subgroups

I don't think this would buy us much, since normal elements don't really have much structure. It's not a group or anything like that, so we would only have it as a subtype.

[Frédéric Dupuis]

Self-adjoint, unitary, and skew-adjoint are not type classes, they're (additive) subgroups. I don't really get your point about structural operations -- what do you mean by that exactly?

[Mario Carneiro]

Frédéric Dupuis said:

Basically, suppose I have a unitary $U$ and I want to apply some function $f : ℂ → ℂ$, to it, I would really prefer to be able to write f U instead of f U.is_star_normal U. The other option I could see would be to define f U to be some garbage value if U is not normal, but this would make most lemmas.

Yes, make f U a garbage value, this is the usual approach

[Mario Carneiro]

I don't think this would buy us much, since normal elements don't really have much structure. It's not a group or anything like that, so we would only have it as a subtype.

Okay, then a plain hypothesis sounds best

[Mario Carneiro]

Self-adjoint, unitary, and skew-adjoint are not type classes, they're (additive) subgroups. I don't really get your point about structural operations -- what do you mean by that exactly?

Typeclasses work best when you have lots of structural operations which you want to deduce a property about. For example, maybe I have a class is_real on complex numbers, with instances like is_real 0, [is_real x] [is_real y] : is_real (x + y), [is_real x] : is_real (conj x) and so on. You get a mini-grammar of all the operations you can put together to get real numbers, and it would be annoying to build up these proofs following the structure of the expression all the time. If there are no such structural operations, then typeclass inference is basically just a glorified assumption tactic, and passing the argument by any other way (e.g. by direct proof) becomes cumbersome.

[Eric Wieser]

I don't think in practice mathlib uses is_real-like typeclasses, even though such a design _could_ work. Certainly we used to use something like that for subobjects (is_add_submonoid), but moved away from that choice.

[Eric Wieser]

invertible is special because it's intended to provide notation

[Eric Rodriguez]

docs#ne_zero, but maybe this should not be used anymore ;b

[Frédéric Dupuis]

I see. Maybe another option would be to actually write a glorified assumption tactic for this and use an autoparam. The thing is, in practice plain normal elements don't show up that often, almost all the time it's either a self-adjoint, or unitary, or something like that.

[Eric Wieser]

Is the design behind measurable and continuous and the respective tactic#measurability (doc#tactic.interactive.measurability) and tactic#continuity (docs#tactic.interactive.continuity) relevant here?

[Frédéric Dupuis]

Eric Wieser said:

Is the design behind measurable and continuous and the respective tactic#measurability (doc#tactic.interactive.measurability) and tactic#continuity (docs#tactic.interactive.continuity) relevant here?

Right, I guess the "glorified assumption tactic" approach would be something like that.

[Sebastien Gouezel]

IMHO, a typeclass is the way to go here, to make sure it is automatically filled for elements of the unitary subgroup, of the self-adjoint subgroup, and the anti-self-adjoint subgroup. I mean, for any element of these subgroups, its coercion to an operator would automatically get the typeclass. And this should cover like 99.9% of uses, so I don't mind if it's a little bit cumbersome to use in the remaining 0.1% cases.

[Jireh Loreaux]

Just to add another thing to the list: any element in a *-subalgebra generated by a normal element will be normal.

[Eric Wieser]

@Sebastien Gouezel, is the case you're describing [is_star_normal X] (x : X) instead of (x : X) [is_star_normal x]? The former would be enough to handle the various subtypes of the elements you mention

[Frédéric Dupuis]

Eric Wieser said:

Sebastien Gouezel, is the case you're describing [is_star_normal X] (x : X) instead of (x : X) [is_star_normal x]? The former would be enough to handle the various subtypes of the elements you mention

Presumably the latter -- if the issue is that using a type class would make it cumbersome to provide the proof manually if needed, the former option would make it literally impossible.

[Jireh Loreaux]

I thought he was describing this:

instance (x : self_adjoint X) : is_star_normal x := sorry

[Reid Barton]

What about just using a subtype? you can create coercions to the subtype and has_zero, has_one instances

[Frédéric Dupuis]

Reid Barton said:

What about just using a subtype? you can create coercions to the subtype and has_zero, has_one instances

My guess is that this would require a lot of type annotations when trying to use the coercion to go from, say, x : self_adjoint E into star_normal E. I haven't actually tried it, but this feels like there will be a lot of star_normal ?m1 going on.

[Frédéric Dupuis]

I just confirmed this fear:

def star_normal [has_mul R] [has_star R] := {x : R // commute (star x) x}

instance : has_coe (self_adjoint R) (star_normal R) :=
⟨λ x, ⟨x, by simp [star_coe_eq]⟩⟩

def foo (x : star_normal R) : ℕ := 0

example (x : self_adjoint R) : foo x = 0 := rfl    -- Fails: star_normal ?m_1
example (x : self_adjoint R) : foo (x : star_normal R) = 0 := rfl    -- works

[Sebastien Gouezel]

Jireh Loreaux said:

I thought he was describing this:

instance (x : self_adjoint X) : is_star_normal x := sorry

Yes, I was thinking of this. With the other option, if you declare a typeclass for subgroups, say, then I don't see how to define the functional calculus on a normal element (i.e., write down the definition of f x when x is star-normal) in terms of this typeclass.

[Sebastien Gouezel]

All the other options that have been mentioned up to now (explicit assumption, or subtypes and coercions) would probably work, but as far as I can tell they would be strictly less convenient in most situations.