API around `Space (d1 + d2)` to `Space d1 x Space d2`

Stream: PhysLean

[Joseph Tooby-Smith]

I want to build an API primarily around: Space (d1 + d2) ≃L[ℝ] Space d1 × Space d2. There are a number of things I am a bit uncertain about in terms of how to build such an API, and would be very glad to hear opinions.

1. What should the map Space (d1 + d2) ≃L[ℝ] Space d1 × Space d2 be called? I would usually tend to something like split, but I don't think this is the best, and maybe there is a better 'physics' term.
2. On top of defining Space (d1 + d2) ≃L[ℝ] Space d1 × Space d2 is it best to separately define the individual projects Space (d1 + d2) → L[ℝ] Space d1 etc. and inclusions Space d1 → L[ℝ] Space (d1 + d2), or just the equivalence above.

My plan with the API is to do things around e.g. differentiation and integration.

[Kevin Buzzard]

Are d1 and d2 likely to be concrete natural numerals (e.g. 3) in practice, or variable naturals (e.g. n)? I ask because 1+3 is definitionally equal to 3+1 (if they're both naturals), but a+b is not definitionally equal to b+a so if you envisage applications where variables are involved you might instead want this to be (h : d3 = d1 + d2) : Space (d3) ≃L[ℝ] Space d1 × Space d2 or else you might end up in dependent type hell.

[Alfredo Moreira-Rosa]

1. Something around the word decoupled looks more physics related than split. Not sure if it's correct in this context though

[Joseph Tooby-Smith]

Kevin Buzzard said:

Are d1 and d2 likely to be concrete natural numerals (e.g. 3) in practice, or variable naturals (e.g. n)? I ask because 1+3 is definitionally equal to 3+1 (if they're both naturals), but a+b is not definitionally equal to b+a so if you envisage applications where variables are involved you might instead want this to be (h : d3 = d1 + d2) : Space (d3) ≃L[ℝ] Space d1 × Space d2 or else you might end up in dependent type hell.

I think there will be mixture of other cases here, so maybe it is best to have something like (h : d3 = d1 + d2 := rfl).

[Joseph Tooby-Smith]

Alfredo Moreira-Rosa said:

1. Something around the word decoupled looks more physics related than split. Not sure if it's correct in this context though

Yeah, I don't think decoupled is quite the right context here. The only other word I can come up with is slice, by similarity with time slice.

[Eric Wieser]

Kevin Buzzard said:

Are d1 and d2 likely to be concrete natural numerals (e.g. 3) in practice, or variable naturals (e.g. n)? I ask because 1+3 is definitionally equal to 3+1 (if they're both naturals), but a+b is not definitionally equal to b+a so if you envisage applications where variables are involved you might instead want this to be (h : d3 = d1 + d2) : Space (d3) ≃L[ℝ] Space d1 × Space d2 or else you might end up in dependent type hell.

I'd normally recommend against this, and instead introduce a cast (h : d1 = d2) : Space d1 ≃L[ℝ] Space d2

[Eric Wieser]

Otherwise it ends up very annoying to write API lemmas

[Joseph Tooby-Smith]

Hmm, there is a lot of stuff in PhysLean so far using Space d and we have never needed to cast as of yet.
I'm wondering if I'm aiming for something too general here, and maybe all we actually need is Space d.succ ≃L[ℝ] Space 1 × Space d. This would be a sacrifice of generality for ease of use.

[Kevin Buzzard]

Given that d.succ := d + 1 I would be tempted to write it as Space d × Space 1 but I'm not sure it matters that much :-) I would trust Eric's opinions over mine when it comes to dependent type hell.

[Alex Meiburg]

Consider that you might want this to be a LinearIsometryEquiv instead of a ContinuousLinearEquiv, which is stronger. (This will require making sure you're getting the correct metric inferred on Space d1 × Space d2, first.)

[Joseph Tooby-Smith]

@Alex Meiburg Yeah, I somehow think the default metric is not going to be correct, since I believe the norm on products of types is defined by taking the maximum of the norms of both factors (for example).

But nevertheless there are certainly places in where ContinuousLinearEquiv has been used, where in fact LinearIsometryEquiv could have been used.

[Alex Meiburg]

Yeah, that's the default metric on a Prod, but you could explore adding a higher priority instance (maybe especially just for Space x Space)

[Kevin Buzzard]

This idea is very brittle. The moment you use a lemma which applies for general normed spaces you pick up the wrong typeclass, you can't fix this with priority hacks.

[Moritz Doll]

Are you aware of WithLp? in particular, you probably want to use docs#PiLp.sumPiLpEquivProdLpPiLp

[Joseph Tooby-Smith]

Thanks @Moritz Doll ! I'll look into using this.

[Joseph Tooby-Smith]

Moritz Doll said:

Are you aware of WithLp? in particular, you probably want to use docs#PiLp.sumPiLpEquivProdLpPiLp

Relatedly, I just start to attempt to bump PhysLean to v4.25.0, and noticed that the definition of WithLp has changed to a structure.