Typeclasses for linear maps

Stream: mathlib4

[Moritz Doll]

I have a rather annoying problem with the typeclass system, which I have a hard time finding a solution for: we have a typeclass for special functions (the Fourier transform, directional derivatives) that are linear (on bundled functions). So the current design is to have a basic class just for the notation (for example docs#FourierTransform), and then one for addition and one for scalar multiplication. In principle that should be enough, but then you end up with the problem that you can't have a general simp lemma for negation or finite sums, because you have to choose a scalar field (and simp doesn't want to do that). The obvious solutions would be to introduce more parameters in the add class to prove all of the additional lemmas in that class, but it involves proving more lemmas that are a bit silly, the other option would be to have a class with addition and smul for a fixed field (probably the reals), but that seems rather clunky. Is there any better solution? I feel like this should have come up somewhere else before.

[Martin Dvořák]

I don't understand what you say. Linear map is a structure, not a class. Are you suggesting it should be a class?

[Moritz Doll]

No, I am using classes for specific linear maps. The class FourierTransform E F says that there is a map E → F called the Fourier transform (whatever that is) and we have notation 𝓕 f for f : E. Then there are additional type classes that state algebraic properties of 𝓕, which amount to it being a continuous linear map. These additional type classes are a bit of a pain.

[Jireh Loreaux]

Moritz Doll said:

you can't have a general simp lemma for negation or finite sums, because you have to choose a scalar field

This doesn't make sense to me. Can you show me the problem?

[Moritz Doll]

docs#FourierTransform.fourier_zero shows the problem: the theorem needs a ring, but obviously the ring does not play a role.

[Kevin Buzzard]

Can you make FourierTransform E F an instance of docs#ZeroHomClass ?

[Moritz Doll]

I don't know how that could work since FourierTransform E F is a class and FourierTransform.fourier is a function, not a type. I guess I would have to wrap it in a set type or something?

[Kevin Buzzard]

Hmm yes it doesn't quite fit does it :-/

[Edward van de Meent]

i guess this just suggests we need a FourierZero class (and FourierInvZero class)? or is this a silly suggestion?

[Edward van de Meent]

at the very least this would seem to be the way the current design around FourierTransform suggests to fix this issue...

[Moritz Doll]

Yeah, this would be a solution, but it feels like a lot of overhead when in the end you construct the Fourier transform as a (continuous) linear map or linear isometry. Especially, since it would end up declaring a lot of instances in each applications. I would love to have a solution with less boilerplate in each application.

[Jireh Loreaux]

@Moritz Doll why do you need the Semi veresions of everything in FourierTransform.fourier_zero? Are you ever working in settings where E or F is not and AddGroup? If not, then just switch to that and then:

import Mathlib.Analysis.Fourier.Notation

variable {E F : Type*} [AddGroup E] [AddGroup F] [FourierTransform E F] [FourierAdd E F]

open scoped FourierTransform

@[simp]
lemma fourier_zero : 𝓕 (0 : E) = 0 := by
  apply add_left_cancel (a := 𝓕 (0 : E))
  simp [← FourierAdd.fourier_add]

@[simp]
lemma fourier_neg (x : E) : 𝓕 (-x) = -(𝓕 x) := by
  apply add_left_cancel (a := 𝓕 x)
  simp [← FourierAdd.fourier_add]

[Jireh Loreaux]

I mean, really this is just saying that an AddHom between additive groups is an AddMonoidHom.

[Jireh Loreaux]

I've been wondering whether we should go back to having an IsAddMonoidHom type class that takes an individual morphism, but that we hardly ever / never instantiate it globally, except for ∀ f : F, IsAddMonoidHom f, where AddMonoidHomClass F _ _. But the point would be that we can have local or scoped instances like IsAddMonoidHom 𝓣.

[Moritz Doll]

Do we have the upgrade from AddHom to AddMonoidHom? That would be enough to have all of the lemmas as term one-liners, which I think is good enough for the moment.

[Moritz Doll]

Alternatively, we could add

import Mathlib.Algebra.Group.Hom.Defs

variable  {G H F : Type*}
  [FunLike F G H] [AddGroup G] [AddGroup H] [AddHomClass F G H] (f : F) (a : G)

@[simp]
theorem map_zero' (f : F) (a : G) : f 0 = 0 := by
  apply add_left_cancel (a := f (a : G))
  simp [← map_add]

@[simp]
theorem map_neg' (f : F) (a : G) : f (-a) = -f a := by
  apply add_left_cancel (a := f (a : G))
  simp [← map_add, map_zero' f a]

[Moritz Doll]

@Jireh Loreaux do you have a preference here? (just adding a few lemmas vs a definition for upgrading an AddHom to an AddMonoidHom?)

[Moritz Doll]

#34283

[Eric Wieser]

docs#AddMonoidHom.mk'

[Moritz Doll]

Perfect - that makes the PR obsolete :tada:

[Jireh Loreaux]

Sure, with Lean Together going on I missed this.

[Moritz Doll]

No worries. Also thank you (and of course also Patrick, Markus and Remy) so much for organizing the meeting