CLM as NormedAddGroupHom?

Stream: Is there code for X?

[Yoh Tanimoto]

I want to to define the lift of a continuous linear map f on a seminormed vector space to the separation quotient. I could do it by defining all fields, but it seems more natural to take f as a NormedAddGroupHom, then lift it.

I found ContinuousLinearMap.isBoundedLinearMap, but it only applies to the same scalar?

Is there already such a thing, or what would be the best way?

[Eric Wieser]

(docs#NormedAddGroupHom)

[Eric Wieser]

@loogle ContinuousLinearMap, NormedAddGroupHom

[loogle]

:shrug: nothing found

[Yoh Tanimoto]

thanks for your comments, does this mean that some instances are missing?

[Eric Wieser]

My uninformed take on this is that docs#NormedAddGroupHom shouldn't exist at all, and we could make do with continuous additive maps. It's likely I'm wrong here, in which case it would be great if the module docstring could elaborate on why we can get away without NormedLinearMaps but can't do so for NormedAddGroupHoms.

[Yoh Tanimoto]

ah do you mean that all NormedAddGroupHom should be just ContinuousAddMonoidHom with the continuity in the sense of (Semi)NormedAddCommGroup?

[Eric Wieser]

That's my claim, but I expect an analyst to tell me why this is wrong. Certainly all NormedAddGroupHoms are continuous, but perhaps the converse is not true

[Yoh Tanimoto]

ok let's wait for comments by analysis...

[Sébastien Gouëzel]

For continuous linear maps over a nontrivially normed field, you can deduce the norm control just from the continuity, because by rescaling by an element of the field you can bring any element arbitrarily close to 0. This is not true for additive homomorphisms, so there is a genuine mathematical difference here.

[Yoh Tanimoto]

right. So should we just define lifts of ContinuousMonoidHom, CLM, NormedGroupHom separately?

[Yury G. Kudryashov]

What is the type signature of the function you want to define?

[Yoh Tanimoto]

say, liftCLM {σ : R →+* S} (f : M →SL[σ] N) (hf : ∀ x y, Inseparable x y → f x = f y) : (SeparationQuotient M) →SL[σ] N for CLM, and similar for others.