# Zulip Chat Archive

## Stream: new members

### Topic: structure forgets its parents

#### Eloi (Jul 20 2020 at 11:43):

Hi, I am writing a structure that indirectly extends from `linear_map`

, and I don't know how to recover this map to impose more conditions on it. Thanks!

```
import linear_algebra.matrix linear_algebra.quadratic_form
variables {d : ℕ}
local notation `Quadratic_form` := quadratic_form ℤ (fin d → ℤ)
structure properly_equivalent (Q Q': Quadratic_form) extends quadratic_form.isometry Q Q':=
(determinant_is_one : to_fun.to_matrix.det = 1)
#check linear_map.to_matrix
#check matrix.det
```

#### Johan Commelin (Jul 20 2020 at 11:44):

Do you mean that this gives an error?

#### Johan Commelin (Jul 20 2020 at 11:45):

Aah, the `to_fun.to_matrix`

looks a bit suspicious

#### Eloi (Jul 20 2020 at 11:48):

Yes I know, because `to_fun`

is only a function and not a `linear_map`

... but at some point this strucure had a `linear_map`

with `to_fun`

as "its" `to_fun`

... I don't know how to recover this `linear_map`

.

#### Johan Commelin (Jul 20 2020 at 11:49):

I see

#### Johan Commelin (Jul 20 2020 at 11:49):

Aside, note that we also have: https://github.com/leanprover-community/mathlib/blob/4ec7cc58e126b736de864b91649c0f7f3d6a7d48/src/linear_algebra/quadratic_form.lean#L490

#### Johan Commelin (Jul 20 2020 at 11:49):

So you might want to have `proper_isometry`

and `properly_equivalent`

along the same lines

#### Johan Commelin (Jul 20 2020 at 11:51):

I think you can talk about `linear_map.to_matrix \< to_fun, map_add', map_smul' \>`

. It's a bit ugly, but it works for the definition.

Then you can restate it afterwards, which you should probably do anyways.

#### Eloi (Jul 20 2020 at 12:02):

What is the correct sintax? I can't get it working... This is what I tried

```
import linear_algebra.matrix linear_algebra.quadratic_form
variables {d : ℕ}
local notation `Quadratic_form` := quadratic_form ℤ (fin d → ℤ)
structure proper_isometry (Q Q': Quadratic_form) extends quadratic_form.isometry Q Q':=
(determinant_is_one : (linear_map.to_matrix ⟨to_fun, map_add', map_smul'⟩).det = 1 )
```

#### Johan Commelin (Jul 20 2020 at 12:03):

Hmm, maybe remove the `\<to_fun, .. \>`

part, and put a `_`

there.

#### Johan Commelin (Jul 20 2020 at 12:03):

Then click onthe light bulb, and choose the "skeleton" option

#### Eloi (Jul 20 2020 at 12:09):

Doesn't work either... I get the following error message:

```
type mismatch as structure instance
{to_fun := to_fun, map_add' := map_add', map_smul' := map_smul'}
has type
(fin d → ℤ) →ₗ[ℤ] fin d → ℤ : Type
but is expected to have type
(?m_2 → ?m_1) →ₗ[?m_1] ?m_3 → ?m_1 : Type (max ? ?)
```

my attempt was:

```
structure proper_isometry (Q Q': Quadratic_form) extends (quadratic_form.isometry Q Q'):=
(determinant_is_one : (linear_map.to_matrix {to_fun := to_fun,
map_add' := map_add',
map_smul' := map_smul'
}).det = 1 )
```

#### Johan Commelin (Jul 20 2020 at 12:12):

Aha, we probably need to tell it a bit more types...

#### Johan Commelin (Jul 20 2020 at 12:12):

If you copy ` : (fin d → ℤ) →ₗ[ℤ] fin d → ℤ`

and put it after the `}`

, but before `).det`

... does that help?

#### Johan Commelin (Jul 20 2020 at 12:13):

(Note the `:`

at the begin of the text-to-be-copied

#### Eloi (Jul 20 2020 at 13:01):

It didn't work... I tried two alternatives:

```
import linear_algebra.matrix linear_algebra.quadratic_form
variables {d : ℕ}
local notation `Quadratic_form` := quadratic_form ℤ (fin d → ℤ)
structure proper_isometry' (Q Q': Quadratic_form) extends (quadratic_form.isometry Q Q'):=
(determinant_is_one :
({to_fun := to_fun, map_add' := map_add', map_smul' := map_smul'} : (fin d → ℤ) →ₗ[ℤ] fin d → ℤ).to_matrix.det = 1 )
structure proper_isometry (Q Q': Quadratic_form) extends (quadratic_form.isometry Q Q'):=
(determinant_is_one : (linear_map.to_matrix {to_fun := to_fun,
map_add' := map_add',
map_smul' := map_smul'
} : (fin d → ℤ) →ₗ[ℤ] fin d → ℤ).det = 1 )
```

both give the error message:

```
type mismatch at application
{to_fun := to_fun, map_add' := map_add', map_smul' := map_smul'}.to_matrix
term
{to_fun := to_fun, map_add' := map_add', map_smul' := map_smul'}
has type
(fin d → ℤ) →ₗ[ℤ] fin d → ℤ : Type
but is expected to have type
(?m_2 → ?m_1) →ₗ[?m_1] ?m_3 → ?m_1 : Type (max ? ?)
```

#### Kevin Buzzard (Jul 20 2020 at 16:32):

My next step would be to write `@linear_map.to_matrix`

and start filling in the implicit fields to see if something funny happens.

#### Kevin Buzzard (Jul 20 2020 at 16:34):

aaand: bingo!

```
import linear_algebra.matrix linear_algebra.quadratic_form
variables {d : ℕ}
local notation `Quadratic_form` := quadratic_form ℤ (fin d → ℤ)
structure proper_isometry (Q Q': Quadratic_form) extends quadratic_form.isometry Q Q' :=
(determinant_is_one :
(@linear_map.to_matrix (fin d) (fin d) _ _ ℤ _ _ ⟨to_fun, map_add', map_smul'⟩).det = 1 )
```

gives error

```
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
pi.semimodule (fin d) (λ (i : fin d), (λ (a : fin d), ℤ) i) ℤ
inferred
pi.semimodule (fin d) (λ (a : fin d), ℤ) ℤ
```

#### Kevin Buzzard (Jul 20 2020 at 16:35):

There is some kind of typeclass diamond which is stopping unification from working.

#### Kevin Buzzard (Jul 20 2020 at 16:36):

I'm afraid this is beyond my pay grade but at least we now know the problem.

Last updated: May 13 2021 at 06:15 UTC