Semilinearizing

Stream: mathlib4

[Anatole Dedecker]

At the end of last week I decided to go on a semilinearizing spree:

• #24170 (ready for review) takes care of LinearAlgebra.Finsupp.Defs and LinearAlgebra.Finsupp.LSum, which means extending the universal property to semilinear maps. I will need this for the GNS constructions associated to kernels of positive type on topological spaces, and to functions of positive type on topological groups.
• #24208 (not ready yet) takes care of LinearAlgebra.BilinearMap and LinearAlgebra.TensorProduct.Basic. This one was really painful due to the length of that second file, and I still need to duplicate some constructions between linear and semilinear to make it convenient to use. This is crucially needed for tensor products of Hilbert spaces, the Stinespring and Kasparov-Stinespring constructions (which generalize GNS), and eventually tensor products of $C^\ast$-algebras.

I have two questions regarding this process:

• how much should I accept in terms of performance drop? On #24170, !bench reports significant changes, but I'm not sure how to interpret them, nor what I should do about them. Surely I shouldn't have a linear version of everything just for the sake of performance?
• More generally, I'm not sure what the guidelines are regarding "linear specialization" of semilinear statements. In #24170 I went with duplicating only thing which would make an annoying RingHom.id in rewrites, and that seems to work fine. #24208 is more tricky, because a lot of lemma which currently take an explicit ring parameter should instead take a RingHom. My guess is I should duplicate them to avoid all the (.id R) arguments?

[Anatole Dedecker]

Some random pings:

@Jireh Loreaux @Frédéric Dupuis for the applications

@Eric Wieser @Anne Baanen for the API design

@Matthew Ballard @Kim Morrison for performance

[Kevin Buzzard]

By the way, we're currently enjoying semialgebra homs in FLT

[Anatole Dedecker]

Aha! This should definitely be backported to Mathlib.

[Antoine Chambert-Loir]

In what context do they appear?
I believe that MulActionEquiv should be there as well. But an intermediate object is interesting, with an equivalence on the acted-on side, and a surjection on the monoid side.

[Kevin Buzzard]

I don't want to derail this thread but if that question was to me then $K_v\to L_w$, $K_v\to\prod_{w|v}L_w$, $\mathbb{A}_K^\infty\to\mathbb{A}_L^\infty$, $\mathbb{A}_{K,\infty}\to\mathbb{A}_{L,\infty}$ and $\mathbb{A}_K\to\mathbb{A}_L$ are all ring homomorphisms extending $K\to L$ (finite separable extension of fields of fractions of Dededkind domains) and it was convenient to carry around the fact that they all extended $K\to L$ in this way, before we tensored up and got $L$-algebra maps $L\otimes_KK_v\to\prod_{w|v}L_w$, $L\otimes_K\mathbb{A}_K\to\mathbb{A}_L$ etc etc

[Junyan Xu]

I wonder whether we should do a different generalization (to noncommutative rings) for TensorProduct simultaneously; the following would combine both generalizations, I think.
Given an R-module N, a module M over two rings S and T with SMulCommClass S T M, a U-module P, and ring homomorphisms σ from R to DomMulAct S (same as MulOpposite S as a ring) and τ from T to U, we could define a tensor product M ⊗[σ] N which inherits a T-module structure from M, and establish the adjunction (M ⊗[σ] N →ₗ[τ] P) ≃+ (N →ₗ[σ] M →ₗ[τ] P). Notice that the order of M and N are switched compared to TensorProduct.lift.equiv, but this seems unavoidable if you want the tensor product to inherit actions from the left component rather than the right component by instances.

[Anatole Dedecker]

I've thought a bit about noncommutative tensor products at some point. One thing that I think is important (EDIT: not really important, but I think it's a good idea) is not to force anything to actually be a right module, so I would say that σ should just be allowed to not be a ring homomorphism, so that it can be both the identity and MulOpposite.op.

Otherwise I think I agree with your proposal, but I think to actually use tensor products over noncommutative rings we will also have to solve the action inheritance issue: how do we allow the tensor product over B of an A-B-module and a B-C-module to come naturally with a A-C-module structure ? This happens all the time in e.g K-theory...

[Anatole Dedecker]

If you want to have a go at your generalization feel free to do so, but I don't think I'll have time for it in the near future.

[Eric Wieser]

Anatole Dedecker said:

One thing that I think is important is not to force anything to actually be a right module,

Can you elaborate on this? My take long ago was that we do want to do this, but we need to make this play better with Algebra to make it justifiable

[Anatole Dedecker]

Okay thinking back about this I realize that I may have confused two independent thoughts. What is bad is the naive "inherit left actions from the left and right actions from the right" (this comes with obvious diamonds).

But this is another question. For the question of wether we should ask the left-hand-side to be a right module, I think it was rather a personal preference ("left-right is mostly useful for humans, so we should do most things in the setting of commuting actions and leave users to choose their left and right"), and also the fact that if we want to cover the commutative case then it's nice to allow not having an artifical right-module structure.

