Zulip Chat Archive

Stream: new members

Topic: structure forgets its parents


view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 20 2020 at 11:44):

Do you mean that this gives an error?

view this post on Zulip Johan Commelin (Jul 20 2020 at 11:45):

Aah, the to_fun.to_matrix looks a bit suspicious

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 20 2020 at 11:49):

I see

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 20 2020 at 11:49):

So you might want to have proper_isometry and properly_equivalent along the same lines

view this post on Zulip 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.

view this post on Zulip 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 )

view this post on Zulip Johan Commelin (Jul 20 2020 at 12:03):

Hmm, maybe remove the \<to_fun, .. \> part, and put a _ there.

view this post on Zulip Johan Commelin (Jul 20 2020 at 12:03):

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

view this post on Zulip 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 )

view this post on Zulip Johan Commelin (Jul 20 2020 at 12:12):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 20 2020 at 12:13):

(Note the : at the begin of the text-to-be-copied

view this post on Zulip 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 ? ?)

view this post on Zulip 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.

view this post on Zulip 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), ) 

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 16:35):

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

view this post on Zulip 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