making a topological ring

Stream: maths

[Kevin Buzzard]

I have a base commutative ring R (in the application it is a field) and a a commutative R-algebra A which is also a topological ring. I have a (non-commutative) R-algebra D which as an R-module is free of finite rank. I want to make $H := D\otimes_RA$ into a topological ring.

The topology can be thought of in the following way: D is isomorphic to R^n as R-module so H is isomorphic to A^n as A-module and we just give it the product topology. I think that a nice way to do this in mathlib would be to use the coarsest topology which makes all the A-linear maps from H to A continuous. So far so good. Now I want to prove that addition and multiplication are continuous. I feel like this should follow from the fact that any A-linear map from A^m to A^n is continuous (erm: as Anatole points out I need a variant of this for bilinear maps). Do we have any machinery which is going to make any of this straightforward?

[Eric Wieser]

I think there are lots of other threads about putting a topology on the tensor product; perhaps your case falls out from these for "free"?

[Anatole Dedecker]

I don’t know how much this is connected to the general theory of topological tensor products, which tend to be in a more restricted generality (e.g with a normed field as scalar ring).

[Anatole Dedecker]

So I don’t know if it is mathematically the best approach, but I think there will be no obstruction from the Lean side here as long as you’re ready to manipulate topologies here. Notably, docs#LinearMap.continuous_on_pi seems like it would be helpful.

[Anatole Dedecker]

