# Zulip Chat Archive

## Stream: new members

### Topic: Quadratic forms don't work on ℤ

#### Eloi (Jul 18 2020 at 17:32):

Hi, I can't define a quadratic form over `ℤ`

, but I can over `ℚ`

...

Here is my code:

```
import linear_algebra.quadratic_form
-- this is the quadratic form x², and it works
example : quadratic_form ℚ (fin 1→ ℚ) :=
@quadratic_form.proj ℚ _ (fin 1) 0 0
-- this does not work
example : quadratic_form ℤ (fin 1→ ℤ) :=
@quadratic_form.proj ℤ _ (fin 1) 0 0
```

The definition of `quadratic_form.proj`

has the following signature in mathlib:

```
def proj (i j : n) : quadratic_form R₁ (n → R₁)
```

with the assumtion `[comm_ring R₁]`

. What is happening?

#### Reid Barton (Jul 18 2020 at 17:41):

What is the error?

#### Markus Himmel (Jul 18 2020 at 17:43):

The error is

```
type mismatch, term
quadratic_form.proj 0 0
has type
@quadratic_form ℤ (fin 1 → ℤ) (@comm_ring.to_ring ℤ int.comm_ring)
(@pi.add_comm_group (fin 1) (λ (a : fin 1), ℤ)
(λ (i : fin 1), @ring.to_add_comm_group ℤ (@comm_ring.to_ring ℤ int.comm_ring)))
(@pi.semimodule (fin 1) (λ (a : fin 1), ℤ) ℤ (@ring.to_semiring ℤ (@comm_ring.to_ring ℤ int.comm_ring))
(λ (i : fin 1),
@add_comm_group.to_add_comm_monoid ℤ (@ring.to_add_comm_group ℤ (@comm_ring.to_ring ℤ int.comm_ring)))
(λ (i : fin 1), @semiring.to_semimodule ℤ (@ring.to_semiring ℤ (@comm_ring.to_ring ℤ int.comm_ring))))
but is expected to have type
@quadratic_form ℤ (fin 1 → ℤ) int.ring
(@pi.add_comm_group (fin 1) (λ (a : fin 1), ℤ)
(λ (i : fin 1),
@decidable_linear_ordered_add_comm_group.to_add_comm_group ℤ int.decidable_linear_ordered_add_comm_group))
(@pi.semimodule (fin 1) (λ (a : fin 1), ℤ) ℤ (@ring.to_semiring ℤ int.ring)
(λ (i : fin 1), int.add_comm_monoid)
(λ (i : fin 1),
@add_comm_group.int_module ℤ (@ring.to_add_comm_group ℤ (@comm_ring.to_ring ℤ int.comm_ring))))
```

There seem to be several typeclass diamonds here.

#### Johan Commelin (Jul 18 2020 at 17:48):

Hmmm... it's the olde `decidable_*`

that strikes again :sad:

#### Johan Commelin (Jul 18 2020 at 17:49):

I wish we could fix all these problems in one go, but I guess it requires a complete rethinking of the way computation / decidability is handled :sad: Most likely a problem for which a solution is not yet known.

#### Alex J. Best (Jul 18 2020 at 17:50):

I'm not saying its the way to go, but if you just leave the type out lean looks happy

```
def a :=
@quadratic_form.proj ℤ _ (fin 1) 0 0
#print a
```

#### Reid Barton (Jul 18 2020 at 17:53):

It works with `by convert`

for some reason

#### Reid Barton (Jul 18 2020 at 17:54):

I thought the problem would be with the module structure.

#### Reid Barton (Jul 18 2020 at 17:54):

Does Lean know Z-module structures are unique?

#### Johan Commelin (Jul 18 2020 at 17:54):

Hmmm, I don't recall seeing that

#### Markus Himmel (Jul 18 2020 at 17:55):

Reid Barton said:

Does Lean know Z-module structures are unique?

#### Reid Barton (Jul 18 2020 at 17:56):

Couldn't we just define `*`

on `int`

to be whatever action comes from `add_comm_group`

?

#### Johan Commelin (Jul 18 2020 at 18:46):

You mean to make the two defeq? It would mean refactoring core...

Last updated: May 11 2021 at 22:14 UTC