LinearMap name

Stream: mathlib4

[Martin Dvořák]

For more than a year, I was confused by docs#LinearMap name.
Shouldn't we rename LinearMap to SemilinearMap while preserving docs#IsLinearMap as it is?

[Yaël Dillies]

I don't think so, for the same reason that docs#Module isn't named Semimodule

[Martin Dvořák]

But there is no IsModule that would lead to confusion.

[Yaël Dillies]

I don't know what IsLinearMap is used for, so I can't vouch for it

[Martin Dvořák]

It can be used to understand what M →ₗ[R] M₂ means, while the reader is burdened by a much smaller trusted code.

[Eric Wieser]

I don't think mathlib is particularly interested in minimizing trusted code beyond trying to shorten the longest pole at compilation time

[Martin Dvořák]

OK

[Martin Dvořák]

Anyways, IsLinearMap helped me a lot in writing my Ph.D. thesis.
I wouldn't want to have to explain M →ₗ[R] M₂ though LinearMap itself.

[Martin Dvořák]

That said, if Mathlib maintainers decide that IsLinearMap should be removed, my voice will not save it, I know.

[Eric Wieser]

I could see IsLinearMap being semilinearized

[Jireh Loreaux]

Martin Dvořák said:

I wouldn't want to have to explain M →ₗ[R] M₂ though LinearMap itself.

Why not?

A linear map M →ₗ[R] M₁ between R-modules is a function f : M → Mₗ which is additive f (x + y) = f x + f y and satisfies f (r • x) = r • f x. However, in mathematics one often cares about conjugate-linear maps (i.e., where R := ℂ and f (r • x) = conj r • f x). In order to have a single concept which covers both cases, Mathlib defines docs#LinearMap in the generality of semilinear maps. In this setting, we have an R-module M and a R₁-module M₁ and a ring homomorphism σ : R →+* R₁. A map f is semilinear (denoted f : M →ₛₗ[σ] M₁) if it is additive and satisfies f (r • x) = σ r • f x. When R₁ := R and σ := .id R, then we recover the usual notion of linear map. When R := ℂ and R₁ := ℂ and σ := conj, we recover the notion of conjugate-linear maps.

[Moritz Doll]

Yaël Dillies said:

I don't know what IsLinearMap is used for, so I can't vouch for it

I am wondering about this too. The documentation says that it should be avoided, but doesn't explain why it should exist at all.

[Jireh Loreaux]

IIRC @Tomas Skrivan finds it useful for certain things, but maybe I'm wrong.

[Tomas Skrivan]

In SciLean, I use unbundled approach most of the time, I use IsLinearMap and also my own IsContinuousLinearMap. When I need to convert to a bundled morphisms I just use fun_prop.

I find it way more convenient as I don't have to remember any of the bundled morphisms API and I don't have to write code in "point free" style. All the fderiv theorems become way more readable.

I made a PR #24095 but there seemed very little interet in it so I didn't bother finishing it.