Semilinear maps

Stream: general

[Frédéric Dupuis]

For a while now, the fact that mathlib doesn't have conjugate linear maps has been blocking progress. For example, the map that takes an operator to its adjoint on a complex Hilbert space is a conjugate linear map, and so is the Riesz representation. This also prevents us from developing the orthogonal group, the unitary group, etc, properly. (See here for a discussion of this issue.)

Last October, @Yury G. Kudryashov proposed a solution involving redefining linear maps to be semilinear maps. A semilinear map f is a map from an R-module to an S-module with a ring equivalence σbetween R and S, such that f (c • x) = (σ c) • (f x). If we plug in the identity into σ, we get regular linear maps, and if we plug in the complex conjugate, we get conjugate linear maps. There are also other examples (e.g. Frobenius-linear maps) where this is useful which are covered by this general formulation.

Now, together with @Heather Macbeth and @Rob Lewis , we have implemented this idea on a ~1-month old version of mathlib! The result can be found on branch semilinear-option2. The main issue that we had to overcome involved composition of such maps, and symm for linear equivalences: having things like σ₁₂.trans σ₂₃ or σ.symm in the types of semilinear maps creates major problems. For example, we want the composition of two conjugate-linear maps to be a regular linear map, not
a conj.trans conj-linear map. To solve this issue, following a discussion from back in January, we created two typeclasses to make Lean infer the right ring equivalence. The first one is [ring_equiv_comp_triple σ₁₂ σ₂₃ σ₁₃] which expresses the fact that σ₁₂.trans σ₂₃ = σ₁₃, and the second one is [ring_equiv_inv_pair σ₁₂ σ₂₁] which states that σ₁₂ and σ₂₁ are inverses of each other. Note that (again following @Yury G. Kudryashov 's idea) we have introduced notation to ensure that regular linear maps can still be used as before, i.e. M →ₗ[R] N still works as before to mean a regular linear map.

This mostly works well (maybe even surprisingly so!). Regular linear maps work essentially the same as
before, and we have a proof-of-concept file that shows how it handles conjugate-linear maps (linear_algebra/conjugate_linear.lean).

Now, even though overall it works quite well, there is still a small cost to be paid:

1. We have phased out the notation M →ₗ N (where the ring is not specified).
2. When defining a regular linear map directly using the structure (i.e. when specifying to_fun, map_smul' and so on), there is a ring_equiv.refl that shows up in map_smul'. This can mostly be dsimp'ed away, but is mildly annoying.
3. Elaboration seems slightly more brittle, and it fails a little bit more often than before. For example, when f is a linear map and g is something that can be coerced to a linear map (say a linear equiv), one has to write ↑g to make it work, or sometimes even to add a type annotation. This also occurs when using trans twice (i.e. e₁.trans (e₂.trans e₃)). To mitigate this problem, we have added new notation for composition of regular linear maps (∘ₗ for comp and ≫ₗ for trans). (Note that this is only provided to fix occasional elaboration issues and we don't necessarily expect this to replace comp and trans.)
4. It seems to exacerbate the bug discussed here for reasons that we don't understand all that well right now. It manifests itself in very slow calls to the tactic ext, and the quick fix is to manually use the right ext lemma.
5. A few random other issues that didn't arise often enough to see a pattern.

We would of course be very interested in PRing this to mathlib, and since this is such a big change we would like to solicit discussion here before actually going through with this.

Any thoughts?

[Patrick Massot]

Point 1 is no issue at all. I didn't even remember that notation existed. Point 2 seems very minor. Points 3 to 5 are extremely hard to evaluate without using the new setup.

[Patrick Massot]

Note also that the elaboration issue may change in Lean 4. I have no idea whether it would become better or worse.

[Adam Topaz]

Is there a particular reason why you want to use a ring equivalence as opposed to just a ring hom?

[Heather Macbeth]

@Adam Topaz Semilinear maps over a ring hom behave badly for certain constructions, in particular docs#submodule.map and docs#linear_map.range. It's not impossible to do the generalization to ring homs, but it's a lot less lightweight.

[Adam Topaz]

I'm mostly thinking of some examples from number theory... for example you might want to consider Frobenius semilinear maps over a non-perfect field.

[Adam Topaz]

It would be a shame to do such a massive refactor only to find out that it's not general enough to cover natural examples

[Heather Macbeth]

In particular, whenever map or range appear in a proof, you have to bump up your assumptions to the ring hom being a ring equiv (well, a one-sided equiv is enough ...). So you get include ... and omit ... everywhere.

[Heather Macbeth]

I tried it at branch#semilinear5 if you're curious. (see this commit
https://github.com/leanprover-community/mathlib/commit/a3a1cfc7accf602f92cd5e0e52a72bfce4735072 ) ... but got bored halfway through linear_algebra.basic

[Heather Macbeth]

Adam Topaz said:

It would be a shame to do such a massive refactor only to find out that it's not general enough to cover natural examples

I don't think the current version would preclude generalizing further to ring homs someday; the two tasks are basically independent. One mathlib has the ring equiv generalization, if you want to further generalize to ring homs, find-and-replacing most of the R ≃+* R₂ in the library to R →+* R₂ is the easy part, the hard part is fixing every proof involving map.

[Eric Wieser]

Why would you need include / omit vs just a cast from a ring_equiv to a ring_hom?

[Anatole Dedecker]

Yes that's what I was about to say. How hard would it be to setup the def to use ring_hom and then for the annoying lemmas you assume it's the coercion of some ring_equiv ?

[Heather Macbeth]

You still have to fix every annoying lemma separately, and that's the big task. Because in some sections of the library the needs-fixing lemmas are closely interspersed with the don't-need-fixing lemmas.

[Eric Wieser]

I have a hunch it might be best to setup the def to take just a plain function, for unification reasons

[Anatole Dedecker]

Oh okay I see the issue with include and omit now

[Frédéric Dupuis]

You would also have to be very careful to ensure that regular linear maps are defined with σ being the coercion from a ring_equiv.refl to a ring_hom and not a ring_hom.id. I'm not sure how annoying this would get.

[Adam Topaz]

docs#submodule.map should work whenever you're semilinear over a surjective ring hom. So again even for map using an equivalence is possibly not the right generalization (in my opinion)

[Heather Macbeth]

Right, this is what I was getting at with "one-sided equiv"

[Heather Macbeth]

Adam Topaz said:

I'm mostly thinking of some examples from number theory... for example you might want to consider Frobenius semilinear maps over a non-perfect field.

In this example, are the ring homs surjective?

[Adam Topaz]

No.

[Heather Macbeth]

So presumably one never uses the map construction for them anyway (i.e., we don't know a use case where we'd want map for semilinear maps over a surjective, non-bijective ring hom).

[Eric Wieser]

Frédéric Dupuis said:

You would also have to be very careful to ensure that regular linear maps are defined with σ being the coercion from a ring_equiv.refl to a ring_hom and not a ring_hom.id. I'm not sure how annoying this would get.

This is what I was referring to when I said
Eric Wieser said:

I have a hunch it might be best to setup the def to take just a plain function, for unification reasons

You're correct that ↑ring_equiv.refl = ring_hom.id is problematic as it is not true by rfl, but ⇑ring_equiv.refl = ⇑ring_hom.id does not suffer from the same problem.

[Eric Wieser]

Heather Macbeth said:

You still have to fix every annoying lemma separately, and that's the big task. Because in some sections of the library the needs-fixing lemmas are closely interspersed with the don't-need-fixing lemmas.

If we get the generality of the definition right we can always relax the lemmas about it later

[Heather Macbeth]

Eric Wieser said:

You're correct that ↑ring_equiv.refl = ring_hom.id is problematic as it is not true by rfl, but ⇑ring_equiv.refl = ⇑ring_hom.id does not suffer from the same problem.

Frederic was responding to Anatole's comment. The natural way in our formalism would be neither, but instead to use two ring homs together with

class ring_equiv_inv_pair : Prop :=
(is_inv_pair₁ : σ'.comp σ = ring_hom.id R₁)
(is_inv_pair₂ : σ.comp σ' = ring_hom.id R₂)

[Eric Wieser]

I guess the idea for writing lemmas that match A →ₗ[⇑σ] B or A →ₗ[↑σ] B would work for the σ : R ≃+* R' case but not for the surjective case @Adam Topaz was thinking about, since we don't have bundled surjective maps.

[Heather Macbeth]

Eric, what problem are you trying to address exactly? The experiment I tried at
https://github.com/leanprover-community/mathlib/commit/a3a1cfc7accf602f92cd5e0e52a72bfce4735072
failed for lack of energy, not because there was any technical problem.

[Heather Macbeth]

If we really want to allow for surjective rather than bijective ring homs in submodule.map, then split my typeclass above as

class ring_equiv_inv_pair_left : Prop :=
(is_inv_pair₁ : σ'.comp σ = ring_hom.id R₁) -- `σ` has a left inverse

class ring_equiv_inv_pair_right : Prop :=
(is_inv_pair₂ : σ.comp σ' = ring_hom.id R₂) -- `σ` has a right inverse

and use only the appropriate one.

[Eric Wieser]

I'm just exploring the consequences of Adam's suggestion to use ring_homs, because it was my first thought too. I haven't made any attempt at actually trying to do it or thought of a particularly compelling reason to do so.

[Heather Macbeth]

But at that commit I am using ring homs ...?

[Eric Wieser]

I think I somehow missed the message where you posted that 5 branch the first time; apologies!

[Frédéric Dupuis]

I think if we really want to have ring_homs instead of ring_equivs, we'll need to have a few more of these typeclasses to express the fact that they are surjective/bijective/whatever. Having to pass these facts as parameters to every lemma sounds untenable.

[Heather Macbeth]

@Frédéric Dupuis If we only need bijective, then nothing needs to change; we can get by with the same two typeclasses ring_equiv_comp_triple and ring_equiv_inv_pair as before, right?

[Heather Macbeth]

With ring_equiv_inv_pair expressing bijectivity.

[Frédéric Dupuis]

Well, the case where we only need bijective is basically what we've done. If we want to be able to define linear maps over any ring_hom, with lemmas that only work in specific cases (i.e. when σ is surjective bijective), then I think we need some more typeclasses.

[Adam Topaz]

Suppose that $\sigma : A \to B$ is a morphism of rings and let $B_0$ denote the image of $\sigma$.
Let $f : M \to N$ be a $\sigma$-semilinear map.
Let $H$ be an $A$-submodule of $M$. The image $f(H)$ is a $B_0$-submodule of $N$. Consider the base-change $B \otimes_{B_0} f(H)$ of this $B_0$-submodule. This is now a $B$-module, and it comes equipped with a natural morphism of $B$-modules to $N$. We can then take the image of this map. In explicit terms, this is going to be the $B$-submodule of $N$ generated by the image of $f$ as a function. I think this deserves to be the correct generalization of docs#submodule.map for a semilinear map, and it doesn't require any further assumptions on $\sigma$.

[Adam Topaz]

The carrier set will not be defeq to the image of f as a function, of course, but it will be propeq in the case where $\sigma$ is surjective.

[Heather Macbeth]

I see, so define submodule.map to have carrier span (f '' H) rather than just f '' H.

[Johan Commelin]

feat(linear_algebra): introduce notation for linear_map.comp and linear_equiv.trans #8857

is a PR by @Frédéric Dupuis that prepares the notation changes.

[Johan Commelin]

I'm in favour of making this change, but it would be good to try to align the notation as much as possible with the notation used in the category theory library.

[Eric Wieser]

What part of semilinear maps motivated the new notation?

[Heather Macbeth]

Frédéric Dupuis said:

3. Elaboration seems slightly more brittle, and it fails a little bit more often than before. For example, when f is a linear map and g is something that can be coerced to a linear map (say a linear equiv), one has to write ↑g to make f.comp ↑g work, or sometimes even to add a type annotation. This also occurs when using trans twice (i.e. e₁.trans (e₂.trans e₃)). To mitigate this problem, we have added new notation for composition of regular linear maps (∘ₗ for comp and ≫ₗ for trans). (Note that this is only provided to fix occasional elaboration issues and we don't necessarily expect this to replace comp and trans.)

[Adam Topaz]

I guess the notation hack

notation f `∘'` := f.comp

will not help at all with this elaboration issue...

[Frédéric Dupuis]

Johan Commelin said:

I'm in favour of making this change, but it would be good to try to align the notation as much as possible with the notation used in the category theory library.

Did you have any specific suggestion in mind? In any case I agree; in fact I picked ≫ₗ for trans precisely to look like the category theory notation.

[Frédéric Dupuis]

Adam Topaz said:

I guess the notation hack

notation f `∘'` := f.comp

will not help at all with this elaboration issue...

Not yet :-) But in the upcoming main PR, it will be changed to

infixr ` ∘ₗ `:80 := @linear_map.comp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
  (ring_hom.id _) (ring_hom.id _) (ring_hom.id _) ring_hom_comp_triple.ids

to hardcode the fact that both maps involved are plain linear maps.

[Johan Commelin]

Doesn't category theory use something like <<>> (but then the fancy unicode variant)?

[Adam Topaz]

See right after src#category_theory.iso.trans

[Frédéric Dupuis]

I see! I took my inspiration from src#category_theory.category_struct. Maybe the other one would be better.

[Frédéric Dupuis]

I have now changed the notation for trans to ≪≫ₗ.

[Anne Baanen]

People have had a week to complain, so now the notation is consistent, I'm going ahead and merging the PR.

[Johan Commelin]

@Heather Macbeth I'm doing some preliminary experiments with a is_tensor_product class. So far I'm mostly amazed by how often tensor products have already been used/imported in mathlib.

[Frédéric Dupuis]

I have now created the main PR for this: #9272. The main change since the discussion here is that we made it work with ring_homs instead of ring_equivs. The diff looks huge but it's not as bad as it looks: almost all of the meat is in algebra/module/basic and linear_algebra/basic, and the rest is small routine fixes.