## Stream: maths

### Topic: bilinear forms

#### Yury G. Kudryashov (Jun 01 2020 at 23:04):

Is there a definition that generalizes both bilinear forms M₁ → M₂ → R where M₁ and M₂ are modules over a ring R and bilinear forms M₁ → M₂ → M₃ where M₁, M₂, and M₃ are modules over a commutative ring R?

#### Oliver Nash (Jun 02 2020 at 07:42):

I don't have an answer to your question Yury. I just wanted to say I'm very glad to see that someone is thinking about such generalisations. I wasn't aware of this thread and spent a few minutes a few days ago messing around with something like:

structure bilinear_pairing :=
(bilin : M₁ → M₂ → R)
(...)

variables (I : ring_anti_equiv R R)

def anti_module : module R M₁ :=
{ smul      := λ r x, (I r) • x,
...}

def sesq_form' := @bilinear_pairing R M₁ M₁ _ _ _ _ (anti_module R M₁ I)


#### Reid Barton (Jun 02 2020 at 13:50):

In the former case shouldn't M₁ be a right R-module?

#### Yury G. Kudryashov (Jun 02 2020 at 18:02):

A right R-module is a left opposite R-module. The question is what to do with the codomain. Should it carry be a bi-module (R-module + opposite R-module + actions commute)?

#### Yury G. Kudryashov (Jun 02 2020 at 18:04):

@Oliver Nash Note that #2884 drops ring_anti_equiv in favour of R ≃+* Rᵒᵖ.

Last updated: May 12 2021 at 08:14 UTC