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.