Zulip Chat Archive

Stream: PR reviews

Topic: 2749 Implicit function theorem


view this post on Zulip Yury G. Kudryashov (May 21 2020 at 02:16):

Two out of three versions are ready for review. I'm not sure yet how should I formulate the prod case. E.g., should I use f : E × F → G or f : E → F → G? How should I say that f is differentiable in both variables and the derivative in the second variable is invertible? I don't like the way it is done now but can't come up with a better API.

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 02:16):

#2749

view this post on Zulip Heather Macbeth (May 21 2020 at 03:29):

This is really exciting!

view this post on Zulip Heather Macbeth (May 21 2020 at 03:29):

The third (prod) version is what some people call the Rank Theorem, right?

view this post on Zulip Heather Macbeth (May 21 2020 at 03:31):

You have probably considered this, but could you phrase the invertibility of the derivative in the second variable by introducing a version of linearity of the right injection in the category of bounded linear maps?

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 03:34):

What exactly do you suggest? Could you please just list arguments?

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 03:35):

I learned all this in Russian and I don't know how people call this in English.

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 03:35):

(except for what I read in Wikipedia and some textbooks)

view this post on Zulip Heather Macbeth (May 21 2020 at 03:44):

Instead of

(f'inv : G L[𝕜] F)  (hf'l :  y : F, f'inv (f' (0, y)) = y) (hf'r :  z : G, f' (0, f'inv z) = z)

could you do

(hf' : is_linear_equiv (f' inr))

where inr is like linearity of the right injection in the category of bounded linear maps

view this post on Zulip Heather Macbeth (May 21 2020 at 03:45):

(the open mapping theorem would give that the inverse is also bounded linear, right?)

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 03:47):

I see the following ways to formulate the prod version:

  • (now in implicit.lean): f : E × F → G has derivative f', f'inv : G →L[k] F is an inverse for λ y, f (0, y);
  • same with linear_map.comp instead of extensional equalities;
  • (f : E → F → G) (f' : (E × F) →L[k] G) (f'y : F ≃L[k] G) (hf' : has_strict_fderiv_at (uncurry f) f'(x, y)) (hf'y : has_strict_fderiv (f x) f'y y);
  • (f : E → F → G) (f' : (E × F) →L[k] G) (f'y : F ≃L[k] G) (hf' : has_strict_fderiv_at (uncurry f) f'(x, y)) (hf'y : f'.comp inr = f'y.

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 03:47):

AFAIR, we don't have is_linear_equiv predicate.

view this post on Zulip Heather Macbeth (May 21 2020 at 03:48):

Yes, just seeing that.

view this post on Zulip Heather Macbeth (May 21 2020 at 03:48):

But can you write f' inr instead of λ y, f' (0, y) ?

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 03:48):

I can write f'.comp inr, yes.

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 03:51):

But I'm not sure whether I should ask for f'inv or f'y : F ≃L[k] G.

view this post on Zulip Heather Macbeth (May 21 2020 at 03:55):

I have seen that people who are more experienced with Lean often prefer the style EFGE \to F \to G, but for me, the style E×FGE\times F\to G seems better-adapted to this context.

view this post on Zulip Heather Macbeth (May 21 2020 at 03:56):

i.e., one is more likely to want to apply inverse function theorem on a map E×FGE\times F\to G, right?

view this post on Zulip Heather Macbeth (May 21 2020 at 04:08):

I don't know about
(f'y : F ≃L[k] G) (hf'y : f'.comp inr = f'y) vs
(f'inv : G →L[k] F) (hf'l : (f'.comp inr).comp f'inv = id) (hf'r : f'inv.comp (f'.comp inr) = id)
(or whatever the notation for the identity is)

view this post on Zulip Heather Macbeth (May 21 2020 at 04:08):

It seems like the former is more attractive, but would in the end be established by proving the latter?

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 04:47):

My main concern about f'y style is that we ask for the same data (forward map of f'y) twice.

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 04:50):

i.e., one is more likely to want to apply inverse function theorem on a map E×FGE\times F\to G, right?

Not if one defines all functions with two arguments as E → F → G.

view this post on Zulip Heather Macbeth (May 21 2020 at 05:06):

But often the domain will be an open subset of E×FE \times F which is not an exact product of an open subset of EE and an open subset of FF?

view this post on Zulip Heather Macbeth (May 21 2020 at 05:18):

It seems a bit strange to think of the function f(x,y,z)=(x2+y22)2+z21f(x,y,z)=(\sqrt{x^2+y^2}-2)^2+z^2-1, which I would apply IFT to to produce a torus, as a map R2C(R)\mathbb{R}^2\to C^\infty(\mathbb{R}), defined by (x,z)(x2+22)2+z21(x,z)\mapsto (\sqrt{x^2+\cdot^2}-2)^2+z^2-1. Maybe I am just not used to the Lean way of thinking yet ....

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 05:28):

Unfortunately, this is not a E×FE \times F case.

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 05:29):

Because yy is the middle variable and because most theorems about Rn\mathbb R^n use fin n → R.

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 05:30):

This means that I probably should completely rewrite the prod case.

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 05:31):

Or just drop it for now.

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 05:31):

And see what we'll really need.

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 07:54):

Added of_proj version which generalizes all others, removed prod_ for now.

view this post on Zulip Patrick Massot (May 21 2020 at 11:36):

Do we already have a version where we consider f:EFf : E \to F and a isomorphism φ:K×HE\varphi : K \times H \simeq E, unrelated to ff, such that, under the appropriate assumptions, there is g:KHg : K \to H such that, for (k,h)(k, h) in a neighborhood of (k0,h0)(k_0, h_0), f(φ(k,h))=f(φ(k0,h0))    h=g(k)f\big(\varphi(k, h)\big) = f\big(\varphi(k_0, h_0)\big) \iff h = g(k)? This appears to solve Heather's issue of "yy not being the last coordinate".

view this post on Zulip Patrick Massot (May 21 2020 at 11:36):

Anyway, I guess we could merge this (after adding some more docstrings) and wait for the real test: define submanifolds and prove Sn\mathbb S^n and On(R)O_n(\mathbb R) are submanifolds.


Last updated: May 07 2021 at 17:36 UTC