bilinear forms

Stream: maths

[Yury G. Kudryashov]

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]

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]

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

[Yury G. Kudryashov]

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]

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