Exponentials in seminormed algebras

Stream: maths

[Eric Wieser]

I'm trying to show that for docs#dual_number s (aka docs#triv_sq_zero_ext), $\operatorname{exp}(x+y\varepsilon) =\operatorname{exp}(x) + (y\operatorname{exp}(x) )\varepsilon$.
I'm able to show that

has_sum (λ n, exp_series S (tsze R M) n (λ _, x)) (inl a + a • inr x.snd)

but I'm not sure how to show that this sum is unique.

I'm able to equate the first components thanks to the projection of the first component being continuous, but I'm not sure how to proceed for the second component since:

• t2_space (tsze R M) doesn't hold
• normed_ring (tsze R M) doesn't hold
• I don't have any topology available on M!

Could someone take a look at #18200 and advise how I might prove snd (exp S x) = exp S x.fst • x.snd; or whether it's even true?

[Eric Wieser]

My guess would be that it's false because my topology is too coarse; but as understand it, if I make my topology finer I would need to choose a different norm

[Jireh Loreaux]

I have only glanced at this briefly, but if I understand correctly, your topology is just induced by the projection onto the first coordinate (i.e., R). So anything which converges to (r,m) also converges to (r,m') for any m' : M. Therefore, this sum is not unique. Consequently, you won't be able to show the specified equality, because docs#formal_multilinear_series.sum is just classical.some applied to summable (which is just an existential wrapper around has_sum).

And yes, if you need to change the topology, then you need to change the norm too. I also don't see how you have much hope of this at all if you don't have some topology on M itself.

[Eric Wieser]

I think I'm concluding that the norm $\|x + y\varepsilon\| = \|x\|$, while perhaps natural, does not produce a desirable topology

[Jireh Loreaux]

I mean, it's not Hausdorff, so limits won't be unique.

[Jireh Loreaux]

Note that norms on objects like these can be a bit subtle. For example, docs#unitization is similar in many ways to docs#triv_sq_zero_ext, and the "best" norm on unitization (not in mathlib, but I have stuff locally for it) is kind of tricky. For example, a natural first choice would be the ℓ¹ norm (sum of the norms of the coordinates), but that norm doesn't preserve the C⋆-property when the original non-unital ring had it. Instead, the right thing to do in that situation is to take the max of (the norm of the left-regular representation of the unitization acting on the non-unital underlying algebra) and (the norm of the scalar part).

[Jireh Loreaux]

Do you have any actual example of a triv_sq_zero_ext where the topology isn't the product topology? It's a bit strange that you would want to topologize tsze R M without a topology on both R and M. (Note: the topology induced by the norm I described on the unitization above is the product topology, not definitionally, but that can be fixed with forgetful inheritance)

[Eric Wieser]

I've concluded that I probably do just want the product topology

[Eric Wieser]

And was led astray by the norm suggested by https://math.stackexchange.com/a/1056378/1896

[Eric Wieser]

I've updated the PR to use the product topology and everything works nicely. Perhaps I'll wait for you to push your unitization work before attempting to define a norm! As it turned out I didn't need it anyway.

[Eric Rodriguez]

Eric Wieser said:

And was led astray by the norm suggested by https://math.stackexchange.com/a/1056378/1896

Is it worth leaving a comment there pointing this out? They seem to just assume the convergence of the exponential and call it a day

[Eric Wieser]

I think someone more versed in convergence than I am should leave that comment

[Kevin Buzzard]

convergence is not a well-behaved property in non-Hausdorff spaces.

[Jireh Loreaux]

Note: it's not that the series doesn't converge to the stated value (it does, with the seminorm specified in the post), it's just that it also converges to a bunch of other random things; this is a problem for us because our definition of the sum uses classical.some to choose an arbitrary one of those, but I suspect it's not much of a problem for people working with dual numbers in practice.

[Eric Wieser]

Is "one of the things f x converges to is y so I'm going to use y" even valid in informal mathematics?

[Eric Wieser]

It feels like the problem is still there, and if it works informally presumably it's because implicitly a different norm/topology was being used to take the limit?

[Jireh Loreaux]

1. If you have a way of specifying y other than "the thing f converges to along some filter", then sure (because you can take this other thing to be the definition). I think in this situation that's likely exactly what happens.
2. I think here it's just convenient to motivate / explain the definition of the exponential by using the sum of the series for parallelism with more familiar exponentials. Moreover, (a) it actually works if you use the product topology, and (b) the topology induced by the seminorm is weaker than the product topology, so the series still converges to the claimed value even though it's no longer a unique limit.

[Eric Wieser]

Ah, so the formal version of 1) would be a typeclass with an exp field and a exp_lawful : has_sum (the_usual_series) exp proof?

[Eric Wieser]

Eric Rodriguez said:

Eric Wieser said:

And was led astray by the norm suggested by https://math.stackexchange.com/a/1056378/1896

Is it worth leaving a comment there pointing this out? They seem to just assume the convergence of the exponential and call it a day

I added a comment

[Jireh Loreaux]

yes, that could be a formalization of it, but I don't think it's really that necessary. Again, I think the series formulation is primarily there for motivation and parallelism.

[Jireh Loreaux]

Eric Wieser said:

Perhaps I'll wait for you to push your unitization work before attempting to define a norm! As it turned out I didn't need it anyway.

Just in case it matters to you @Eric Wieser, I wasn't planning on pushing this until after the port is finished.

