## 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 → ℤ)

(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.

I see

#### 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 → ℤ)

(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
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_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 → ℤ)

(determinant_is_one :
({to_fun := to_fun, map_add' := map_add', map_smul' := map_smul'} : (fin d → ℤ) →ₗ[ℤ] fin d → ℤ).to_matrix.det = 1 )

(determinant_is_one :  (linear_map.to_matrix {to_fun := to_fun,
map_smul' := map_smul'
} : (fin d → ℤ) →ₗ[ℤ] fin d → ℤ).det = 1 )


both give the error message:

type mismatch at application
term
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 → ℤ)

(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