instance for `End k (BilinForm k V)`

Stream: mathlib4

[George McNinch]

Hi--

For a vector space V over a field k, I'd like to view LinearMap.lflip as an endomorphism of BilinForms k V, and I wanted to express that the minimal polynomial was the correct thing. But before getting started, I'm having some instance issues, as follows:

import Mathlib.Tactic

open Module
open LinearMap
open LinearMap (BilinForm)

variable  {k V :Type} [Field k]
  [AddCommGroup V] [Module k V] [Module.Finite k V]

example : Ring (Module.End k V) := inferInstance       -- baseline; this succeeds

example : Ring (Module.End k (BilinForm k V)) := inferInstance -- fails

example : Algebra k (Module.End k (BilinForm k V)) := inferInstance -- succeeds?!

example : Polynomial k := minpoly k (B := Module.End k (BilinForm k V)) lflip

-- minpoly example reports "failed to synthesize
--                          Ring (End k (BilinForm k V)) "


-- the following also fails, but maybe that is less surprising
example : Polynomial k := minpoly k (lflip:(BilinForm k V) →ₗ[k] (BilinForm k V))

Is there something else I should try?

Thanks and all the best,
george

[Kevin Buzzard]

You can just make the instance with

instance : Ring (Module.End k (BilinForm k V)) := End.instRing (N₁ := BilinForm k V)

Maybe typeclass inference is confused by Bilinform being an abbrev? I just tried changing it to a reducible def but now I have to compile several hundred mathlib files...

[Kyle Miller]

@Kevin Buzzard abbrev definitions get @[reducible]. Do you ever see cases where changing abbrev to @[reducible] def make typeclass inference succeed when it previously failed?

[Kevin Buzzard]

No, I have no understanding of why suddenly people are saying abbrev should be reducible def so I'm just experimenting to try and understand what if anything the difference is. I really don't understand how the system works at all.

[Kyle Miller]

This still fails:

example : Ring (Module.End k (V →ₗ[k] V →ₗ[k] k)) := inferInstance -- fails

That means @[reducible] definitely won't help.

[Kyle Miller]

Kevin Buzzard said:

I have no understanding of why suddenly people are saying abbrev should be reducible def

There are some cases where using @[reducible] def instead of abbrev avoids some typechecking timeouts. Beyond that — for the occasional workaround — there is no reason to avoid abbrev or to try using @[reducible] def if typeclass inference can't find an instance.

Just to reiterate: both abbrev and @[reducible] def create abbreviations that typeclass inference can see through equally well.

[Aaron Liu]

import Mathlib.Tactic

open Module
open LinearMap
open LinearMap (BilinForm)

variable  {k V :Type} [Field k]
  [AddCommGroup V] [Module k V] [Module.Finite k V]

example : Ring (Module.End k V) := inferInstance       -- baseline; this succeeds

-- comment this out and it fails
instance : AddCommGroup (V →ₗ[k] k) := inferInstance

example : Ring (Module.End k (BilinForm k V)) := inferInstance -- succeeds?!

[Kevin Buzzard]

got it:

set_option maxSynthPendingDepth 2 in
#synth Ring (Module.End k (BilinForm k V))

[Kevin Buzzard]

import Mathlib.Tactic

open Module
open LinearMap (BilinForm)
open LinearMap (lflip)

variable  {k V :Type} [Field k]
  [AddCommGroup V] [Module k V] [Module.Finite k V]

set_option maxSynthPendingDepth 2

-- works
#synth Ring (Module.End k (BilinForm k V))

-- works
noncomputable example : Polynomial k := minpoly k (B := Module.End k (BilinForm k V)) lflip

-- also works
noncomputable example : Polynomial k := minpoly k (lflip:(BilinForm k V) →ₗ[k] (BilinForm k V))

[George McNinch]

Huh, thanks! Any comments on why maxSynthPendingDepth != 2 is problematic?

[Sahan Wijetunga]

It works for >= 2 as well

[Kevin Buzzard]

The default in some situations is 1 (but I thought mathlib changed the default to 3 precisely to avoid this kind of confusion). I have seen instances where lowering 3 to 1 makes things compile much faster, so there is a trade-off here.