## Stream: maths

### Topic: Bilinear forms

#### Yury G. Kudryashov (Mar 12 2020 at 16:58):

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 (Mar 12 2020 at 16:59):

What kind of change do you mean exactly?

#### Johan Commelin (Mar 12 2020 at 17:00):

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

#### Patrick Massot (Mar 12 2020 at 17:00):

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 (Mar 12 2020 at 17:01):

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

#### Yury G. Kudryashov (Mar 12 2020 at 17:24):

@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_smul_right' := ∀ c x y, to_fun x (c • y) = c • to_fun x y }


#### Yury G. Kudryashov (Mar 12 2020 at 17:25):

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

#### Yury G. Kudryashov (Mar 12 2020 at 17:26):

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

#### Yury G. Kudryashov (Mar 12 2020 at 17:33):

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 (Mar 12 2020 at 17:39):

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 (Mar 12 2020 at 17:46):

@Sebastien Gouezel Sure.

#### Yury G. Kudryashov (Mar 12 2020 at 17:48):

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 (Mar 12 2020 at 18:11):

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 (Mar 12 2020 at 18:23):

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 (Mar 12 2020 at 18:36):

One right and one left module.

#### Yury G. Kudryashov (Mar 12 2020 at 19:57):

Thank you, I'll take this route then

#### Johan Commelin (Mar 12 2020 at 20:03):

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

#### Kevin Buzzard (Mar 12 2020 at 20:52):

We probably have opposite rings

#### Reid Barton (Mar 12 2020 at 21:15):

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 (Mar 12 2020 at 21:16):

Yep, I think that's right.

#### Reid Barton (Mar 12 2020 at 21:19):

I'm wondering how I never knew that before.

#### Reid Barton (Mar 12 2020 at 21:20):

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 (Mar 12 2020 at 21:29):

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

#### Kevin Buzzard (Mar 12 2020 at 21:38):

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

#### Reid Barton (Mar 12 2020 at 21:38):

What's the category here then?

Last updated: May 18 2021 at 08:14 UTC