Additive Pontryagin dual

Stream: mathlib4

[Kevin Buzzard]

Mathlib has docs#PontryaginDual , the dual of a topological abelian (multiplicative) group, defined as the ContinuousMonoidHoms to docs#circle. But Tate's thesis is full of additive Pontryagin duals and the file hasn't been to_additivised.

There are several definitions of additive Pontryagin dual of A which spring to mind. Firstly we could definite as Additive (PontryaginDual (Multiplicative A)) which looks like a nightmare. Secondly we could define ContinuousAddChar and still use circle. But probably the most sensible approach (do others agree?) is to just use ContinuousAddMonoidHoms to an additive version of circle, which will either be $\R/\Z$ or $\R/2\pi i\Z$ (this is a design decision which might need some thought, I'm not sure). I'm hoping that with this choice, to_additive will leap into action and will keep the multiplicative and additive theory of Pontryagin duals aligned. But right now AddCircle (1 : \R) is defined as a quotient, whereas circle is defined as a submonoid of the complexes. Is this going to be an issue with to_additive?

[Floris van Doorn]

Yes, this is going to be an issue.

[Floris van Doorn]

Multiplicative and additive definitions should at least have the same number of arguments, and ideally also in the same order. circle and AddCircle do not satisfy this. They also have very different types.

[Kevin Buzzard]

Can we made some definition addCircle which will solve this problem?

[Floris van Doorn]

docs#AddCircle looks like something we can multiplicativize, i.e. define MulCircle and make AddCircle the additive version of it. If we then move to always use MulCircle/AddCircle (and not circle) we can keep the additive and multiplicative developments parallel.

[Floris van Doorn]

Though that doesn't help once you instantiate AddCircle to $\mathbb{R}/\mathbb{Z}$...

[Floris van Doorn]

We can also try to define AddPontryaginDual using AddCircle, and then manually prove a bunch of parallel lemmas about AddPontryaginDual and PontryaginDual, and align them with @[to_additive]. In that case, to_additive will be able to translate everything afterwards that doesn't use the definition of PontryaginDual (and it will break badly on everything that does).

[Floris van Doorn]

But that probably doesn't work: you want to keep using that it is defined as ContinuousMonoidHom... Maybe we can try to push the opaqueness one level deeper: define NewMulCircle and NewAddCircle, both types without arguments, prove some parallel API about them, and then let to_additive translate anything that doesn't unfold those types...
Probably still not ideal, but maybe workable?

[Kevin Buzzard]

I mentioned these ideas to the student (@Dawid Lipinski ) and he pointed out that he wants to use docs#Fourier.fourierIntegral which has AddChar embedded in it :-/ I'm now wondering if we just can't avoid a bunch of boilerplate here.

[Jireh Loreaux]

I think we have to have circle as-is for complex analysis, by the way.

[Oliver Nash]

I wonder if a useful approach here might be not to work relative to a concrete object such as docs#AddCircle or docs#circle but to any object with the right properties.

[Oliver Nash]

The circle is the unique 1-dimensional connected, compact, commutative, Lie group. We don't want to bring calculus in here so we can't use this characterisation but surely there is a convenient non-analytical characterisation.

[Oliver Nash]

The idea then would be to define:

def PontryaginDual' (A C : Type*) [Monoid A] [TopologicalSpace A]
    [CommGroup C] [TopologicalSpace C] [TopologicalGroup C]
    [CompactSpace C] [ConnectedSpace C] /- what else: how to we say 1-dimensional? -/ :=
  ContinuousMonoidHom A C

[Oliver Nash]

Sadly I had only a minute so I must now run but I will try to write more tomorrow evening if I have time.

[Thomas Browning]

What would be the advantage of writing PontryaginDual' G circle over ContinuousMonoidHom G circle? In theory we could just toadditivize ContinuousMonoidHom and state everything in terms of ContinuousMonoidHom with the typeclass assumptions that you're describing.