Is the zero algebra normed?

Stream: maths

[Eric Wieser]

This got lost in the #rss stream:

rss-bot said:

feat(analysis/normed_space/basic): pi and prod are normed_algebras (mathlib#13442)

Note that over an empty index type, pi is not a normed_algebra since it is trivial as a ring.

Authored-by: eric-wieser (commit)

@Reid Barton said:

The zero algebra isn't normed? Looks odd from the viewpoint of algebra or geometry. I found a few references saying that $C(X)$ is a normed (unital) algebra for $X$ compact, even when (on the same page nearly) they claim to require $||1|| = 1$

(referring to docs#pi.normed_algebra)

[Kevin Buzzard]

IIRC in Bosch-Guentzer-Remmert they require ||1||<=1 and go on to prove that either 1=0 or ||1||=1.

[Kevin Buzzard]

Oh I'm slightly off. The axioms for a seminormed ring in BGR are |xy|<=|x||y| and |1|<=1, and then they instantly observe that because |1|<=|1|^2<=|1| either |1|=1 or |1|=0 and in the latter case |x|=0 for all x. And a norm is just a seminorm with |x|=0 iff x=0, so the zero ring is a normed ring in the sense of BGR.

[Eric Wieser]

Mathlib agrees that the zero ring is a normed_ring (docs#pi.normed_ring has no nonemptiness requirement)

[Reid Barton]

The BGR axioms make sense to me. However I note that docs#normed_ring doesn't seem to require ||1|| <= 1 and I'm not sure whether this is intentional.

[Reid Barton]

If the zero ring is a normed ring then I think it really doesn't make sense to not allow it as a normed algebra.

[Eric Wieser]

Should we require norm (algebra_map R A r) ≤ norm r instead of the current equality (docs#norm_algebra_map_eq), or is that too weak?

[Reid Barton]

I think the correct way to think about it is $||r a||_A \le ||r||_R \cdot ||a||_A$, which as our algebras are unital, is equivalent to $||r||_A \le ||r||_R$, at least if we add the missing axiom $||1|| \le 1$

[Reid Barton]

i.e. a normed algebra is an algebra that is a docs#normed_space

[Reid Barton]

Except that α should not need to be a normed_field in normed_space

[Eric Wieser]

I've had a go at using norm (algebra_map R A r) ≤ norm r which seem weak enough for my purposes

[Eric Wieser]

I agree that we can do better

[Eric Wieser]

PR'd as #13544, although I suspect CI will complain

[Jireh Loreaux]

I agree that 0 should definitely be a normed_algebra. However, I also care a great deal about the case of non-unital algebras. In that case, the correct condition should I think be $||r a||_A = ||r||_R \cdot ||a||_A$ (which, incidentally, also works in the unital case even if it isn't the way we want to phrase it). I guess we don't have anything like this for non-unital algebras in mathlib, right?

[Eric Wieser]

Are you sure you want equality?

[Eric Wieser]

That's the problem that motivated this thread in the first place

[Eric Wieser]

Oh, I guess that's just docs#norm_smul

[Kevin Buzzard]

but norm_smul is about fields. There's a trick with fields where you multiply by r and then by r^{-1} and show that equality is equivalent to <=

[Eric Wieser]

Right, but normed_space only exists for fields at the moment anyway

[Eric Wieser]

@Jireh Loreaux, You can already do non-unital normed algebras with [normed_field α] [non_unital_semi_normed_ring β] [normed_space α β] [is_scalar_tower α β β] [is_scalar_tower α α β]

[Jireh Loreaux]

Ah, right, you get it with normed_space. I knew that and forgot.

[Kevin Buzzard]

and a cunning use of is_scalar_tower by the looks of things

[Eric Wieser]

It's the same cunningness as in the docs#algebra docstring

[Eric Wieser]

Perhaps we should copy that across to normed_algebra's docs

[Jireh Loreaux]

By the way, the equality version I mentioned above works because you include the a. So in the case of the zero ring, both sides are automatically zero.

[Jireh Loreaux]

I think in various sources I've read on Banach algebras, the equality I stated above (essentially docs#norm_smul) is the definition, without the added condition that ∥1∥ ≤ 1. In this case, one gets ∥1∥ ≥ 1 (except for the zero ring) for free because it's a normed ring. Then there are various shenanigans involved to renorm the algebra with an equivalent norm so that ∥1∥ = 1 (except for the zero ring). I'm not claiming this is what we want in mathlib.

[Eric Wieser]

In this case, one gets ∥1∥ ≥ 1 (except for the zero ring) for free

Do we have this lemma anywhere? docs#one_le_norm_one?

[Jireh Loreaux]

in mathlib we have the stronger docs#normed_algebra.norm_one_class because our definition of normed_algebra is stronger than the one I just described.

[Eric Wieser]

I thought you said that ∥1∥ ≥ 1 was a consequence of normed_ring alone?

[Eric Wieser]

(note that #13544 removes docs#normed_algebra.norm_one_class as it is no longer true)

[Jireh Loreaux]

Ah, I see what you mean. Well, I haven't seen that lemma, so maybe we don't have it. Of course you need nontrivial R. The proof is just ∥1∥ = ∥1 * 1∥ ≤ ∥1∥ * ∥1∥, and then cancel a ∥1∥ on both sides because it's positive by nontriviality.

[Jireh Loreaux]

Isn't docs#normed_algebra.norm_one_class still true assuming nontriviality? I thought the only difference in #13544 is that it also the zero ring to be a normed algebra. Or is there a further weakening?

[Reid Barton]

Yes, I think it is still true

[Eric Wieser]

What prevents the norm being 0 everywhere?

[Eric Wieser]

(in a non-trivial ring)

[Eric Wieser]

Ah, never mind

[Jireh Loreaux]

You're probably already changing it, but I think in #13544 because of the above it makes sense to have everything point the opposite direction. That is, nontrivial → norm_one_class, and then add the nontrivial type class everywhere necessary instead of norm_one_class.

[Eric Wieser]

I'm trying to, but I'm struggling to find the right cancellation lemma for "cancel a ∥1∥ on both sides"

[Jireh Loreaux]

docs#le_of_mul_le_mul_left?

[Mauricio Collares]

docs#le_mul_iff_one_le_left

[Eric Wieser]

Wait, I'm still confused what you're suggesting I do here

[Eric Wieser]

As far as I can tell nontrivial does not imply norm_one_class:

lemma norm_one_class.nontrivial (α : Type*) [semi_normed_group α] [has_one α] [norm_one_class α] :
  nontrivial α :=
nontrivial_of_ne 0 1 $ ne_of_apply_ne norm $ by simp

def norm_one_class_iff_nontrivial {α} [normed_ring α] : norm_one_class α ↔ nontrivial α :=
⟨λ h, by { resetI, exact norm_one_class.nontrivial α },
  λ h, ⟨by {
    resetI,
    have := norm_mul_le (1 : α) (1 : α),
    rw [←one_mul ∥(1 * 1 : α)∥, mul_one] at this,
    have : 1 ≤ ∥(1 : α)∥ := le_of_mul_le_mul_right this (norm_pos_iff.mpr one_ne_zero),
    refine le_antisymm _ this,
    show ∥(1 : α)∥ ≤ 1,
    sorry
  }⟩⟩

[Eric Wieser]

Eric Wieser said:

What prevents the norm being 0 everywhere?

Answer: normed_group as opposed to semi_normed_group

[Reid Barton]

Oh yeah if you are missing $||1|| \le 1$ then it doesn't follow.

[Eric Wieser]

I'd be inclined to leave things as is in #13544 then

[Jireh Loreaux]

right, I thought we were adding that hypothesis to the the definition of normed_algebra?

[Reid Barton]

I would kind of prefer to decide on what we actually want and fix it from the bottom up rather than replacing things piecemeal

[Eric Wieser]

Jireh Loreaux said:

right, I thought we were adding that hypothesis to the the definition of normed_algebra?

My proposed change in that PR is

-(norm_algebra_map_eq : ∀x:𝕜, ∥algebra_map 𝕜 𝕜' x∥ = ∥x∥)
+(norm_algebra_map_le : ∀ x, ∥algebra_map 𝕜 𝕜' x∥ ≤ ∥x∥)

The consequence is a handful of lemmas hold more generally on trivial norm structures, and the ones that don't now need to assume [normed_algebra R A] [norm_one_class A]

[Reid Barton]

Jireh Loreaux said:

right, I thought we were adding that hypothesis to the the definition of normed_algebra?

Do you really mean normed_algebra and not normed_ring?

[Eric Wieser]

Reid Barton said:

Oh yeah if you are missing $||1|| \le 1$ then it doesn't follow.

Note that if we add this hypothesis to normed_ring, then the frobenious norm on matrices is no longer an instance of this

[Jireh Loreaux]

So, the question is: do we want to allow normed algebras where the norm of the identity is strictly greater than 1? If not, then ∥1∥ ≤ 1 should be added to the definition, otherwise not. (Even with that condition the results would still hold on trivial norm structures.)

[Kevin Buzzard]

What's the Frobenious norm on matrices?

[Jireh Loreaux]

I think not adding the condition is better though. It matches my familiarity with the literature.

[Eric Wieser]

Kevin Buzzard said:

What's the Frobenious norm on matrices?

https://mathworld.wolfram.com/FrobeniusNorm.html (or #13497)

[Eric Wieser]

I spelt it wrong, oops

[Kevin Buzzard]

It matches my familiarity with the literature.

yeah, and it doesn't match mine! This makes the question quite interesting I think! In the nonarchimedean setting this is commonplace but apparently it's not commonplace elsewhere?

[Jireh Loreaux]

@Reid Barton : I actually did mean normed algebras, yes. It doesn't make sense to add it for normed rings I don't think.

[Jireh Loreaux]

Sorry, can you be more specific Kevin? You mean that in your literature a normed algebra always satisfies ∥1∥ = 1 (except for the zero ring)?

[Kevin Buzzard]

|1|<=1 is an axiom in one of the canonical references for nonarchimedean normed rings.

[Eric Wieser]

Does ∥1∥ ≤ 1 follow from ∥algebra_map 𝕜 𝕜' x∥ ≤ ∥x∥ applied at x=1, noting that 𝕜 is a normed field and so docs#normed_division_ring.to_norm_one_class applies?

[Kevin Buzzard]

Is \k a field? If so then this looks promising.

[Reid Barton]

Well I guess in the nonarchimedean setting you would not be adding norms together anyways, so it makes sense that you would not have an example like the Frobenius norm

[Eric Wieser]

Kevin Buzzard said:

Is \k a field? If so then this looks promising.

Yes, right now normed_algebra refers only to fields

[Jireh Loreaux]

@Eric Wieser , yes, I think that works.

[Eric Wieser]

Yep:

lemma norm_one_le : ∥(1 : 𝕜')∥ ≤ 1 :=
calc ∥(1 : 𝕜')∥ = ∥algebra_map 𝕜 𝕜' 1∥ : by rw map_one
            ... ≤ ∥(1 : 𝕜)∥ : norm_algebra_map_le _ _
            ... = 1 : norm_one

[Jireh Loreaux]

Okay, so the reason it works here and it differs in the literature I read is the following: In my literature, an algebra is basically defined to be a vector space with a compatible (non-unital) ring structure, and then a normed algebra is basically a vector space with a compatible (non-unital) normed ring structure. However, it is never assumed in this context that we have the ring homomorphism algebra_map (or the corresponding condition on the norm), and the reason it is never assumed is that we consider non-unital algebras as first-class citizens, so it wouldn't make sense to have that homomorphism.

[Reid Barton]

I guess a related issue is whether "algebra" means unital or not. In Bourbaki it does not mean a unital algebra by default.
In math, we could perhaps distinguish "normed unital algebra" ($||1|| \le 1$) and "unital normed algebra" (no assumption on $||1||$).

[Eric Wieser]

Does the literature have much to say about semi_normed algebras?

[Eric Wieser]

Jireh Loreaux said:

You're probably already changing it, but I think in #13544 because of the above it makes sense to have everything point the opposite direction. That is, nontrivial → norm_one_class, and then add the nontrivial type class everywhere necessary instead of norm_one_class.

I'm still reluctant to do this, as the reverse direction only holds in a normed_ring not a semi_normed_ring. I also really don't want to open too many cans of worms at once!

[Jireh Loreaux]

I understand, but I guess then we can't have normed_algebra + nontrivial → norm_one_class as an instance because of instance loops? That would be a shame.

[Eric Wieser]

Not even instance loops, we can't have normed_algebra K A - > foo A ever because K is unknown

[Eric Wieser]

Which is why docs#normed_algebra.norm_one_class is not an instance

[Jireh Loreaux]

Then I completely agree with you. Adding norm_one_class everywhere necessary is fine with me.

[Eric Wieser]

In that case, the correct condition should I think be $||r a||_A = ||r||_R \cdot ||a||_A$

I think this is weaker (by itself, as it doesn't imply $||1|| ≤ 1$); on the other hand, this weakening means that the frobenius norm on matrices _is_ a normed algebra

[Eric Wieser]

So maybe normed_algebra should be as you describe there, which is even weaker than what I have in the PR.

[Eric Wieser]

(or as norm (algebra_map R A r) ≤ norm r * norm (1 : A), which is probably equivalent but likely easier to prove)

[Eric Wieser]

In the presence of norm_one_class it's still just the same as what we have now

[Jireh Loreaux]

@Kevin Buzzard thoughts?

[Eric Wieser]

The interpretation becomes simply "a normed algebra is an algebra that is a normed module and a normed ring"

[Eric Wieser]

With no extra conditions

[Reid Barton]

Jireh Loreaux said:

However, I also care a great deal about the case of non-unital algebras. In that case, the correct condition should I think be $||r a||_A = ||r||_R \cdot ||a||_A$

Do you have $=$ and not $\le$ because you are assuming $R$ is a normed field?

[Jireh Loreaux]

Yes, that's the only context in which we currently have normed_algebra in mathlib

[Eric Wieser]

Note that even though that's the case, src#normed_space only requires the inequality (and derives docs#norm_smul from it)

[Jireh Loreaux]

Do you want me to PR this, putting it right after docs#nnnorm_mul_le?

lemma one_le_norm_one (β) [normed_ring β] [nontrivial β] : 1 ≤ ∥(1 : β)∥ :=
(le_mul_iff_one_le_left $ norm_pos_iff.mpr (one_ne_zero : (1 : β) ≠ 0)).mp
  (by simpa only [mul_one] using norm_mul_le (1 : β) 1)

lemma one_le_nnnorm_one (β) [normed_ring β] [nontrivial β] : 1 ≤ ∥(1 : β)∥₊ :=
by simpa only [←norm_to_nnreal, real.to_nnreal_one] using real.to_nnreal_mono (one_le_norm_one β)

[Jireh Loreaux]

#13556 : you're welcome to push any changes if you want. I put it in the root namespace because I don't think it should clash with anything.

[Kevin Buzzard]

The only thing I have to add is that yes seminormed algebras over a field are a thing. The spectral seminorm plays an important role in nonarchimedean analysis in the sense of Tate; here you would have a field like k=Q_p and then any affinoid k-algebra e.g. k[T]/(T^2) gets a canonical spectral seminorm which in this case would not be a norm because |T|=0.

[Eric Wieser]

Eric Wieser said:

(or as norm (algebra_map R A r) ≤ norm r * norm (1 : A), which is probably equivalent but likely easier to prove)

I don't think this is equivalent after all

Reid Barton said:

I think the correct way to think about it is $||r a||_A \le ||r||_R \cdot ||a||_A$

I've modified #13544 to use this definition