topology theorems for free via adjoint functors?

Stream: maths

[Kevin Buzzard]

Over the last few months I've been developing a theory of the docs#moduleTopology , this is a canonical topology on a module over a topological ring. One abstract definition of it is as follows: if $R$ is a topological ring then a topological module $M$ for $R$ is an $R$-module equipped with a topology such that $+:M\times M\to M$ and $\bullet:R\times M\to M$ are both continuous. There's a forgetful functor $F$ from the category of topological $R$-modules to the category of $R$-modules, and this functor has an adjoint $T$ such that $Hom(T(A),B)=Hom(A,F(B))$ (I always forget which way around these things are -- I think $T$ is a left adjoint?); this functor $T$ equips a module over a topological ring with its module topology (adjointness is basically docs#IsModuleTopology.continuous_of_linearMap ).

I'm about to launch into PRing proofs of statements such as: if two modules over a topological ring are both given the module topology, then the product topology has the module topology (and similar for finite products). But can I get such results for free from some adjoint functor nonsense argument?

[Yaël Dillies]

Product is a limit and right adjoints preserve limits. So $F(A × B) = F(A) × F(B)$. If you want $T(A × B) = T(A) × T(B)$ instead, then you need to find a left adjoint $L$ to $T$, so that $\mathrm{Hom}(L(A), B) = \mathrm{Hom}(A, T(B))$

[Johan Commelin]

Also, you will need to define the category of topological modules, and understand that what CategoryTheory thinks tje product should be, matches with what you want.

[Kevin Buzzard]

Product of modules is also a colimit so it sounds like I could do it this way? I didn't check the details though. The proof I have in FLT involves a big fight with the typeclass system so I was wondering whether this was a viable alternative. But in thinking how the category theory argument might look I realised that perhaps a type synonym in the middle of the non-category proof might save me.

[Kevin Buzzard]

I can't quite work out whether category theory not being useful here is something I should be annoyed about, or whether it's just showing my lack of understanding of all the details which would go into a category theory argument

[Yaël Dillies]

Kevin Buzzard said:

Product of modules is also a colimit

Good point, but the product of topological modules isn't a colimit, right?

[Yaël Dillies]

At least, the fact that the product of modules is a colimit is docs#LinearMap.coprodEquiv, and we don't have ContinuousLinearMap.coprodEquiv

[Yaël Dillies]

Okay well that was easy: #20016

[Kevin Buzzard]

Using a type synonym has solved my problems.

[Yaël Dillies]

For a topological $R$-module $M$, is there an easy way to construct a topological $R$-module $N$ such that $M ≅ \mathrm{Hom}(M, N)$?

[Yaël Dillies]

If so, you can chain this with coprodEquiv and get $T(A × B) = T(A) × T(B)$

[Kevin Buzzard]

Yaël Dillies said:

For a topological $R$-module $M$, is there an easy way to construct a topological $R$-module $N$ such that $M ≅ \mathrm{Hom}(M, N)$?

No that doesn't look right. Even without the topology this doesn't look right.

[Yaël Dillies]

So coyoneda doesn't hold for $\mathrm{Mod}$?

[Kevin Buzzard]

M=Hom_R(R,M) but you can't have something the other way around, if that's what you're asking.

[Kevin Buzzard]

Hom_R(M,N) for a fixed N is contravariant in M so you can't expect it to be related to M or even have a map to or from M in general. (but I don't know what "coyoneda doesn't hold for Mod" means)

[Yaël Dillies]

What I am saying is that I can prove $\mathrm{Hom}(T(A \times B), C) \cong \mathrm{Hom}(T(A) \times T(B), C)$ for all $C$, but I don't know how to get $T(A \times B) \cong T(A) \times T(B)$ from it. Unless I have misunderstood, the way to get this is the Yoneda lemma.

[Yaël Dillies]

Oh, is the idea that I set $C := T(A × B)$ and push forward the identity morphism, then set $C := T(A) × T(B)$ and pull back the identity morphism?

[Kevin Buzzard]

Just to be clear, I've now done this in a category-free way in FLT having found a way to avoid the typeclass battle (set P:= M x N with module topology, and let Lean believe that M x N has product topology)

[Adam Topaz]

I don't see how tricks with yoneda will help here. Constructing an isomoprhism between $T(A \times B)$ and $T(A) \times T(B)$ is equivalent to constructing a natural isomorphism after applying the coyoneda embedding. There is a natural morphism $T(A \times B) \to T(A) \times T(B)$ and presumably it would be easier to prove that this is an isomoprhism.

[Kevin Buzzard]

FWIW my non-category proof had some content. The key argument was proving that the identity map from (M x N, product topology) to (M x N, module topology) was continuous, which involved writing it as the function sending mn to i1(pr1(mn))+i2(pr2(mn)) where the pr's are projections from products hence continuous, the i's are inclusions M -> P (P:=MxN with module topology) are linear and hence continuous, and addition on P is continuous.

[Adam Topaz]

Note that the topology on $T(A)$ is sInf ..., and the topology on the product is ... \sqcap .... The map $T(A \times B) \to T(A) \times T(B)$ is the identity on the underlying modules, so it suffices to show that the topologies agree, and so it looks like this could be accomplished using the fact that sInf commutes with \sqcap in a suitable lattice.

[Kevin Buzzard]

This (the fact that my argument had some content) was another reason why I was interested about whether it could all be done with abstract nonsense (but not interested enough to think about it myself)

[Adam Topaz]

In fact your definition of $T(M)$ is as a limit over the diagram of all topological module structures on this fixed $M$. And since limits commute with limits, this could be a abstract-nonsense approach.

[Mitchell Lee]

It is enough to show that the direct sum of two topological $R$-modules $M$ and $N$, in the category of topological $R$-modules, is the usual direct sum $M \oplus N$ with the product topology. Then $T$ is a left adjoint, so it is right exact, so it preserves direct sums.

[Mitchell Lee]

However, it is not obvious to me whether this fact can be proved with abstract nonsense.

[Mitchell Lee]

There is also this proposition which makes it easier to prove that something is a direct sum, but I think there is still something to be done: https://ncatlab.org/nlab/show/additive+category#ProductsAreBiproducts

[Mitchell Lee]

This would also imply thay the category of topological $R$-modules is an additive category, which might be useful for other purposes.

[Mitchell Lee]

Ok, I found a lemma in mathlib that lets you do all this:

https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Preadditive/Biproducts.html#CategoryTheory.Limits.isBinaryBilimitOfTotal

[Mitchell Lee]

This can be used to prove that the direct sum (binary biproduct) of $M$ and $N$ in the category of topological $R$-modules is the Cartesian product $M \times N$ with the product topology. It might still just be easier to prove your theorems directly without category theory, though.

[Kevin Buzzard]

Mitchell Lee said:

It might still just be easier to prove your theorems directly without category theory, though.

https://github.com/ImperialCollegeLondon/FLT/blob/8a133980a700b1a25a465f08c2dec56e367ccd78/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean#L188-L221

[Mitchell Lee]

Yeah, that does look easier

[Kevin Buzzard]

FWIW here's what that proof looked like 2 days ago, and this was what inspired the question. I then had the idea of using a type synonym and all my problems evaporated.