continuous semi-algebra maps

Stream: Is there code for X?

[Kevin Buzzard]

If $K$ and $L$ are number fields with $L$ a $K$-algebra, and if $w$ is a place of $L$ dividing a place $v$ of $K$ (i.e. $v$ is the pullback of $w$ to $K$), then there is a canonical inclusion of the completions $K_v\to L_w$ extending the canonical map $K\to L$. This map is a continuous semilinear algebra morphism and my instinct is that what I've just said is by far the nicest way to express what is going on. But we don't even have semilinear algebra morphisms in Lean, let alone continuous ones.

Should I encourage someone to set up all the machinery of semilinear algebra maps, semilinear algebra map classes, continuous semilinear algebra maps and continuous semilinear algebra map classes? (or am I blind and we have some or all of these already?) Could we envisage having all of this in mathlib? It's probably worth flagging that semilinear algebra maps are what looks to me like a nice way of encoding commutative squares where the vertical maps are algebraMap (which is often the case, for example in the AKLB set-up we have K an A-algebra and L a B-algebra, and we're currently expressing commutativity of the square with two IsScalarTower instances).

[Eric Wieser]

Semilinear algebra maps don't work so well for when there are two connected commutative squares, right?

[Michael Stoll]

What is the "semi" here in "semilinear"?

[Kevin Buzzard]

Eric Wieser said:

Semilinear algebra maps don't work so well for when there are two connected commutative squares, right?

We have docs#LinearMap.comp which is composition of semilinear maps, I can't imagine that demanding that the top maps preserve multiplication will be any different? Or are you stacking the squares vertically? In the examples coming from adeles the stacking is horizontal like in the linear map case.

[Kevin Buzzard]

Michael Stoll said:

What is the "semi" here in "semilinear"?

Sorry, I realise I didn't even mention that we already have semilinear maps and continuous semilinear maps in mathlib. I guess I mean "semialgebra maps"?

The map $K_v\to L_w$ is semilinear in the sense that the square with this on the top and $K\to L$ on the bottom commutes. See the definition of docs#LinearMap (note the presence of two base rings and notation →ₛₗ[σ]). See https://arxiv.org/abs/2202.05360 for the story of the formalization.

[Kevin Buzzard]

In FLT at the minute, in the nonarch case, I'm expressing that the square with $K_v\to L_w$ and $K\to L$ commutes by artificially making $L_w$ into a $K$-algebra (it's already an $L$-algebra), demanding the IsScalarTower instance making the triangle commute, and then saying that the map is $K$-linear. For this to even make sense we have to have $L$ a $K$-algebra rather than just a morphism of rings. It just occurred to me today when thinking about the infinite case that a much more conceptual way of stating this would be just by showing that the map $K_v\to L_w$ is semilinear wrt $K\to L$.

[Jireh Loreaux]

I was hoping we could get away without semilinear algebra maps, but since you have a use case, then I think we should develop them. There is also another use case I know about (the modular conjugation operator in Tomita-Takesaki theory), but it's sufficiently specialized that it probably could be it's own thing if semilinear algebra maps weren't need elsewhere.

[Antoine Chambert-Loir]

When I had developed the semilinear maps of actions, I had refactored the semilinear maps of modules, but I had noticed that the semi-linear extension stopped just before the algebra map. Of course, the docs#IsScalarTower is more or less playing the same game and the interaction between the two will have to be clarified.

[Kevin Buzzard]

One difference is that if I want different maps $K\to L$ then I'm in trouble with IsScalarTower because it wants [Algebra K L] (well, it wants SMul K L but in practice this is coming from Alegbra K L).