[Anatole Dedecker]

Really the main point is that the ring-hom part in our semilinear setup is mostly useless, and we could use bare function as in docs#MulActionHom

[Anatole Dedecker]

Coming back to the subject of this thread: I know it's annoying to review, but could someone have a look at #24170 ? Thanks!

[Junyan Xu]

so I would say that σ should just be allowed to not be a ring homomorphism, so that it can be both the identity and MulOpposite.op

For a commutative ring, MulOpposite.op is a ring homomorphism (RingEquiv.toOpposite).
Tensor products over commutative and non-commutative rings would use different ring homs, but hopefully we can generalize the lemmas so they don't need to be duplicated.
In the case of induced representation (K[G] ⊗[K[H]] V, with H a subgroup of G), we can even take the ring hom to be the inclusion from K[H] into K[G] to avoid introducing a right-K[H]-module structure on K[G].

[Anatole Dedecker]

I guess this works (took me some time to understand what you meant), but if there is such a disjunction between the commutative and noncommutative case I think I'd rather have them as separate definitions

[Anatole Dedecker]

To be fair we may want to do this anyways, so maybe your approach is fine.

[Jireh Loreaux]

Anatole Dedecker said:

I think I'd rather have them as separate definitions

That seems like an awful lot of duplication. It seems to me it would be hard to keep the API in sync.

[Anatole Dedecker]

I agree, and I don't have a strong argument for the duplication, but I prefer to be pessimistic and assume that whatever we do will annoy sufficiently the commutative algbraists that we need to duplicate x)

[Anatole Dedecker]

But I'd be happy if we don't need it!

[Anatole Dedecker]

I should emphasize: I don't want to discourage anyone giving noncommutative tensor products a try. I'd be happy with anything that works, and I haven't thought about it enough to have a crystal-clear idea of what the ideal setup would be.

[Junyan Xu]

I'd aim to generalize most lemmas in the file to arbitrary σ : R →+* R₁ᵈᵐᵃ as in this commit (it's just a start, the adjunction is not yet generalized, and it doesn't include the generalization in #24208). I envision that the commutative part of the library will use σ = RingEquiv.toOpposite R while the noncommutative part will use σ = RingEquiv.opOp R, but the same lemmas would apply to them because they work for arbitrary σ.
I'm unfortunately busy this week and won't be able to get back to branch#NoncommTensorProduct until next week.

[Eric Wieser]

Why DMA and not MOP?

[Junyan Xu]

See this message: #mathlib4 > Semilinearizing @ 💬
In the adjunction (M ⊗[σ] N →ₗ[τ] P) ≃+ (N →ₗ[σ] M →ₗ[τ] P), in the RHS we want a semilinear map from N to M →ₗ[τ] P, which DomMulAct S acts on (because S acts on M) but MulOpposite S doesn't (as an instance), so σ needs to be from R (which acts on N) to DomMulAct S.
When I talked about RingEquiv.opOp R and RingEquiv.toOpposite R above, I'm abusing the defeq between DomMulAct and MulOpposite (which are defeq as rings).

[Eric Wieser]

Right, my objection was mainly because of the defeq abuse

[Raghuram]

It seems to me like there is an unavoidable issue here because some tensor products are of left R-modules and right R-modules where the right-sidedness of the latter action often doesn't come from any kind of "acting on the domain", so that it is an Rᵐᵒᵖ and not Rᵈᵐᵃ action. For example, if σ: R → S is a ring homomorphism then base-changing S ⊗[R] M would be (in the sense of the parameter σ : R →+* R₁ᵈᵐᵃ proposed above) using the Sᵐᵒᵖ action on S by right-multiplication and σ: R → S, and hence use that S = (Sᵐᵒᵖ)ᵈᵐᵃ.

To avoid this one should use σ : R →+* R₁ᵐᵒᵖ for tensor products, but we still need σ : R →+* R₁ᵈᵐᵃ for N →ₗ[σ] M →ₗ[τ] P to make sense. In summary, it seems like the tensor-hom adjunction over non-commutative rings intrinsically requires the line between ᵐᵒᵖ and ᵈᵐᵃ to be blurred, because it really uses that the action on a morphism space inherited from the action of the domain is an action of the opposite ring.

Another example of this is that although we have an example above of tensor product where the right module structure is naturally ᵐᵒᵖ, sometimes it is ᵈᵐᵃ rather than ᵐᵒᵖ. E.g., if we are considering the evaluation map (A →ₗ[R] B) ⊗[Module.End R A] A → B for R-modules A, B, then the opposite Module.End R A-module structure on A →ₗ[R] B is a ᵈᵐᵃ rather than ᵐᵒᵖ. So again either the distinction between the two has to be erased while defining one of the tensor products, or there would have to be two kinds of tensor products for ᵐᵒᵖ and ᵈᵐᵃ or something.

[Raghuram]

(Admittedly this is really about the non-commutative generalisation of tensor products rather than the semilinear generalisation.)