Zulip Chat Archive

Stream: maths

Topic: Bilinear forms


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 12 2020 at 16:59):

What kind of change do you mean exactly?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 12 2020 at 17:01):

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

view this post on Zulip 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_add_right' := ...,
  map_smul_right' :=  c x y, to_fun x (c  y) = c  to_fun x y }

view this post on Zulip Yury G. Kudryashov (Mar 12 2020 at 17:25):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Mar 12 2020 at 17:46):

@Sebastien Gouezel Sure.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 12 2020 at 18:36):

One right and one left module.

view this post on Zulip Yury G. Kudryashov (Mar 12 2020 at 19:57):

Thank you, I'll take this route then

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 12 2020 at 20:52):

We probably have opposite rings

view this post on Zulip 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 C\mathbb{C}-vector space, am I supposed to consider it as a right C\mathbb{C}-vector space by the conjugate action?

view this post on Zulip Johan Commelin (Mar 12 2020 at 21:16):

Yep, I think that's right.

view this post on Zulip Reid Barton (Mar 12 2020 at 21:19):

I'm wondering how I never knew that before.

view this post on Zulip 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)?

view this post on Zulip Scott Morrison (Mar 12 2020 at 21:29):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Mar 12 2020 at 21:38):

What's the category here then?


Last updated: May 18 2021 at 08:14 UTC