algebra_map clm

Stream: Is there code for X?

[Jireh Loreaux]

Do we have a definition for an algebra map as a continuous linear map (when the algebra is a normed algebra)?

def algebra_map_clm (𝕜 : Type*) (E : Type*) [normed_field 𝕜] [semi_normed_ring E]
  [normed_algebra 𝕜 E] : 𝕜 →L[𝕜] E :=
{ to_fun := algebra_map 𝕜 E,
  map_add' := (algebra_map 𝕜 E).map_add,
  map_smul' := λ r x, by rw [algebra.id.smul_eq_mul, map_mul, ring_hom.id_apply, algebra.smul_def],
  cont := (algebra_map_isometry 𝕜 E).continuous }

[Jireh Loreaux]

@Yaël Dillies this seems related to your question about continuous algebra homomorphisms.

[Yaël Dillies]

Do you want the fact that it is both an algebra hom and continuous?

[Jireh Loreaux]

well, not in my current application (I need continuous_linear_map.map_tsum applied to algebra_map), but it's related because the algebra map would be a continuous algebra homomorphism, from which we should have a natural to_continuous_linear_map.

[Eric Wieser]

to_linear_map := algebra.linear_map 𝕜 E is a bit closer

[Wrenna Robson]

[posted in error]