Topology on power series

Stream: new members

[Philippe Duchon]

(Still trying to understand how things work in Mathlib, what is there and what is not)
(Also, not sure how to input Unicode characters - the VS code shortcuts don't work)

Given a variable type X and a commutative semiring R, Mathlib has power series with coefficients in R and variable set X as (X \to\0 \N)\to R -- I understand X\to\0 \N to describe monomials: function with finite support from X to \N. So far, so good.

But then, if I assume R to be a topological semiring (hence, a topological space), I would expect Lean to have an instance for TopologicalSpace (MvPowerSeries X R) (presumably via the Pi product construction), but #synth fails to find it.

So, am I looking in the wrong place, or doesn't Mathlib have any topology on power series? (I would expect a power series to be the sum of its monomial terms, which in my mind should be true - maybe with a countable variable set? - even with the discrete topology on the ring of coefficients)

Of course, Mathlib tends to do things with such generality (I never learned about filters in my youth, even though I live in Bourbaki territory), I might very well be missing important conditions, or looking in the wrong place.

[Kevin Buzzard]

Surely it's reasonable to expect that different people might want different topologies on a multi-variable power series. To take an example from number theory, there are at least three topologies on $\mathbb{\Z_p}[[T]]$ which people use -- the $p$-adic topology, the $T$-adic topology, and the $(p,T)$-adic topology. So it's probably dangerous to just make an instance in mathlib of a topology which then applies across the board. It wouldn't surprise me if mathlib has several topologies on power series but that none are activated by default. It also wouldn't surprise me if it has none. Let's try:

[Kevin Buzzard]

@loogle MvPowerSeries, TopologicalSpace

[loogle]

:shrug: nothing found

[Kevin Buzzard]

So indeed maybe there are none.

[Kevin Buzzard]

The reason #synth won't work is that this line

def MvPowerSeries (σ : Type*) (R : Type*) :=
  (σ →₀ ℕ) → R

will not be unfolded by typeclass synthesis: it can't see through the def.

import Mathlib

#synth Add ℕ -- you can add naturals

def Foo := ℕ -- Foo is the naturals

#synth Add Foo -- you can't add Foos (by default)

This is by design. For example we definitely do not want typeclass inference to see through the definition when it comes to multiplication; if R has a multiplication then for any type X, the function type X -> R will have a multiplication (pointwise), but if typeclass inference could see through the def then power series would have the wrong multiplication!

[Philippe Duchon]

Thanks! I knew (at least in some part of my head) that there were mechanisms designed so that typeclass inference would not pick the wrong instance. And of course I can imagine that people might want to use different topologies.

But then, if one were to explicitly define (name) two different topologies for the same power series space, what would theorems using them look like? Would they have to mention the topology explicitly? Could one have, say, two namespaces where there would be different "default" topologies? (of course this is no longer specific to power series and topologies, just situations where more than one instance of a given typeclass for the same types would be "natural" in different contexts)

[Kevin Buzzard]

You can make a topology a local instance and then typeclass inference only knows about it for a finite time (for example until the end of a file)

[David Loeffler]

There is an extant PR about this (#14866).

[Luigi Massacci]

Another approach is to introduce a synonym for your type, this is what is done in the case of docs#PiLp for example

[Philippe Duchon]

Luigi Massacci said:

Another approach is to introduce a synonym for your type, this is what is done in the case of docs#PiLp for example

Like: define a new name for "power series with the product topology from the discrete topology on coefficients" (formal power series), and _then_ declare an instance for this "new type"?

I get the idea - but then do you still have access to the general theorems for the original type? Or do you have to "manually convert" to the original type?

[Kevin Buzzard]

Yes, the moment you make a type synonym (like Foo above) you have to make a bunch of API for it, and the proofs are all "abuse definitional equality and deduce it from the old thing".

import Mathlib.Tactic

#synth Add ℕ -- you can add naturals

def Foo := ℕ -- Foo is the naturals

instance : Add Foo := (show Add ℕ by infer_instance)

lemma Foo.add_comm (a b : Foo) : a + b = b + a := Nat.add_comm a b -- definitional abuse
-- etc etc

[Luigi Massacci]

Philippe Duchon said:

I get the idea - but then do you still have access to the general theorems for the original type? Or do you have to "manually convert" to the original type?

As Kevin said it will cause a bit of duplication, but using things like abbrev or reducible will let a lot of tactics (though not the typeclass inference system directly) see through it, so in practice you will not have to duplicate everything (far from it in fact)

[Antoine Chambert-Loir]

In PR #14866, @María Inés de Frutos Fernández and I define the basic topology on power series, which is defined as the product topology when the coefficients are assumed to be endowed with some topology. For the reason evoked by @Kevin Buzzard , this topology is not made a global instance but can be summoned with open scoped MvPowerSeries.PiTopology (with the obvious variant for PowerSeries).

There are a few subsequent PRs that allow to evaluate power series (#15019, under good circumstances) and to make substitutions (#15158). In particular, in this last PR, which is working but probably not yet in final form, it is shown how to endow the ring of coefficients with the discrete topology.

[Jireh Loreaux]

@Luigi Massacci abbrev and reducible do let type class synthesis see through the type synonym. One quite inconvenient fact, which I found out only recently, is that Lean can even pull instances backwards through an abbrev :fear: .

[Edward van de Meent]

meaning if you have abbrev Foo := Bar and an instance for Foo, lean is able to synthesise that instance for Bar?

[Jireh Loreaux]

import Lean

#synth Add Nat -- `instAddNat`

abbrev Foo := Nat

#synth Add Foo -- `instAddNat` still found

class Bar (α : Type) where

instance : Bar Foo where

#synth Bar Nat -- `instBarFoo` oh no!

[Jireh Loreaux]

The context in which I discovered this is that I wanted to make a type synonym for matrices with a specified norm (or rather, Frédéric Dupuis did). Since the matrices don't already have a norm, that's great! So I thought, we can just make an abbrev and get everything we want for free, and then just add the norm instance on the new type. But then after some headaches with a proof, I learned that Lean was inferring the new norm instance on Matrix.

[Luigi Massacci]

Jireh Loreaux said:

Luigi Massacci abbrev and reducible do let type class synthesis see through the type synonym. One quite inconvenient fact, which I found out only recently, is that Lean can even pull instances backwards through an abbrev :fear: .

:scream: TIL I guess it’s one of those things I always believed for some reason so never bothered to check

[Philippe Duchon]

Antoine Chambert-Loir said:

In PR #14866, María Inés de Frutos Fernández and I define the basic topology on power series, which is defined as the product topology when the coefficients are assumed to be endowed with some topology.

Thanks @Antoine Chambert-Loir ! With some luck, I'll even manage to understand how it all works (meaning, the difference between the discrete case, which I had in mind, and the more case of a more general topology on the coefficients).

Any idea when this will make its way into Mathlib?

[Riccardo Brasca]

#14866 just landed!

[Antoine Chambert-Loir]

@Philippe Duchon the definition is the same: a sequence of power series $f_n$ converges to a power series $f$ if for each exponent $d$, the $$d$$th coefficients of $f_n$ converge to that of $f$ (when the topology on the coefficients is discrete, that means ultimately equal).