Continuous linear map to normed group hom

Stream: Is there code for X?

[Daniel Roca González]

Hi,
I am in a situation where I have a continuous_linear_map and need to convert it to a normed_group_hom. It seems weird to me that these are even different notions. Is there an automatic way to convert between them? I don't find any function to do this. Should automatic coercion work?

[Eric Wieser]

This certainly won't be automatic, someone will have had to prove continuous_linear_map.to_normed_group_hom by hand (and as far as I can see they haven't). Are you able to prove that yourself? (I can't comment on whether it's true)

[Patrick Massot]

Daniel Roca González said:

Hi,
I am in a situation where I have a continuous_linear_map and need to convert it to a normed_group_hom. It seems weird to me that these are even different notions.

Normed group homomorphisms are maps between normed group that have no reason to be linear spaces, so there is no way they could "the same notion".

[Patrick Massot]

And continuous linear maps assume you have a topological module (say a topological vector space) but they do not assume the topology comes from a norm.

[Patrick Massot]

Does it make sense?

[Eric Wieser]

Here's the missing definition:

import analysis.normed.group.hom
import analysis.normed_space.operator_norm

variables {𝕜 𝕜₂ E F : Type*}
variables [semi_normed_group E] [semi_normed_group F]
variables [nondiscrete_normed_field 𝕜] [nondiscrete_normed_field 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
variables [normed_space 𝕜 E] [normed_space 𝕜₂ F] [ring_hom_isometric σ₁₂]

@[simps]
def continuous_linear_map.to_normed_group_hom (f : E →SL[σ₁₂] F) : normed_group_hom E F :=
{ to_fun := f,
  map_add' := f.map_add,
  bound' := let ⟨r, hr, h⟩ := f.bound in ⟨r, h⟩ }

So all the maths is already there (docs#continuous_linear_map.bound), the glue was just missing

[Daniel Roca González]

Thank you, now I understand why one can't be a subset of the other. I do think that we should have @Eric Wieser 's conversion in the library, along with the other direction.

[Eric Wieser]

Is the other direction true? How do you prove map_smul?

[Daniel Roca González]

wait, you're right, that's not true either

[Patrick Massot]

Crap, Eric was faster

[Patrick Massot]

Mine was:

import analysis.normed_space.operator_norm
import analysis.normed.group.hom

def continuous_linear_map.to_normed_group_hom
  {𝕜 𝕜': Type*} {E : Type*} {F : Type*} [semi_normed_group E]
  [semi_normed_group F] [nondiscrete_normed_field 𝕜] [nondiscrete_normed_field 𝕜']
  [semi_normed_space 𝕜 E] [semi_normed_space 𝕜' F] {σ : 𝕜 →+* 𝕜'} [ring_hom_isometric σ]
  (f : E →SL[σ] F) : normed_group_hom E F :=
{ to_fun := f,
  map_add' := map_add f,
  bound' := ⟨∥f∥, f.le_op_norm⟩ }

[Patrick Massot]

I still prefer my last line.

[Eric Wieser]

I don't get how your last line is so short yet the proof of continuous_linear_map.bound doesn't seem to unfold to it -- oh nevermind, le_op_norm is proved in terms of bound

[Patrick Massot]

Daniel, we could add this, but I'm a bit worried this is an #xy issue. There's a reason why nobody ever needed that. I'm pretty skeptical that you "need to convert it to a normed_group_hom".

[Patrick Massot]

Daniel, if you wonder about the sigma stuff in our code, you can read this blog post.

[Daniel Roca González]

You're right: I said this because I didn't find the equivalent of normed_group_hom.antilipschitz_of_norm_ge , but after looking some more I found linear_map.antilipschitz_of_bound , which is basically what I needed. Thank you both.

[Eric Wieser]

I think the def is still worth having in mathlib simply to show the statement is true, even if it's not useful