Sesquilinear form

Stream: Is there code for X?

[Winston Yin]

How would one concisely write down a sesquilinear form? Is there an equivalent of bilin_form? I'm trying to write statements about the (anti)dual space of n → ℂ consisting of antilinear maps from n → ℂ to ℂ. For example, a sesquilinear form defines for every element x : n → ℂ a (anti)dual ⟪x,⬝⟫, so that the (anti)dual of a map may be identified with the conjugate transpose of the corresponding matrix. A set of theorems may then be stated for the antidual space similar to those for module.dual, basis.dual_basis, and linear_map.dual_map. Or would that be redundant?

[Winston Yin]

Would it just be a composition of semilinear maps f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P, where the first semilinear map is antilinear, and the second semilinear map is linear? If so, why is there a separate bilin_form?

[Eric Wieser]

Do we still have docs#sesq_form

[Eric Wieser]

Seemingly not; I think we replaced it with semilinear maps

[Eric Wieser]

I think the eventual goal was to do the same for bilin_form

[Moritz Doll]

Yes, I was working on that, but I had lots of other stuff going on.. @Winston Yin the idea was that we don't need separate definitions for bilin_form and sesq_form, they are just special cases of linear maps, namely M →ₗ[R] M ₗ[R] R for bilin_form and similarly for sesq_form. In the later case all the stuff that got implemented is in linear_algebra/sesquilinear_form and linear_algebra/bilinear_maps,
the issue for bilin_form is just that the file is extremely large and is used in quite a lot of places.