upper hemicontinuity vs. upper semicontinuity

Stream: maths

[Jireh Loreaux]

There is a standard fact in the theory of complex Banach algebras: the spectrum is upper hemicontinuous (although sometimes in the literature on this subject it is also called upper semicontinuous). I just assumed that it should be possible to unify this with our current definition of docs#UpperSemicontinuous, which would give us access to all that API, but as it stands it is not quite so easy.

[Jireh Loreaux]

For reference:

def UpperSemicontinuousAt {α : Type*} [TopologicalSpace α]
    {β : Type*} [Preorder β] (f : α → β) (x : α) : Prop :=
  ∀ (y : β), f x < y → ∀ᶠ (x' : α) in nhds x, f x' < y

[Jireh Loreaux]

The definition of f : α → Set γbeing upper hemicontinuous at a : α is that for every open set u with f a ⊆ u, there is a neighborhood v ∈ 𝓝 a such that for every x ∈ v, f x ⊆ u. Or, in the language of filters (this definition does not currently exist in Mathlib):

UpperHemicontinuousAt (f : α → Set γ) (a : α) := ∀ u : Set γ, u ∈ nhdsSet (f a) → ∀ᶠ (x : α) in 𝓝 a, u ∈ nhdsSet (f x)

[Jireh Loreaux]

And now you can see the similarity with the definition of upper semicontinuity (by choosing β := Set γ and (s < t) := (t ∈ nhdsSet s)). However, there are two problems with this.

1. t ∈ nhdsSet s is definitely not the LT instance on Set γ
2. t ∈ nhdsSet s doesn't correspond to the < for some Preorder on Set γ as it's not irreflexive (since u ∈ nhdsSet u if u is open).

[Jireh Loreaux]

There is one way to deal with the fact that it doesn't correspond to a Preorder: bundle spectrum ℂ into a function from the complex Banach algebra A to docs#TopologicalSpace.NonemptyCompacts (here you need to assume [Nontrivial A] which is annoying), and then for t s : NonemptyCompacts ℂ, the relation (t : Set ℂ) ∈ nhdsSet (s : Set ℂ) is irreflexive, and so corresponds to the < of a Preorder. However, NonemptyCompacts already has an ordering, and it's just the pullback from the coercion to Set ℂ. So, (a) this only partially solves the problem, and (b) it still doesn't allow us to talk about hemicontinuity as semicontinuity more generally.

[Jireh Loreaux]

Therefore, I wonder if we might replace the definition of UpperSemicontinuousAt (and friends) with:

def UpperSemicontinuousAt {α : Type*} [TopologicalSpace α]
    {β : Type*} (r : β → β → Prop) [hr : IsTrans r] (f : α → β) (x : α) : Prop :=
  ∀ (y : β), r (f x) y → ∀ᶠ (x' : α) in nhds x, r (f x') y

I'm interested to hear comments on this. Another possibility would be to define UpperSemicontinuousAtWith as this more general version, and then let UpperSemicontinuousAt be an abbrev for this with r instantiated as < and assuming a Preorder β.

[Jireh Loreaux]

Of course, I could just define UpperHemicontinuousAt, but duplicating API makes me :mad: and :cry:

[Mario Carneiro]

is it even "upper" anymore at that point? Presumably lower semicontinuous just uses > instead of <

[Mario Carneiro]

I was also thinking you could merge r and f into one relational argument r' x y = r (f x) y, since they don't appear separately

[Jireh Loreaux]

fair point, we should remove the Upper in the name in that case.

[Jireh Loreaux]

I think you don't want to merge r and f, because I think you still want to know that r itself is transitive, otherwise I suspect it will be relatively useless.

[Mario Carneiro]

is knowing r is transitive but f is not monotone good for anything?

[Mario Carneiro]

it might be worth doing some reverse math on theorems using this assumption

[Jireh Loreaux]

I mean, f := spectrum ℂ is certainly not monotone in any sense, so the answer to your question is definitely "yes"

[Jireh Loreaux]

Many Banach algebra don't even have an ordering, and the ones that do (e.g., C⋆-algebras) don't make spectrum ℂ monotone.

[Mario Carneiro]

in that case, it seems the useful application of transitivity in this context is r (f x) y -> r y z -> r (f x) z, and the equivalent of that for r' is r' x y -> r' x z (or \forall x, r' x y -> r' x z) viewed as an inequality relation between y and z

[Mario Carneiro]

(which is, incidentally, transitive for any r')

[Jireh Loreaux]

Well, here's the other half of this: if I'm going to make this generalization, I want to make it as seamless as possible for the existing use case, which is Preorder β. Writing SemicontinuousAtWith (· < ·) f, while a bit annoying, wouldn't be nearly as bad as SemicontinuousAtWith (· < ·) (stupid term proving ∀ x, r' x y → r' x z) f. I guess if it's an abbrev, then maybe it's okay, but it's not my favorite thing unless we have yet another use case.

[Mario Carneiro]

I don't think the stupid term needs to be part of the definition, it would just be SemicontinuousAtWith (f · < ·)

[Jireh Loreaux]

aha, I see.

[Mario Carneiro]

you would use the term when applying a theorem that actually uses transitivity in some way

[Antoine Chambert-Loir]

@Anatole Dedecker and I had a discussion about this because we need a lot of semicontinuity for our proof of the von Neumann minimax theorem (Sion's theorem, actually), all of which I can remember is that mathlib's definition of semicontinuity is not the good one (only valid for real numbers) and that a naive extension (for nonlinear orders) is ridiculously uninteresting.

[Antoine Chambert-Loir]

Still, the thread is there: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Semicontinuity.20definition.20for.20non-linear.20orders/near/432898278