structure forgets its parents

Stream: new members

[Eloi]

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]

Do you mean that this gives an error?

[Johan Commelin]

Aah, the to_fun.to_matrix looks a bit suspicious

[Eloi]

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]

I see

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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

[Eloi]

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]

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

[Johan Commelin]

If you copy : (fin d → ℤ) →ₗ[ℤ] fin d → ℤ and put it after the }, but before ).det... does that help?

[Johan Commelin]

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

[Eloi]

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]

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]

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]

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

[Kevin Buzzard]

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