[Eric Wieser]

Any particular reason?

[Eric Wieser]

I'd be keen to see the approach, even if you ultimately don't have time to polish it for a PR

[Jireh Loreaux]

Mainly just to avoid creating extra mathlib3 burden, but I can push to a branch. I'll take a few minutes to clean it up and push to a branch. I didn't actually implement the forgetful inheritance for the topological structure yet.

[Jireh Loreaux]

@Eric Wieser branch#j-loreaux/cstar-unitization contains my implementation of the C⋆-norm on the unitization. I did end up implementing the forgetful inheritance for the uniform_space structure (it greatly simplifies the proof of completeness anyway; otherwise it's a bit of a pain). It's still a bit messy, but I suspect you'll be able to follow it without too much trouble.

One note: I realized that this norm is actually not quite as nice as I had remembered when the underlying algebra is not a C⋆-algebra. The reason is that it's only a seminorm unless the left regular representation of the algebra is injective (it often is, but that's a separate proof obligation). This condition is automatic for C⋆-algebras because of the C⋆-property.

[Eric Wieser]

If the norm is only a seminorm, doesn't that make it incompatible with the product topology? (Edit: I see now that this is about the product topology on (𝕜 × (A →L[𝕜] A), so they're compatible)

[Reid Barton]

I think the SE is making an unjustified assumption that norms that are good for algebra are always also good for topology.

[Eric Wieser]

Is mathlib also making that unjustified assumption in your opinion?

[Reid Barton]

I'm not sure what that question means

[Reid Barton]

but I would guess not

[Reid Barton]

Like, in general the algebraic norm $N_{L/K}(a)$ of an element of a field extension $K \subseteq L$ isn't a real number in the first place--it's an element of $K$.

[Reid Barton]

So really there are two different meanings of "norm" involved.

[Eric Wieser]

Reid Barton said:

I'm not sure what that question means

The way that normed_space derives from topological_space means you can't implement an algebraic norm without having the associated topology forced upon you. Maybe the answer is that norm is not for algebraic norms.

[Reid Barton]

Certainly not, if it always takes values in real.

[Eric Wieser]

Is there a good reason that a topological norm should always take values in real?

[Reid Barton]

Well it had better at least take values in something ordered

[Kevin Buzzard]

For algebraic norms we have "valuation", taking values in an arbitrary totally ordered commutative additive group with 0.

[Kevin Buzzard]

Oh but this does not apply to norms for finite extensions of fields.

[Jireh Loreaux]

Eric Wieser said:

If the norm is only a seminorm, doesn't that make it incompatible with the product topology? (Edit: I see now that this is about the product topology on (𝕜 × (A →L[𝕜] A), so they're compatible)

No, we're trying to put a norm on unitization 𝕜 A := 𝕜 × A. We do this by pulling back the norm on 𝕜 × (A →L[𝕜] A) via the map ((k, a) : unitization 𝕜 A) ↦ (k, algebra_map 𝕜 (A →L[𝕜] A) k + continuous_linear_map.mul 𝕜 A a). Note that (0, a) ↦ (0, continuous_linear_map.mul 𝕜 A a), so, if continuous_linear_map.mul 𝕜 A is not injective, then we only end up with a seminorm on unitization 𝕜 A.

That being said, it's a bit unusual for continuous_linear_map.mul 𝕜 A to fail to be injective, but it is possible. For instance, take A to be the (non-unital) algebra of strictly upper triangular 2 × 2 matrices. Note that the product of any two elements of this algebra is 0, so in fact continuous_linear_map.mul 𝕜 A = 0, and hence the induced norm on the unitization simplifies to: ‖(k, a)‖ = ‖k‖ (so this does not induce the product topology).

[Jireh Loreaux]

Note: C⋆-norms on a specified algebra are unique, if they exist, so as far as C⋆-algebras are concerned, there really isn't another choice for the norm. This may necessitate another type synonym if we want to put this norm on the unitization of C⋆-algebras and another norm on the unitization of other Banach algebras.

[Eric Wieser]

there really isn't another choice for the norm

Presumably it's possible that there's another definition that's equal to your definition in the C* case, but still produces the product topology in the more general case?

[Jireh Loreaux]

I'm not so sure about that. I think it's unlikely. It seems that in the literature there is focus on so-called regular norms, which I think are norms for which continuous_linear_map.mul is an isometry.

[Kevin Buzzard]

In the p-adic theory when you have non-reduced affinoids you frequently get Banach spaces equipped with a so-called supremum seminorm which does not induce the Banach space topology.

[Jireh Loreaux]

For reference, the papers I saw on this subject were norms on unitizations of banach algebras and a follow-up paper norms on unitizations of banach algebras revisited.

In case you see this stack exchange question, just realize that several things in the question and in the accepted answer are wrong (I need to add a comment to this effect). Basically, the OP claims that the supremum gives you a norm, but this is incorrect even in the C⋆-algebra case unless the algebra is actually not unital (i.e., there is no identity, having one that we forgot about is not allowed). And when it's not a C⋆-algebra I showed earlier in the thread how it can even be the zero function. The answrt is incorrect because it's assuming you actually get Banach spaces from both these "norms" (for ‖⬝‖₁ this is correct), however, when that actually happens (e.g., when the norm on A is regular) then the rest of the answer is valid, and the subject of investigation in the papers above is the minimal constant c you can get (apparently c=3 is optimal).