Bilinear forms

Stream: maths

[Yury G. Kudryashov]

I'm going to rewrite bilinear forms using the modules over a ring instead of M, M, and R. Should I care about noncommutative rings?

[Johan Commelin]

What kind of change do you mean exactly?

[Johan Commelin]

Since we only have left-modules, I guess that bilinear forms over non-commutative rings are currently hard to do.

[Patrick Massot]

We clearly need someone to care about noncommutative rings in mathlib. We can't let algebraic geometers pretend there are no commutative rings forever.

[Johan Commelin]

I care about central simple algebras. I bet that Kevin also cares about them.

[Yury G. Kudryashov]

@Johan Commelin I still can define

structure bilinear_map :=
{ to_fun : M₁ → M₂ → M₃,
  map_add_left' := ∀ x₁ x₂ y, to_fun (x₁ + x₂) y = to_fun x₁ y + to_fun x₂ y,
  map_smul_left' := ∀ c x y, to_fun (c • x) y = c • to_fun x y,
  map_add_right' := ...,
  map_smul_right' := ∀ c x y, to_fun x (c • y) = c • to_fun x y }

[Yury G. Kudryashov]

The question is: does it make sense in the non-commutative case?

[Yury G. Kudryashov]

For a commutative case, I can use M₁ →ₗ[R] M₂ →ₗ[R] M₃ with a custom constructor.

[Yury G. Kudryashov]

But in a non-commutative case there is no R-module structure on M₂ →ₗ[R] M₃, so I have to use the structure definition above and define separately to_linear_left, to_linear_right etc.

[Sebastien Gouezel]

There are also already general multilinear maps (over a non-commutative ring) in linear_algebra/multilinear. They are defined on a Pi type, so I think it is worth having a concrete specialisation for bilinear maps, but establishing a link between the two would also be useful.

[Yury G. Kudryashov]

@Sebastien Gouezel Sure.

[Yury G. Kudryashov]

But before starting the refactor I need to know whether it is OK to define bilinear_map only for modules over commutative rings, or I should care about modules over non-commutative rings. In the latter case, (a) what is the "good" definition? (b) what examples I should care about?

[Johan Commelin]

Hmmm, re (a) I'm not sure what the correct definition is; re (b) I think I've only used bilinear forms over quaternion algebras, I think. So I don't know good examples.

[Yury G. Kudryashov]

How do you define bilinear forms over quaternion algebras? Do you have two left modules, or one left module and one right module?

[Johan Commelin]

One right and one left module.

[Yury G. Kudryashov]

Thank you, I'll take this route then

[Johan Commelin]

@Yury G. Kudryashov Which route do you mean? We don't have right modules, and surely you don't only want forms.

[Kevin Buzzard]

We probably have opposite rings

[Reid Barton]

Now I'm wondering, as a math question: in situations involving sesquilinear forms, Hermitian matrices, etc, if I have a left $\mathbb{C}$-vector space, am I supposed to consider it as a right $\mathbb{C}$-vector space by the conjugate action?

[Johan Commelin]

Yep, I think that's right.

[Reid Barton]

I'm wondering how I never knew that before.

[Reid Barton]

Is there some specific fancy structure on a monoidal category or something that tells me how to turn a left module into a right module (@Scott Morrison)?

[Scott Morrison]

The category being braided, and the algebra being commutative wrt that braiding.

[Kevin Buzzard]

I didn't know that way of thinking about sesquilinear forms either. I always thought they were just weird.

[Reid Barton]

What's the category here then?