two module instance over ℤ

Stream: Is there code for X?

[Edison Xie]

Do we have a solution to this? Or more specifically, for a isomorphism between cohomology group, how do I get the AddEquiv version of that without causing error like below?

theorem eq_inst (M : ModuleCat ℤ): M.isModule = @AddCommGroup.toIntModule M M.isAddCommGroup := sorry

[Kevin Buzzard]

docs#ModuleCat.isModule

[Kevin Buzzard]

If you just want a proof then take everything apart; there's only one way Z can act on an additive group. Are you sure you want this though? What's the application?

[Eric Wieser]

I don't think it is possible to make this defeq

[Eric Wieser]

Subsingleton.elim _ _ should prove the theorem though

[Edward van de Meent]

a quick glance suggests there is no Subsingleton instance here, though...

[Edward van de Meent]

this should do it

instance (M : Type*) [AddCommGroup M] : Subsingleton (Module ℤ M) where
  allEq inst1 inst2 := by
    ext z m
    rw [int_smul_eq_zsmul inst1,int_smul_eq_zsmul]

[Edward van de Meent]

see also:

theorem eq_inst (M : ModuleCat ℤ) :
    M.isModule = @AddCommGroup.toIntModule M M.isAddCommGroup := by
  ext z m
  rw [int_smul_eq_zsmul M.isModule]
  rfl

[Aaron Liu]

Should that be AddCommMonoid M, or is that not a useful generalization?

[Edward van de Meent]

i don't think so? i believe the whole point is that you get -1 • x = -x

[Edward van de Meent]

so you need additive inverses

[Aaron Liu]

Then you need to derive AddCommGroup M if you don't have it already

[Aaron Liu]

from docs#Module.addCommMonoidToAddCommGroup

[Edward van de Meent]

:hmm:

[Edward van de Meent]

it does seem unidiomatic, but i guess it might work?

[Edward van de Meent]

as in, the extra cases where this would apply are unidiomatic, but it's fair to make it work then nonetheless

[Aaron Liu]

Also, you might not have any actual Module ℤ M instance yet, for example when using docs#Quotient.recOnSubsingleton or similar

[Edward van de Meent]

instance (M : Type*) [AddCommMonoid M] : Subsingleton (Module ℤ M) where
  allEq inst1 inst2 := by
    let _ := Module.addCommMonoidToAddCommGroup ℤ (M := M)
    ext z m
    rw [int_smul_eq_zsmul inst1,int_smul_eq_zsmul]

[Edison Xie]

Kevin Buzzard said:

If you just want a proof then take everything apart; there's only one way Z can act on an additive group. Are you sure you want this though? What's the application?

I'm trying to convert groupCohomology.isoH2 into an AddEquiv

[Edison Xie]

Thanks everyone!

[Kevin Buzzard]

docs#groupCohomology.isoH2

[Kevin Buzzard]

Convert it into an AlgEquiv instead

[Edison Xie]

Kevin Buzzard said:

Convert it into an AlgEquiv instead

Ah but it's an equivalence in ModuleCat?

[Kevin Buzzard]

Yes so hopefully there will be something in mathlib saying that this is the same thing as an algEquiv

[Eric Wieser]

Edward van de Meent said:

a quick glance suggests there is no Subsingleton instance here, though...

docs#AddCommGroup.uniqueIntModule

[Kevin Buzzard]

So the Unique isn't an instance for AddCommGroup and the docstring makes it clear why, but is there any argument against making the Subsingleton instance for AddCommMonoid? Part of me wonders whether it will lead typeclass inference on a merry dance but I think it won't because I'm guessing R = Int will be quick to fail.

[Eric Wieser]

I guess let's try it and see