Sesquilinear form notation

Stream: maths

[Wrenna Robson]

Hi,

Why is the notation used for inner products not available for general sesquilinear forms? There's good notions of these that apply for fields that aren't R or C, but the approach in linear_algebra.sesquilinear_form seems a little tricky - there's no bundled form?

[Frédéric Dupuis]

The only notation for inner products that is defined globally is

notation `⟪`x`, `y`⟫_ℝ` := @inner ℝ _ _ x y
notation `⟪`x`, `y`⟫_ℂ` := @inner ℂ _ _ x y

and wherever we use the plain ⟪x, y⟫ notation, it's actually defined locally. So there's nothing stopping you from using it for sesquilinear forms.

[Eric Wieser]

I think this question might be about associating a canonical sesquilinear/bilinear/quadratic form (but not necessarily an inner product) with a type. Is that accurate, @Wrenna Robson?

[Eric Wieser]

Or are you only interested in the case where the sesquilinear form really is in some weakened sense an docs#inner_product_space?

[Eric Wieser]

Right now the

norm_sq_eq_inner : ∀ (x : E), ∥x∥ ^ 2 = ⇑is_R_or_C.re (has_inner.inner x x)

axiom makes it sort of pointless to talk about fields other than R or C

[Eric Wieser]

Maybe replacing that with the stronger

norm_sq_eq_inner : ∀ (x : E), algebra_map ℝ K (∥x∥ ^ 2) = (has_inner.inner x x)

would help

[Wrenna Robson]

I think essentially I want access to the notation. The context is that in coding theory one talks about the dual space as being the space made up of the orthogonal vectors, and there's a clear idea that the "dot product" is a meaningful notion there. But it is just the bilinear form, it isn't an inner product.