approximate units

Stream: maths

[Jireh Loreaux]

Approximate units (multiplicative) are absolutely essential in the theory of $C^*$-algebras. In this case, one often considers approximate units consisting only of positive contractions. However, this is too restrictive for a general definition, even if we will want to restrict to that later. So, what is the right generality for this? A first attempt (is my translation from nets to filters correct?):

import topology.basic

open filter
open_locale topological_space

structure approximate_unit {ι M : Type*} [has_mul M] [topological_space M] [preorder ι]
  [ne_bot (at_top : filter ι)] :=
(to_fun : ι → M)
(tendsto_mul_left_self : ∀ m : M, tendsto (λ i, to_fun i * m) at_top (𝓝 m))
(tendsto_mul_right_self : ∀ m : M, tendsto (λ i, m * to_fun i) at_top (𝓝 m))

[Antoine Chambert-Loir]

Exactly, the right formulation is in terms of filters of subsets. This is a screen capture from page 120 of Bourbaki, Théories spectrales, chapter 1, §6, no. 10, 2nd edition, Springer, 2019. DOI:10.1007/978-3-030-14064-9.

image.png

[Patrick Massot]

What does "sur la boule unité de A" means here?

[Patrick Massot]

I missed Jireh's earlier message. Jireh, this cannot be the correct translation.

[Patrick Massot]

Antoine, is this meant to mean that F has a basis whose elements are contained in the unit ball?

[Antoine Chambert-Loir]

I think so, yes.

[Antoine Chambert-Loir]

(I'm not sure Bourbaki is consistent with his own terminology here…)

[Antoine Chambert-Loir]

It means that the members of F are subsets of the unit ball (for all S \in F, and all a \in S, || a || <= 1).
And F is increasing if the members of F are subsets of the positive cone (for all S \in F, and all a \in S, a is positive).

[Jireh Loreaux]

But surely we want something more general, right? As in, something that would also apply to mollifiers where we might not have a norm? Bourbaki's definition is what I'm familiar with (albeit phrased in terms of nets instead of filter bases), but I think it's not quite general enough.

[Antoine Chambert-Loir]

You would want an efficient definition of an approximate unit in a topological algebra (without one)? One question, then, is to ask whether one needs some boundedness condition on the filter (which would be automatic in some contexts, via Banach's theorem).

[Jireh Loreaux]

I don't see any reason to explicitly require a boundedness condition. It's also not clear why we want to restrict to an algebra (or even a ring), even if that's the most common use case. For example, if you throw a @[to_additive] on my definition above then you could have an approximate additive unit on the type of positive reals. I'm not saying that particular thing would be terribly useful, only that it exists and there might be other cases where it would be. (Note: it's fine if the type in question has an actual unit because then you can make an approximate unit by taking the constant net, or the principal filter)

There will be plenty of specializations of this concept. For example, even within $C^*$-algebra theory, approximate units are always taken to be bounded and consisting of positive elements, but one would also like to consider approximate units which are quasicentral, or sequential, or consisting of projections, or any combination thereof.

@Patrick Massot what exactly is wrong with the definition I suggested?

[Antoine Chambert-Loir]

I see. You might generalize and consider approximate units for has_scalar types on something which has topology.
Also, it might be more natural to consider the approximate unit as a filter on M (with your notation) rather than as a filter on something else. Additional conditions can be imposed by requiring the filter to have basis of a particular type.

import topology.basic

open filter
open_locale topological_space

structure approximate_unit {α M : Type*} [has_scalar α M] [topological_space M] extends filter α :=
(tendsto_one : ∀ (m : M), tendsto (λ (a : α), a • m) to_filter (𝓝 m))

[Jireh Loreaux]

I'm not sure about has_scalar besides the trivial case of multiplication, but the existence of a filter basis idea was the thing I was missing. I guess we just avoid meaningless statements by requiring the filter is ne_bot?

[Antoine Chambert-Loir]

Well, you could want an approximate unit for an asymmetrical convolution $L^p \times L^q \to L^r$, hence in more general contexts : \alpha \to \beta \to \gamma .

Nets and filters are basically equivalent notions, but the former is inspired by sequences and forces to think in terms of maps from an ordered set; the second is more static but the ordered set is set set of subsets of the ambient set, with inclusion (reversed). An ordered set gives rise to a filter, called the filter of sections (its elements are subsets of \iota that contain all elements larger than some a : \iota), and a map between to sets allows you to push/pull back filters (take the filter generated by images, resp preimages).

[Antoine Chambert-Loir]

(How do you guys type greek/unicode in your web browser? Please teach me!)

[Jireh Loreaux]

I have Gabriel Ebner's https://github.com/gebner/m17n-lean installed using ibus.

[Jireh Loreaux]

It's nice to have system-wide Lean-style unicode input. I use it for writing emails all the time now.

[Jireh Loreaux]

Right, I realize that nets and filters are basically equivalent. I hadn't considered those even more general setting, but then even has_scalar wouldn't be sufficient, right? Or am I missing something?

[Jireh Loreaux]

Actually, I'm not even sure what an approximate unit α → β → γ would even mean?

[Antoine Chambert-Loir]

I was typing the definition, until the very tendsto which made me realize it means nothing unless β = γ, sorry…

[Patrick Massot]

Jireh, if you need Lean-friendly information about filters, there is a draft of Mathematics in Lean section at https://www.imo.universite-paris-saclay.fr/~pmassot/mil/07_Topology.html