Question about to_additive

Stream: general

[Wang Jingting]

When we are working on non-Abelian group cohomology (#31613), we realized that we need to develop a corresponding set of API for groups acting on multiplicative groups. So I tried using to_additive, but couldn't make it work on the following basic example. Could anyone help me on this? Thanks!

import Mathlib

attribute [to_additive existing (dont_translate := M) (relevant_arg := N) DistribMulAction]
  MulDistribMulAction

/-- Equivariant monoid homomorphisms. -/
@[to_additive (dont_translate := M N) (relevant_arg := A) DistribMulActionHom]
structure MulDistribMulActionHom {M : Type*} [Monoid M] {N : Type*} [Monoid N] (φ : M →* N)
    (A : Type*) [Monoid A] [MulDistribMulAction M A] (B : Type*) [Monoid B] [MulDistribMulAction N B]
    extends A →ₑ[φ] B, A →* B

notation:25 (name := «MulDistribMulActionHomIdLocal≺»)
  A " →*[" M:25 "] " B:0 => MulDistribMulActionHom (MonoidHom.id M) A B

section mwe

variable (G : Type*) [Group G]

/-- The addsubgroup of `A` consisting of elements invariant under `G`-action. -/
def H0 (A : Type*) [AddGroup A] [DistribMulAction G A] : AddSubgroup A where
  carrier := setOf fun v => ∀ g : G, g • v = v
  add_mem' := by simp +contextual
  zero_mem' := by simp
  neg_mem' := by simp +contextual

/-- The subgroup of `A` consisting of elements invariant under `G`-action. -/
@[to_additive existing (dont_translate := G) (relevant_arg := A) H0]
def MulH0 (A : Type*) [Group A] [MulDistribMulAction G A] : Subgroup A where
  carrier := setOf fun v => ∀ g : G, g • v = v
  mul_mem' := by simp +contextual
  one_mem' := by simp
  inv_mem' := by simp +contextual

variable {G}

/-- `f : A →+[G] B` induces a homomorphism `H0 G A →+ H0 G B`. -/
def H0.map {A B : Type*} [AddGroup A] [AddGroup B]
    [DistribMulAction G A] [DistribMulAction G B]
    (f : A →+[G] B) : H0 G A →+ H0 G B := sorry

set_option trace.translate_detail true
/-- `f : A →*[G] B` induces a homomorphism `MulH0 G A →* MulH0 G B`. -/
@[to_additive existing (attr := simp) (dont_translate := G) (relevant_arg := A)]
def MulH0.map {A B : Type*} [Group A] [Group B] [MulDistribMulAction G A]
  [MulDistribMulAction G B] (f : A →*[G] B): MulH0 G A →* MulH0 G B := sorry

end mwe

The code reported that to_additive didn't translate the target type from MulH0 G A →* MulH0 G B to H0 G A →+ H0 G B, instead it tried to translate to H0 G A →* H0 G B. How could I make this work? (I tried suggestions in the troubleshooting section of to_additive, but failed to fix this)

[Kevin Buzzard]

A general design question: are you planning on sticking to low degree n<=2?

[Floris van Doorn]

I didn't investigate, but I think this is a limitation of the to_additive heuristic.
The domain and codomain of the MulHom contain G, which you asked not to translate, and therefore the heuristic thinks that MulHom shouldn't be translated.

Maybe @Jovan Gerbscheid has an idea on how to deal with this case.

[Wang Jingting]

Kevin Buzzard said:

A general design question: are you planning on sticking to low degree n<=2?

Well, according to the book Local Fields by Serre (GTM 67), group cohomology can only be defined for n = 0, 1 when the group is not necessarily commutative (the long exact sequence extends to the commutative version of H^2(G, A) under certain conditions)

[Wang Jingting]

Floris van Doorn said:

I didn't investigate, but I think this is a limitation of the to_additive heuristic.
The domain and codomain of the MulHom contain G, which you asked not to translate, and therefore the heuristic thinks that MulHom shouldn't be translated.

Maybe Jovan Gerbscheid has an idea on how to deal with this case.

I agree with you on the interpretation of the error message, but I have the feeling that the heuristic could probably be changed into the following procedure: It looks at MonoidHom (MulH0 G A) (MulH0 G B), find that MulH0 G A would be translated, and the relevant_arg for MonoidHom is the first argument, so MonoidHom would also be translated.

[Jovan Gerbscheid]

When I copy the code into lean web, I don't see an error?

[Wang Jingting]

Jovan Gerbscheid said:

When I copy the code into lean web, I don't see an error?

Wait, that's weird, I'm pretty sure it has an error when I posted this. (and you can see that others have seen the error as well) But anyway, thanks, I'll merge master in my PR and start working on it again. Hopefully it'll work this time.