There’s basically no work to do in order to get the axioms of topological module (see docs#topologicalAddGroup_iInf and docs#topologicalAddGroup_induced for example)

[Anatole Dedecker]

Now the issue I could see with multiplication is that it’s not linear but bilinear, so you may have to redo the argument of docs#LinearMap.continuous_on_pi, but I think that will work.

[Anatole Dedecker]

Aha, but multiplication won’t be A-bilinear since A is not commutative! I think this is where troubles will appear.

[Anatole Dedecker]

(And I mean mathematical troubles)

[Kevin Buzzard]

A is commutative, don't worry :-) It's D that's not commutative

[Kevin Buzzard]

R is a number field, A is the finite adeles of (the integers of) R and D is a quarternion algebra over R in the application.

[Kevin Buzzard]

So perhaps this is the challenge (note: I don't have a maths proof):

import Mathlib.LinearAlgebra.FreeModule.Basic
import Mathlib.Topology.Algebra.Ring.Basic
import Mathlib.RingTheory.Finiteness

theorem LinearMap.continuous_on_bilinear {ι κ : Type*} {R : Type*} {M : Type*}
    [Finite ι] [Finite κ] [CommSemiring R] [TopologicalSpace R] [AddCommMonoid M] [Module R M]
    [TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M]
    (f : (ι → R) →ₗ[R] (κ → R) →ₗ[R] M) :
    Continuous (fun xy ↦ f xy.1 xy.2 : (ι → R) × (κ → R) → M) := sorry

[Anatole Dedecker]

The maths proof is "write f as its matrix, i.e write it as a linear combination of products of projections, and use that projections are continuous" (so you need the R in this lemma, which is the A in the general setup, to have continuous multiplication, but IIUC this is not an issue).

[Anatole Dedecker]

I can write all of this in Lean a bit later today, but if someone can beat me to it I’d be happy as well.

[Kevin Buzzard]

I've done the sorry above (modulo adding the assumption that multiplication on R was continuous) so hopefully I'm in good shape now. Thanks for your help!

[Kevin Buzzard]

OK so this is a really funky little API.

The story is this. Let $A$ be a commutative topological ring. Then for any abstract $A$-module $M$ you can put a "canonical" topology on $M$, defined to be the inf of the induced (pullback) topologies that you get from all A-linear maps from M to A. In other words, the canonical topology on $M$ is the coarsest topology such that all A-linear maps M -> A are continuous.

I've proved that if M and N are A-modules and if you put the canonical topology on both M and N then every A-linear map is continuous. Hence if M -> N is an isomorphism, it's a homeomorphism. I've proved that if M = A^n then the topology is the product topology.
Next up: if D is an A-algebra (not necessarily commutative) which is finite and free as an A-module, then the topology makes D into a topological ring. I've also proved (see above) that if f : A^n x A^m -> M is bilinear then it's continuous, and in retrospect it looks like I should have proved that if M x N -> P is bilinear then it's continuous.

Presumably I'm reinventing the wheel (although it entertained me on a long train journey...)

[Anatole Dedecker]

By the way I forgot to tell you that we have a name for this "canonical" topology using docs#WeakBilin (searching the docs is a nightmare right now so I can’t write the exact spelling), which will give you the module instances for free. But indeed what you describe is precisely what I had in mind and I’m glad there’s no hidden issue.

[Anatole Dedecker]

Oh, except that the way I imagined proving that all linear maps are continuous for these canonical topologies was by going first reducing to products and then using docs#LinearMap.continuous_on_pi, but of course you don’t need that :face_palm: and it would impose unnecessary assumptions

[Anatole Dedecker]

So now I guess the question, since linear maps are continuous without assuming free and finite, is it the case for bilinear maps ? I’m guessing the answer has to be no even in infinite dimensional vector spaces.

[Anatole Dedecker]

At least the naive way doesn’t work : it’s easy to build an example of a bilinear form which is not a finite combination of products of linear forms

[Kevin Buzzard]

I just gave continuity of bilinear maps to a couple of undergraduates to work on :-)

[Kevin Buzzard]

Here's what I know: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT%2FHIMExperiments%2Fmodule_topology.lean

[Kevin Buzzard]

The sorries are exercises. One consequence of the sorries is that if A is a topological comm ring and D is an A-algebra then the module topology on D turns D into a top ring.

[Adam Topaz]

/-- The "canonical topology" on a module `M` over a topological ring `A`. It's defined as
the weakest topology on `M` which makes every `A`-linear map `M → A` continuous. -/
-- make it an abbreviation not a definition; this means that Lean "prints `Module.topology`
-- in the tactic state for the human reader" but interally is syntactically equal to
-- to the `iInf`, meaning that all the `iInf` rewrites still work.
abbrev Module.topology : TopologicalSpace M :=
-- Topology defined as greatest lower bound of pullback topologies. So it's the biggest
-- topology making all the `f`s continuous.
  ⨅ (f : M →ₗ[A] A), TopologicalSpace.induced f inferInstance

Is this really the right definition? I would imagine that one should take linear maps to quotients of $A$, not just $A$ itself.

[Kevin Buzzard]

Adam I have no idea, I'm just making stuff up. You want quotients by closed ideals or all ideals? I guess you're pointing out that if $A$ is a topological ring then you think $A/I$ deserves to get a topology, but there might well be no maps to $A$.

I need some definition which gives me that if $D$ is a quaternion algebra over a commutative topological ring (and so in particular free of rank 4) then $D$ inherits the structure of a topological ring, in a way which is sufficiently natural that the proofs aren't horrible. My proof still isn't sorry-free but I've got @Hannah Scholz and @Ludwig Monnerjahn working on it in Bonn :-)

[Anatole Dedecker]

Kevin Buzzard said:

Here's what I know: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT%2FHIMExperiments%2Fmodule_topology.lean

Now that you've done all of this I feel really bad for not telling you earlier about docs#WeakBilin ...

[Anatole Dedecker]

I still have no hope for Module.continuous_bilinear to be true without strong extra assumptions, but I have no counterexample yet.

[Adam Topaz]

Kevin Buzzard said:

Adam I have no idea, I'm just making stuff up. You want quotients by closed ideals or all ideals? I guess you're pointing out that if $A$ is a topological ring then you think $A/I$ deserves to get a topology, but there might well be no maps to $A$.

I need some definition which gives me that if $D$ is a quaternion algebra over a commutative topological ring (and so in particular free of rank 4) then $D$ inherits the structure of a topological ring, in a way which is sufficiently natural that the proofs aren't horrible. My proof still isn't sorry-free but I've got Hannah Scholz and Ludwig Monnerjahn working on it in Bonn :-)

For free modules, I think your definition is perfectly fine. And yes, the concern is that $A/I$ should get a topology, and there may be no maps to $A$ (in general the module may have some torsion, etc.). I this that in general when you have a good duality theory for $M$ with maps to $A$ then the definition you give would work. I think you can focus just on closed ideals, or for an arbitrary ideal $I$ take the finest topology on $A/I$ making the projection $A \to A/I$ continuous

[Anatole Dedecker]

Adam I don't understand your last sentence, in any case you want the quotient topology on $A/I$, wether $I$ is closed or not, right ?

[Adam Topaz]

I'm not sure if it's the same (my guess is that it's not unless the ideal is closed).

[Adam Topaz]

But I think you want the quotient to be the correct (categorical) quotient, and I think taking the finest topology where the projection is continuous would give you that.

[Anatole Dedecker]

What you wrote is precisely the definition of the quotient topology.

[Adam Topaz]

Oh, of course... I'm being dumb.

[Adam Topaz]

oh wait... it's not clear that this is a ring topology on $A/I$.

[Kevin Buzzard]

Another pathology is that if you give $\Z$ the discrete topology then the module $\mathbb{Q}$ gets the indiscrete topology :-)

[Adam Topaz]

I guess what I had in mind is to take the finest ring topology making the map continuous, but it's not clear that such a thing is well-defined.

[Adam Topaz]

Oh, maybe it works out... If you call the map $f : A \to A/I$ then it turns out to be open since $f^{-1}(f(U)) = \cup_{a \in I} a + U$ which is open, and I guess from this you can show that the quotient topology is a ring topology.

[Adam Topaz]

If you want some separatedness to be inherited from $A$ then you would need $I$ to be closed.

[Anatole Dedecker]

docs#topologicalRing_quotient

[Anatole Dedecker]

Of course you need $I$ closed if you want some separation.

[Adam Topaz]

Anatole Dedecker said:

docs#topologicalRing_quotient

Now I'm really convinced!

[Adam Topaz]

Kevin Buzzard said:

Another pathology is that if you give $\Z$ the discrete topology then the module $\mathbb{Q}$ gets the indiscrete topology :-)

