Boundaryless models

Stream: mathlib4

[Yury G. Kudryashov]

What do you think about replacing docs#ModelWithCorners.Boundaryless with this?

class ModelWithCorners.IsTrivial (I : ModelWithCorners 𝕜 E E) where
  eq_self : I = modelWithCornersSelf 𝕜 E

[Yury G. Kudryashov]

Or adding this as a new typeclass.

[Yury G. Kudryashov]

#5499

[Sebastien Gouezel]

The point of the boundaryless typeclass is that it is stable under products. Do you have a use case where it doesn't work for you?

[Yury G. Kudryashov]

IsTrivial is also stable under products.

[Yury G. Kudryashov]

The use case is to move between MDifferentiable I I' (f : E → F) and Differentiable 𝕜 f.

[Sebastien Gouezel]

Ah, yes, it is a propositional equality that you require, not a definitional one.

[Yury G. Kudryashov]

We have, e.g., docs#Smooth.prod_mk and docs#Smooth.prod_mk_space.

[Yury G. Kudryashov]

I suggest that we add this new typeclass and define lemmas like Smooth.cod_to_space Smooth.cod_of_space instead.

[Sebastien Gouezel]

I'm not sure I understand how the new design would turn the two two lemmas like docs#Smooth.prod_mk and docs#Smooth.prod_mk_space into just one. I'll understand better when you PR it! I would be interested in @Floris van Doorn thoughts, because he had to use a lot the library in concrete situations for sphere eversion.

[Yury G. Kudryashov]

We can leave docs#Smooth.prod_mk only. If you have h : Smooth I I' f with [I'.IsTrivial], then h.cod_to_space will give you Smooth I 𝓘(𝕜, F) f.

[Yury G. Kudryashov]

I have to wait with a PR till mathlib4 is open for refactors.

[Sebastien Gouezel]

ok, I get it. Looks good to me!

[Yury G. Kudryashov]

I found a very important flaw: the main issue is not about I being equal to the trivial model; the main issue is about ChartedSpace instances being equal.