Not not picking up module structure on bounded linear ops

Stream: new members

[Cameron Torrance]

I'm working on a construction involving a non-unital C*-algebra A but I am not sure how to make the ℂ-module structure on A →L[ℂ] A .

Here is how I'm modelling A and my imports.

import analysis.normed_space.operator_norm
import analysis.complex.basic
import algebra.module.prod
import topology.continuous_function.algebra

noncomputable theory
open_locale nnreal ennreal
local postfix `⋆`:std.prec.max_plus := star

variables {A : Type*} [non_unital_normed_ring A] [star_ring A] [module ℂ A] [star_module ℂ A]
variables [smul_comm_class ℂ A A] [is_scalar_tower ℂ A A] [normed_space ℂ A]
variables [cstar_ring A] [complete_space A]

[Kevin Buzzard]

The instance seems to be called continuous_linear_map.module but

example : module ℂ (A →L[ℂ] A) := continuous_linear_map.module

fails because Lean complains that it can't find has_continuous_const_smul ℂ A. I don't know anything about how C^* algebras are implemented in Lean (in particular I have absolutely no idea whether your variables are OK) but my guess is that it's saying that, given your choice, it doesn't know why C acts continuously on A (so in particular it can't make the module structure because it can't prove that the C-action on linear maps preserves continuity).

[Cameron Torrance]

There is a instance of normed_space defined in the op norm file which extends module and I think my assumptions are stronger than those needed.

[Cameron Torrance]

though it could be they aren't in quite the right form

[Eric Wieser]

It feels like that has_continuous_const_smul should be coming from the normed_space instance

[Cameron Torrance]

Eric Wieser said:

It feels like that has_continuous_const_smul should be coming from the normed_space instance

I've tried using continuous_linear_map.to_x_instance map defn in the operator norm file but lean complains when I give that a try

[Cameron Torrance]

I think the fundamental problem here is that lean is not seeing that A →L[ℂ] A has a norm and at least for now the has_continuous_const_smul stuff is a bit of a red herring.

For example the assumptions (using continuous_linear_map.to_semi_normed_ring) for A →L[ℂ] A to be a semi_normed_ring are the following :

• A is a semi_normed_group( A being a non_unital_normed_ring should, at least morally, be enough)
• ℂ is a nondiscrete_normed_field (holds)
• A is a normed_space over ℂ (explicit assumption).