instances for `Rep R G`

Stream: maths

[Richard Hill]

I'm confused about the following code:

import Mathlib

variable {R : Type} [CommRing R]
variable {G : Type} [Group G]
open Rep

instance myInstance (A B : Rep R G) : MulActionHomClass (Action.HomSubtype _ _ A B)
    R A B where
  map_smulₛₗ f := map_smul f.val


instance (A : Rep R G) : MulActionHomClass (Action.HomSubtype _ _ A (leftRegular R G))
    R A (leftRegular R G) :=
  myInstance _ _

why is the second instance needed, since it seems to be just a special case of the first ?

[Aaron Liu]

Where is this code coming from?

[Richard Hill]

it's my code. I just don't know why I need the second instance which looks like a hack.
The same thing happens with AddMonoidHomClass.

[Aaron Liu]

#discr_tree_key for myInstance reveals

MulActionSemiHomClass
  (@Subtype (@LinearMap _ _ _ _ (RingHom.id _ _) _.1.1 _.1.1 _ _ _ _) <other>)
  _
  _
  (@id _)
  _.1.1
  _.1.1
  _
  _
  _

and for the other instance it is

MulActionSemiHomClass
  (@Subtype (@LinearMap _ _ _ _ (RingHom.id _ _) _.1.1 (Finsupp _ _ _) _ _ _ _) <other>)
  _
  _
  (@id _)
  _.1.1
  (Finsupp _ _ _)
  _
  _
  _

[Aaron Liu]

So presumably _.1.1 didn't match Finsupp _ _ _

[Richard Hill]

Thanks. So I guess I'll get the same problem with any representation made in the same way as leftRegular R G.
This would include things constructed as ofMulAction R G H.

Is there any way I can make the first instance more general to cover these cases?

[Matthew Ballard]

Abstraction boundaries seem to have completely collapsed here…

[Kevin Buzzard]

Matthew Ballard said:

Abstraction boundaries seem to have completely collapsed here…

I don't understand. The type of leftRegular is Rep k G as it should be. Where is the actual problem?

[Aaron Liu]

Kevin Buzzard said:

Matthew Ballard said:

Abstraction boundaries seem to have completely collapsed here…

I don't understand. The type of leftRegular is Rep k G as it should be. Where is the actual problem?

Everything's reducible all the way down to docs#ModuleCat.of, so they all get unfolded by typeclass

[Kevin Buzzard]

Maybe it's time to bite the bullet and make something irreducible and then just add more API?

[Kevin Buzzard]

Talking to Amelia and she has already done all of this (made several things irreducible, including leftRegular) and they're in a big chain of PRs which we might want to consider working on.

[Richard Hill]

can you remember which PR this is?

[Kevin Buzzard]

I've just checked that #24696 has fixed the other issue which you DMed me:

import Mathlib

variable (G R : Type) [Group G] [CommRing R] (M : Rep R G)
#synth AddCommMonoid (groupCohomology M 2)
#synth AddCommMonoid (groupCohomology.H2 M) -- works on #24696, fails on master

[Richard Hill]

Thanks, that's great news!