Unitary is not linear?

Stream: maths

[Bjørn Kjos-Hanssen]

This seems strange:

import data.complex.basic
import algebra.star.unitary
theorem mwe (A:ℂ→ℂ)(h:A ∈ unitary (ℂ→ℂ)) : ((star A) * A) 0 = 1 :=
calc (star A * A) 0 = (1:ℂ→ℂ) 0: by rw h.1
                ... = 1: rfl

I would have expected (star A) * A to be the identity map?

[Frédéric Dupuis]

You're probably looking for ℂ →L[ℂ] ℂ instead of ℂ → ℂ. The monoid instance on ℂ → ℂ is docs#pi.monoid, which defines one to be λ x, 1, as you can see by trying

theorem mwe2 : (1 : ℂ → ℂ) = λ x, 1 := rfl

[Bjørn Kjos-Hanssen]

Ah, thanks @Frédéric Dupuis . I guess it does make sense that in the general case of $A: M \to N$ for monoids $M\ne N$, there is no identity map, so 1 should mean the constant function 1.

[Bjørn Kjos-Hanssen]

How do you type / import the L?

[Jireh Loreaux]

that's docs#continuous_linear_map. So anything that imports that will suffice.

[Eric Wieser]

You can also use 1 : function.End ℂ

[Bjørn Kjos-Hanssen]

Thanks @Eric Wieser Indeed, I was wondering if there was a way to take advantage of the fact that an identity function exists when $M=N$ (above)

[Bjørn Kjos-Hanssen]

To guarantee that unitary maps are linear perhaps we have to use something like euclidean_space?

[Notification Bot]

Bjørn Kjos-Hanssen has marked this topic as unresolved.

[Kevin Buzzard]

The identity function M -> M is called id rather than 1.

[Jireh Loreaux]

docs#unitary is a submonoid of a star monoid. That is, for any type with star, 1 and * (plus compatibility requirements), the unitary elements are exactly those u such that u⁻¹ = u⋆. So, for example, u : unitary ℂ is a complex number of modulus one. One can always view unitaries as elements of the original monoid (i.e., if u : unitary ℂ, then ↑u : ℂ makes sense, the ↑ is a coercion). However, there is no way to view this as a linear map; I know there is mathematically, but there is no linear coercion from ℂ to linear maps from ℂ to ℂ. Thus, in general, one cannot think of unitaries as linear maps.

Note that this is what you should expect. For example, if A is a C⋆-algebra, and u : unitary A, then it makes sense to think of ↑u : A, but the only way to think of u as a linear map is to represent A faithfully on some Hilbert space, but which one should you choose? So, we shouldn't expect this behavior.

Finally, to answer what I think is your question: the type of linear maps E →ₗ[𝕜] E where E is an inner product space over 𝕜 (= ℝ or ℂ) has an docs#linear_map.adjoint which is the docs#linear_map.has_star operation on this type. Moreover, such linear maps also have 1 and * (identity map and composition). Therefore, unitary (E →ₗ[𝕜] E) makes sense and some u of this type will have a coercion to an honest-to-God linear map.

[Jireh Loreaux]

The type euclidean_space ℂ (fin n) →ₗ[ℂ] euclidean_space ℂ (fin n) where n : ℕ is the type of all ℂ-linear maps from ℂⁿ to itself.