adding @[to_additive] to a structure

Stream: mathlib4

[Antoine Chambert-Loir]

I am trying to define the additive version of docs#MulActionHom from its definition

variable {M : Type*} {N : Type*} (φ : M → N)
variable (X : Type*) [SMul M X] (Y : Type*) [SMul N Y]

/-- Equivariant functions :
When `φ : M → N` is a function, and types `X` and `Y` are endowed with actions of `M` and `N`,
a function `f : X → Y` is `φ`-equivariant if `f (m • x) = (φ m) • (f x)`. -/
-- Porting note(#5171): this linter isn't ported yet.
-- @[nolint has_nonempty_instance]
structure MulActionHom where
  /-- The underlying function. -/
  protected toFun : X → Y
  /-- The proposition that the function commutes with the actions. -/
  protected map_smul' : ∀ (m : M) (x : X), toFun (m • x) = (φ m) • toFun x

I can add it by hand:

/-- Equivariant functions :
When `φ : M → N` is a function, and types `X` and `Y` are endowed
with additive actions of `M` and `N`,
a function `f : X → Y` is `φ`-equivariant if `f (m +ᵥ x) = (φ m) +ᵥ (f x)`. -/
structure AddActionHom {M N X Y: Type*} (φ : M → N) [VAdd M X] [VAdd N Y] where
  /-- The underlying function. -/
  protected toFun : X → Y
  /-- The proposition that the function commutes with the actions. -/
  protected map_smul' : ∀ (m : M) (x : X), toFun (m +ᵥ x) = (φ m) +ᵥ toFun x

but tagging the structure with @[to_additive AddActionHom "<adjusted docstring…>"]tells me that it needs a value,

@[to_additive AddActionHom "Equivariant functions :
When `φ : M → N` is a function, and types `X` and `Y` are endowed
with additive actions of `M` and `N`,
a function `f : X → Y` is `φ`-equivariant if `f (m +ᵥ x) = (φ m) +ᵥ (f x)`"]
structure MulActionHom where
  /-- The underlying function. -/
  protected toFun : X → Y
  /-- The proposition that the function commutes with the actions. -/
  protected map_smul' : ∀ (m : M) (x : X), toFun (m • x) = (φ m) • toFun x

and I don't understand what that means.

[Ruben Van de Velde]

I'm not sure that's supported

[Antoine Chambert-Loir]

What is “that” thing that might not be supported? — that I'm defining a structure?

[Riccardo Brasca]

Yes, I think structures have to be "additivized" by hand

[Floris van Doorn]

Yes, structures have to still be additivized by hand (for now), and tagged with to_additive after both the additive and multiplicative versions exists.

[Kevin Buzzard]

Also it looks to me like the inputs of AddActionHom are in a different order to MulActionHom (at least from the code you posted -- does phi come before or after X?)

[Antoine Chambert-Loir]

yes, that was a toy example thrown here in case people understand what happens better than me.