Quadratic Maps

Stream: maths

[Christopher Hoskin]

I'd like to introduce Quadratic Maps over a (commutative) Ring to Mathlib. This is in order to be able to define such things as quadratic Jordan Algebras and Jordan Pairs.

Currently Mathlib has Quadratic Forms. These are defined over a non-commutative semiring.

There are a number of possible ways of proceeding:

1. Develop QuadraticMap and QuadraticForm as separate (but very similar) theories, with the former over a commutative ring and the latter over a non-commutative ring
2. Have QuadraticForm as a special case of QuadraticMap, but both over a commutative ring. This would result in a QuadraticForm that is less general than what we currently have
3. Develop a theory of QuadraticMap over a non-commutative ring that specialises to the current QuadraticForm

Option 1. seems undesirable to me. I made a start on 3. in this PR https://github.com/leanprover-community/mathlib4/pull/7569 but it requires more bi-module theory than we currently have.

@Eric Wieser is suggesting that we try 2. instead, but we thought it might be worth asking here first.

Possibly @Anne Baanen may have an opinion as their PR first introduced Quadratic Forms https://github.com/leanprover-community/mathlib/pull/2480

[Eric Wieser]

In particular, 2 would start with un-generalizing docs#QuadraticForm from Semiring to CommSemiring

[Eric Wieser]

But I claim that the $Q(rm) = r^2Q(m)$ axiom we currently have is nonsense in the non-commutative case anyway, so we'd not be losing anything of value

[Yaël Dillies]

What's the correct axiom then? $Q(rm) = rQ(m)r$?

[Christopher Hoskin]

Yaël Dillies said:

What's the correct axiom then? $Q(rm) = rQ(m)r$?

We've already ruled that out: https://github.com/leanprover-community/mathlib4/pull/7538#issuecomment-1751785216

[Eric Wieser]

I think it's $Q(rm)= rQ(m)r^*$, but I don't think that generalization is worth the effort yet

[Eric Wieser]

(in that the generalization that Christopher wants now is more important than fixing the incorrect one that we already have but no one wants yet)

[Jireh Loreaux]

This is relevant: https://eudml.org/doc/257900

[Eric Wieser]

That looks consistent with my guess above, though it's nice to have a reference now

[Anne Baanen]

I have very little use for the noncommutative case, so I think we should go for whatever works best in the commutative case, and is easy enough to make work noncommutatively. My slight preference goes towards 2 since you've convinced me that our noncommutative quadratic form isn't really a quadratic form (yet).

[Eric Wieser]

Are we concluding that docs#BilinForm is also nonsense when R is non-commutative?

[Eric Wieser]

@Heather Macbeth made some generalization in that direction in #6824, but it seems we've had

structure bilin_form (α : Type u) (β : Type v) [ring α] [add_comm_group β] [module α β] :=

right from the very beginning in #1300

[Eric Wieser]

#7581 removes support for non-commutative rings from docs#QuadraticForm

[Eric Wieser]

I guess the questions about BilinForm become irrelevant once we finish the refactor to replace it with nested linear maps

[Julian Külshammer]

Yes, pulling out both scalars on the left seems non-standard in the non-commutative setting, see e.g. Morita's "A theorem on Frobenius extensions" (1969), where a generalisation of Frobenius algebras appears.

[Eric Wieser]

Now that #7581 is merged, you can start on 2 @Christopher Hoskin without having to worry about non-commutativity

[Christopher Hoskin]

Thanks! It seems to be working. :)

[Eric Wieser]

It's starting to look like maybe we should finish the def BilinForm R M := M →ₗ[R] M →ₗ[R] R refactor before going ahead too far with this one

[Christopher Hoskin]

Eric Wieser said:

It's starting to look like maybe we should finish the def BilinForm R M := M →ₗ[R] M →ₗ[R] R refactor before going ahead too far with this one

Okay, is there an issue or PR I can track for that, so I know when the refactor is done?