Yeah, this is also a "problem" isn't it? I guess that allowing for quotients would give a good topology for finitely-generated modules.

[Adam Topaz]

What about the "cocanonical" topology?

variable (A M : Type*) [CommRing A] [TopologicalSpace A] [TopologicalRing A]
  [AddCommGroup M] [Module A M]

def Module.cocanonicalTopology : TopologicalSpace M :=
  ⨆ m : M, TopologicalSpace.coinduced (fun a : A => a • m) inferInstance

[Antoine Chambert-Loir]

I'm annoyed by the fact that if F is a valued field, the equivalence of all topological vector space topologies on a finite dimensional vector space E involves the fact that F is complete. Where would such an hypothesis appear in your description?

[Kevin Buzzard]

The approach as written now will just pick a basis and use the product topology, and will prove that this topology is independent of choice of basis.

I only want this topological ring result in the case where the module is finite and free.

[Anatole Dedecker]

Antoine Chambert-Loir said:

I'm annoyed by the fact that if F is a valued field, the equivalence of all topological vector space topologies on a finite dimensional vector space E involves the fact that F is complete. Where would such an hypothesis appear in your description?

I don’t understand the issue. What Kevin says (and I agree) is that if you can always build a functor from vector spaces to topological vector spaces by taking the weak topology for the algebraic dual. I think if you restrict the target category to weak spaces (topological vector spaces whose topology is defined by their topological dual) you even get a left adjoint to the obvious forgetful functor. But of course you need a bunch of extra things if you want true uniqueness (among T2 topologies), in this case completeness of the base field and finite dimension (and a few extra things)

