Bounded bilinear forms

Stream: maths

[Frédéric Dupuis]

Moritz said:

I've looked at the linear algebra part of it and I feel like even that is in need of a quite significant cleanup: I think it is possible to unify bilinear_map, bilin_form and sesq_form into a single semibilin_map which has the former three as special cases. The definition could be essentially what is the definition of bilin_form but way more general (yesterday I generalized it to a bilinear map, but not with the ring homomorphism yet). the way that bilin_form is written makes it easy to extend it to a bounded bilinear form, I don't see how to do the same thing with the current definition of the bilinear map.

Is there any reason to use these over things like E →ₗ[R] F →ₗ[R] G?

[Heather Macbeth]

@Moritz I agree, that whole part of the library needs a clean-up. I think we all know this, and have been put off because it's a big task! Here are some of the design considerations that have occured to me ... what do you think? (Tagging @Frédéric Dupuis @Eric Wieser also):

1. (you mentioned this one) do we try to unite R-bilinear maps M → N → P with R-bilinear forms M → M → R?

2. do we try to make the theory parallel with R-multilinear maps Π(i : ι), M₁ i → M₂? (note: it is common in mathlib to have parallel developments of the 2-input and arbitrary-input version of something, like pi vs prod, sup vs Sup, etc; sometimes there is an effor to make these two developments exactly parallel, sometimes it's looser).

3. how do we deal with semilinearity, and in particular with the interaction between semilinearity and noncommutativity? Note that currently sesq_form is effectively for a docs#star_ring R, requiring the map be R-linear in one argument and I : R ≃+* Rᵒᵖ-semilinear in the other argument, so a full generalization would need to deal with multiple possible scalar rings (R, Rᵒᵖat least, but why not more?). Or we could just give up on the attempt to deal with noncommutativity here.

4. (maybe to be deferred to a future refactor) how does this interact with docs#inner_product_space? I think eventually it would be nice to have something like the integration library, where you can work with a particular measure if you specify it, or with some silent default measure if not -- so here there might in some cases be a silent default bilinear form, and sometimes an explicitly-specified one.

[Notification Bot]

This topic was moved here from #new members > Bounded bilinear forms by Anne Baanen

[Frédéric Dupuis]

I was also thinking about this because just yesterday I opened a PR (#10373) to allow semilinear versions of maps of type E →ₗ[R] F →ₗ[R] G, i.e. E →ₛₗ[σ] F →ₛₗ[ρ] G, with [module R₁ E], [module R₂ F] and [module R₃ G], and σ : R₁ →+* R₃, ρ : R₂ →+* R₃. As far as I can tell, this should cover pretty much all cases of interest, so I was wondering if we should just use that systematically and deprecate bilin_form and sesq_form.

[Heather Macbeth]

Interesting ... yes, it does seem to cover all cases of interest. It makes the parallel with multilinear maps Π(i : ι), M₁ i → M₂ less direct, though. (Note that eventually we want semimultilinear maps, too, or at least I do! How do we do those?)

[Frédéric Dupuis]

Heather Macbeth said:

Interesting ... yes, it does seem to cover all cases of interest. It makes the parallel with multilinear maps Π(i : ι), M₁ i → M₂ less direct, though. (Note that eventually we want semimultilinear maps, too, or at least I do! How do we do those?)

We could semilinearize multilinear maps by replacing R with an indexed family of ring homs that all go to the same output ring.

[Heather Macbeth]

But that doesn't work if (say) the output ring is sometimes R, sometimes Rᵒᵖ

[Heather Macbeth]

(For me, it would be a commutative ring, where this doesn't matter.)

[Heather Macbeth]

Maybe we need an indexed family of ring homs, all of whose output rings have actions on M₂

[Heather Macbeth]

with some compatibility condition like docs#smul_comm_class on these actions

[Frédéric Dupuis]

What do you mean "sometimes"? The output space has to be a module over some ring -- which one is it?

[Frédéric Dupuis]

Ah I see. Yes that could work.

[Heather Macbeth]

Frédéric Dupuis said:

What do you mean "sometimes"? The output space has to be a module over some ring -- which one is it?

Look at the current docs#sesq_form, which is a map M → M → R, where the R is considered as being both an R-module and an Rᵒᵖ-module, so that a sesquilinear form is R-linear in the first argument and (I : R ≃+* Rᵒᵖ)-sesquilinear in the second argument.

[Frédéric Dupuis]

Ah I see. Yeah we would need some sort of compatibility condition on the actions on the output space.

[Frédéric Dupuis]

Maybe even just having two unrelated module instances would suffice.

[Heather Macbeth]

Yes ... with the assumption of compatibility added in where actually required.

[Heather Macbeth]

Here's something that seems as general as I can make it, and which would admit an exact parallel for docs#multilinear_map:

import algebra.module.basic

variables (R₁ R₂ S₁ S₂ M₁ M₂ N : Type*)
variables [semiring R₁] [semiring R₂] [semiring S₁] [semiring S₂]
variables [add_comm_monoid M₁] [module R₁ M₁]
variables [add_comm_monoid M₂] [module R₂ M₂]
variables [add_comm_monoid N] [module S₁ N] [module S₂ N]
variables (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂)

structure bilinear_map :=
(bilin : M₁ → M₂ → N)
(bilin_add_left : ∀ (x y : M₁) (z : M₂), bilin (x + y) z = bilin x z + bilin y z)
(bilin_smul_left : ∀ (a : R₁) (x : M₁) (y : M₂), bilin (a • x) y = σ₁ a • (bilin x y))
(bilin_add_right : ∀ (x : M₁) (y z : M₂), bilin x (y + z) = bilin x y + bilin x z)
(bilin_smul_right : ∀ (a : R₂) (x : M₁) (y : M₂), bilin x (a • y) = σ₂ a • (bilin x y))

[Heather Macbeth]

(with [smul_comm_class S₁ S₂ N] added presumably for certain theorems)

[Frédéric Dupuis]

Do we actually need a structure for this? I was hoping to be able to get away with just E →ₛₗ[σ] F →ₛₗ[ρ] G, and I guess now with σ : R₁ →+* R₃ and ρ : R₂ →+* S₃, where R₃ and S₃ both have actions on G.

[Moritz]

Frédéric Dupuis said:

Moritz said:

I've looked at the linear algebra part of it and I feel like even that is in need of a quite significant cleanup: I think it is possible to unify bilinear_map, bilin_form and sesq_form into a single semibilin_map which has the former three as special cases. The definition could be essentially what is the definition of bilin_form but way more general (yesterday I generalized it to a bilinear map, but not with the ring homomorphism yet). the way that bilin_form is written makes it easy to extend it to a bounded bilinear form, I don't see how to do the same thing with the current definition of the bilinear map.

Is there any reason to use these over things like E →ₗ[R] F →ₗ[R] G?

The way this is done in bilinear_map is not really satisfying in my opinion since it treats the first and second variable differently and there is still the need for boilerplate code in that module. Another question is whether we need even more boilerplate once we want to bundle E →ₗ[R] F →ₗ[R] G with other properties such as is_bounded.

[Moritz]

Heather Macbeth said:

Here's something that seems as general as I can make it, and which would admit an exact parallel for docs#multilinear_map:

import algebra.module.basic

variables (R₁ R₂ S₁ S₂ M₁ M₂ N : Type*)
variables [semiring R₁] [semiring R₂] [semiring S₁] [semiring S₂]
variables [add_comm_monoid M₁] [module R₁ M₁]
variables [add_comm_monoid M₂] [module R₂ M₂]
variables [add_comm_monoid N] [module S₁ N] [module S₂ N]
variables (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂)

structure bilinear_map :=
(bilin : M₁ → M₂ → N)
(bilin_add_left : ∀ (x y : M₁) (z : M₂), bilin (x + y) z = bilin x z + bilin y z)
(bilin_smul_left : ∀ (a : R₁) (x : M₁) (y : M₂), bilin (a • x) y = σ₁ a • (bilin x y))
(bilin_add_right : ∀ (x : M₁) (y z : M₂), bilin x (y + z) = bilin x y + bilin x z)
(bilin_smul_right : ∀ (a : R₂) (x : M₁) (y : M₂), bilin x (a • y) = σ₂ a • (bilin x y))

This looks almost exactly what I came up with modulo the σ₁ and σ₂. Almost everything from bilin_form translates without any major changes to that definition.

[Frédéric Dupuis]

Moritz said:

The way this is done in bilinear_map is not really satisfying in my opinion since it treats the first and second variable differently and there is still the need for boilerplate code in that module. Another question is whether we need even more boilerplate once we want to bundle E →ₗ[R] F →ₗ[R] G with other properties such as is_bounded.

You can always add lemmas to "get rid" of the asymmetry, which still seems like less work that building a full API from scratch as you have to do with a structure.

[Heather Macbeth]

@Frédéric Dupuis Just for clarity let me translate your proposal into the same notation as the low-level one I wrote, I think you're suggesting

import algebra.module.linear_map

variables (R₁ R₂ S₁ S₂ M₁ M₂ N : Type*)
variables [semiring R₁] [semiring R₂] [semiring S₁] [semiring S₂]
variables [add_comm_monoid M₁] [module R₁ M₁]
variables [add_comm_monoid M₂] [module R₂ M₂]
variables [add_comm_monoid N] [module S₁ N] [module S₂ N]
variables (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂)

#check M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N

[Heather Macbeth]

When run this I hit the error

failed to synthesize type class instance for
...
⊢ module S₁ (M₂ →ₛₗ[σ₂] N)

[Heather Macbeth]

but I guess that's from not having assumed [smul_comm_class S₁ S₂ N] and also from docs#linear_map.module not having been semilinearized yet

[Frédéric Dupuis]

Yes, currently there is no module instance on E →ₛₗ[σ] F unless σ is the identity. We need to add one given an instance of [module S F].

[Heather Macbeth]

Frédéric Dupuis said:

Yes, currently there is no module instance on E →ₛₗ[σ] F unless σ is the identity. We need to add one given an instance of [module S F].

This should be added, certainly. (Is it part of your current PR?)

Regarding the point you and Moritz were discussing, I don't think I have any intuition for whether it would be better to use M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N for bilinear maps or to keep a separate definition generalizing the current docs#bilin_form ... would be curious to hear more people's opinions.

[Eric Wieser]

Whatever we do I think we want bilin_form to exist as a type, so that we have a place for dot notation for things like docs#bilin_form.nondegerate

[Eric Wieser]

Even if we just define it in terms of linear maps

[Heather Macbeth]

@Moritz By the way, inspired by Frédéric's idea, I guess E →L[𝕜] F →L[𝕜] G over normed spaces is exactly equivalent to is_bounded_bilinear_map. (The →L[𝕜] means docs#continuous_linear_map, and the equivalence between continuity and boundedness is in docs#linear_map.mk_continuous). So if you just want some effective definition to go on with, that would work ...

[Moritz]

@Eric Wieser that only seems to work if we define a structure. I tried it with a def bilin_form R M := bilin_map R R M M R, where bilin_map is defined as was written by @Heather Macbeth and I had to use the namespace bilin_map.

[Moritz]

Nevermind, I did a stupid mistake. It does work

[Moritz]

As soon as Frédéric's PR is merged I can do a refactor to the bilinear_map file, that should be easy because only one other file really depends on it

[Frédéric Dupuis]

Heather Macbeth said:

Look at the current docs#sesq_form, which is a map M → M → R, where the R is considered as being both an R-module and an Rᵒᵖ-module, so that a sesquilinear form is R-linear in the first argument and (I : R ≃+* Rᵒᵖ)-semilinear in the second argument.

BTW I have now checked this in my PR, and

example (I : R →+* Rᵒᵖ): M →ₗ[R] M →ₛₗ[I] R

typechecks.

[Heather Macbeth]

@Frédéric Dupuis did you check whether this example,

M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N

typechecks?

[Frédéric Dupuis]

It doesn't, you need that smul_comm_class instance.

[Frédéric Dupuis]

With [smul_comm_class S₂ S₁ N] it works.

[Moritz]

Frédéric Dupuis said:

With [smul_comm_class S₂ S₁ N] it works.

Doesn't that mean that we can only define bilinear forms over commutative rings? because we would need smul_comm_class R R R

[Frédéric Dupuis]

@Moritz It sounds confusing, but in the case of R and Rᵒᵖ, the smul_comm_class instance states that multiplying on the left commutes with multiplying on the right. See docs#semigroup.opposite_smul_comm_class for the relevant instance.

[Eric Wieser]

Which is exactly what you want for a conjugate-linear form, as you can pass docs#star_ring_equiv : R ≃+* Rᵐᵒᵖ as σ₂.

[Moritz]

The question was about the case of bilinear forms, so that ρ = σ = ring_hom.id R

[Moritz]

def semibilin_map (R : Type*) (R₂ : Type*) (S : Type*) (S₂ : Type*)
  [semiring R] [semiring R₂] [semiring S] [semiring S₂]
  (M : Type*) (N : Type*) (P : Type*)
  [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P]
  [module R M] [module S N] [module R₂ P] [module S₂ P]
  [smul_comm_class S₂ R₂ P]
  (ρ₁₂ : R →+* R₂) (σ₁₂ : S →+* S₂)
  := M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P

def bilin_map (R : Type*) [semiring R] (M : Type*) (N : Type*) (P : Type*)
  [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P]
  [module R M] [module R N] [module R P] [smul_comm_class R R P]
  := semibilin_map R R R R M N P (ring_hom.id R) (ring_hom.id R)

def bilin_form (R : Type*) [semiring R] (M : Type*) [add_comm_monoid M] [module R M]
  [smul_comm_class R R R]
  := bilin_map R M M R

[Moritz]

(deleted)

[Moritz]

(deleted)

[Eric Wieser]

While the current docs#bilin_form only requires semiring R, it looks like the axioms pretty much force you to have R be commutative

[Eric Wieser]

They're enough to show that (a * b) * self.bilin x y = (b * a) * self.bilin x y for all a, b, x, y, which is only a few steps away from a * b = b * a. I guess you can happily use the 0 form in the noncommutative setting, but it's pretty useless.

[Heather Macbeth]

If these sesquilinear forms are being forced to be trivial, I think something is wrong. Because apparently this definition should be interesting over noncommutative rings:
https://en.wikipedia.org/wiki/Sesquilinear_form#Over_a_division_ring

[Heather Macbeth]

(I've never used sesquilinear forms over rings other than $\mathbb{C}$, myself, but presumably some people do, and it would be a shame to rule out their use case ...)

[Eric Wieser]

I'm talking about the bilinear ones not the sesquilinear ones

[Moritz]

I made the definition for semibilinear maps in both the version, which is used in bilinear_map (with modification that it is now a structure, so that we can use namespaces) as well as bilinear_form:
https://gist.github.com/mcdoll/7bd87a9a3e2f58b22f55dd43749d1dfe
https://gist.github.com/mcdoll/83c11d5d4422eb6552330a7b56f82077

[Moritz]

while the first version has a way more satisfying definition, it is more tedious to interact with (you have to unpack more structure), but the later might give more boilerplate code.

[Heather Macbeth]

@Moritz Did you consider a variant on the second thing you listed,

def semibilin_map (R : Type*) (R₂ : Type*) (S : Type*) (S₂ : Type*)
  [semiring R] [semiring R₂] [semiring S] [semiring S₂]
  (M : Type*) (N : Type*) (P : Type*)
  [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P]
  [module R M] [module S N] [module R₂ P] [module S₂ P]
  [smul_comm_class S₂ R₂ P]
  (ρ₁₂ : R →+* R₂) (σ₁₂ : S →+* S₂)
  := M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P

[Moritz]

this has the issues that were mentioned by Eric: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bounded.20bilinear.20forms/near/261981962

[Moritz]

I made a mwe why this is not good: https://gist.github.com/mcdoll/dfdaffa35e5b66c442b910384b9086fe

[Heather Macbeth]

Come to think of it (sorry if you already answered this) -- is there a reason we need the definition semibilin_map? (I agree that a definition semibilin_form for M → M → R or M → M → N would be useful but I don't yet see what lemmas would need a special namespace for M → N → P).

[Heather Macbeth]

Maybe the idea is to develop something parallel to
https://leanprover-community.github.io/mathlib_docs/linear_algebra/multilinear/basic.html
?

[Moritz]

we could unify all the calculation things for sesquilinear and bilinear maps/forms. Now there is a lot of copy&paste stuff between sesquilinear_form and bilinear_form and we could remove most of it by defining structure bilin_map extends semibilin_map R R R R M N P (ring_hom.id R) (ring_hom.id R) and then invoking B.to_semilin_map.stuff

[Heather Macbeth]

Moritz said:

we could unify all the calculation things for sesquilinear and bilinear maps/forms.

This part I am completely in favour with

[Moritz]

It would be quite parallel with the multilinear library

[Moritz]

At least the second version I wrote above

[Heather Macbeth]

But when we define the semibilinear version, I don't think we need a special name for the bilinear and sesquilinear versions -- you can just take as your input to a lemma a semibilinear form/map in which the arguments are appropriate

[Heather Macbeth]

And I'm also asking whether semibilin_map needs to be named, or whether semibilin_form is the first thing that needs a name.

[Heather Macbeth]

(Basically, as you have discovered yourself in these tests, every time you give a new name to something, Lean finds more trouble in discovering that it is equal to its definition when you need that. So it's often better to minimize the number of things that get names ...)

[Moritz]

If we want that bounded_bilinear_map is an extension, then we have to use semibilin_map

[Moritz]

is there a possibility to do type-aliases in lean? so that we could write bilinear_form R M and it gets internally resolved to semibilin_map R R R R M M R (ring_hom.id R) (ring_hom.id R)

[Moritz]

I agree with the too many definitions/namespaces argument

[Heather Macbeth]

Moritz said:

If we want that bounded_bilinear_map is an extension, then we have to use semibilin_map

I think you can do

import analysis.normed_space.basic

variables {𝕜 : Type*} [normed_field 𝕜]
variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
variables {F : Type*} [normed_group F] [normed_space 𝕜 F]
variables {G : Type*} [normed_group G] [normed_space 𝕜 G]

structure bounded_bilinear_map extends E →ₗ[𝕜] F →ₗ[𝕜] G :=
(bounded : ∃ (C : ℝ) (H : C > 0), ∀ (x : E) (y : F), ∥to_fun x y∥ ≤ (C * ∥x∥) * ∥y∥)

[Heather Macbeth]

(not sure if this is the best way, just an argument that we don't need the definition semibilin_map)

[Heather Macbeth]

And another way is of course to just use E →L[𝕜] F →L[𝕜] G (see here)

[Heather Macbeth]

Moritz said:

is there a possibility to do type-aliases in lean? so that we could write bilinear_form R M and it gets internally resolved to semibilin_map R R R R M M R (ring_hom.id R) (ring_hom.id R)

Unfortunately not; you can define type-aliases but they don't unfold everywhere so to speak, so are not completely silent.

A very common workaround in mathlib is notation, which is completely silent. So for the case of linear/conjugate-linear/semilinear maps we have separate notations for the concepts, even though the first two are special cases of the last.

[Heather Macbeth]

notation M ` →ₛₗ[`:25 σ:25 `] `:0 M₂:0 := linear_map σ M M₂
notation M ` →ₗ[`:25 R:25 `] `:0 M₂:0 := linear_map (ring_hom.id R) M M₂
notation M ` →ₗ⋆[`:25 R:25 `] `:0 M₂:0 := linear_map (@star_ring_aut R _ _ : R →+* R) M M₂

[Heather Macbeth]

This provides for

f : M →ₛₗ[σ] M₂
f : M →ₗ[R] M₂
f : M →ₗ⋆[R] M₂

semilinear, linear, conjugate-linear in that order.

We might like to introduce some notation for bilinear and sesquilinear forms; then they could be silent special cases of semibilinear forms.

[Frédéric Dupuis]

If the only reason we want those types to exist is to enable dot notation, what's wrong with putting the lemmas we want in the linear_map and continuous_linear_map namespaces, as is done in bilinear_map.lean?

[Moritz]

Heather Macbeth said:

Moritz said:

If we want that bounded_bilinear_map is an extension, then we have to use semibilin_map

I think you can do

import analysis.normed_space.basic

variables {𝕜 : Type*} [normed_field 𝕜]
variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
variables {F : Type*} [normed_group F] [normed_space 𝕜 F]
variables {G : Type*} [normed_group G] [normed_space 𝕜 G]

structure bounded_bilinear_map extends E →ₗ[𝕜] F →ₗ[𝕜] G :=
(bounded : ∃ (C : ℝ) (H : C > 0), ∀ (x : E) (y : F), ∥to_fun x y∥ ≤ (C * ∥x∥) * ∥y∥)

I did not know that that could work.

[Heather Macbeth]

Neither did I, till I tried it just now! :)

[Yaël Dillies]

Sorry what! We can extend compound type? :open_mouth:

[Moritz]

Frédéric Dupuis said:

If the only reason we want those types to exist is to enable dot notation, what's wrong with putting the lemmas we want in the linear_map and continuous_linear_map namespaces, as is done in bilinear_map.lean?

If the thing Heather posted works, I don't see any problems with that.

[Heather Macbeth]

Do try the E →L[𝕜] F →L[𝕜] G way, too!

[Frédéric Dupuis]

Yeah, I don't see why we want a structure for this -- what advantages would it have over just using E →L[𝕜] F →L[𝕜] G?

[Frédéric Dupuis]

We can just use linear_map.mk_continuous₂ to have a constructor similar to that structure, without having to start duplicating the API.