[Ralf Stephan]

Sorry to hijack this thread, but I also need to make a topological ring, and I have no idea about topology whatsoever. From web search I gather that power series over topological rings (QQ, RR) are themselves t.r.s, but none of these structures in Mathlib are inheriting from TopologicalSpace?. What I need would be an example in Mathlib that I can follow for PowerSeries, or a checklist of things to be done. Can you help?

My motivation is this:

import Mathlib
set_option autoImplicit false

variable {R} [CommSemiring R]
namespace PowerSeries

noncomputable def log (f : ℚ⟦X⟧) : ℚ⟦X⟧ :=
  if (constantCoeff ℚ f ≠ 1) then 0 else
    ∑' j : ℕ, rescale (((-1) ^ j : ℚ) * ((j + 1) : ℚ)⁻¹)
      (((mk fun p => coeff ℚ (p + 1) f) * X) ^ (j + 1))

failed to synthesize
  TopologicalSpace ℚ⟦X⟧

(Feel free to move this post elsewhere)

[Antoine Chambert-Loir]

In ongoing work that we have to PR, @María Inés de Frutos Fernández and I have a topology on power series and some of its properties, in particular evaluation and substitution. But this is not in mathlib yet.

[Antoine Chambert-Loir]

(And while substitution can give a meaning to $\log(1+f)$ and $\exp(f)$ for a power series $f\in R[[T]]$ with constant term 0, we have not proved that $\log(1+(\exp(f)-1))=f$ and $\exp(\log(1+f))-1=f$.)

[Ralf Stephan]

Thanks for the info. So, for me as amateur it seems best to find lower hanging fruit, and follow the work of the professionals.

[Ralf Stephan]

@Antoine Chambert-Loir You did see the proofs at https://math.stackexchange.com/questions/4488730/composition-of-formal-power-series-of-exp-and-log?

[Antoine Chambert-Loir]

That's a complicated one. It is easier to set $f(x)=\exp(\log(1+x))$, and to differentiate to obtain $(1+x) f'(x)= f(x)$, and then to solve for the coefficients given that $f(x)=1+\cdots$.

[Ralf Stephan]

Do I understand it right that the previous posts affect power series in the analytical sense? If so, does that mean for formal power series a different structure of infinite sums is needed, in particular one that does not evaluate to some value, but possibly at most to its generating function (as a symbolic expression)?

And if so, does that special type of infinite sum exist in Mathlib? Infinite lists?

[Ralf Stephan]

import Mathlib
set_option autoImplicit false

variable {R} [CommSemiring R]
namespace PowerSeries

noncomputable def log (f : ℚ⟦X⟧) : ℚ⟦X⟧ :=
  if (constantCoeff ℚ f ≠ 1) then 0 else
    mk fun j => coeff ℚ j (rescale (((-1) ^ j : ℚ) * ((j + 1) : ℚ)⁻¹)
      (((mk fun p => coeff ℚ (p + 1) f) * X) ^ (j + 1)))

[Ralf Stephan]

So, using mk fun instead of tsum seems to be the way for formal power series. It should be possible to define operators over general formal power series with this.

[Antoine Chambert-Loir]

One of the things that the correct topology on the space of formal power series has to satisfy is indeed that a formal power series is the tsum of its components.

[Antoine Chambert-Loir]

(Maybe, @María Inés de Frutos Fernández and I should take the opportunity of next week's Formalising algebraic geometry workshop to PR this.)

[Ralf Stephan]

Antoine Chambert-Loir said:

One of the things that the correct topology on the space of formal power series has to satisfy is indeed that a formal power series is the tsum of its components.

It would help me avoid spouting nonsense if I had a reference to the connection of power series with topology. Can you please give one?

[Antoine Chambert-Loir]

Not an easy reading, but quite impossible to avoid: Bourbaki, Algebra, chapter IV, §4.