## Stream: PR reviews

### Topic: 2749 Implicit function theorem

#### 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.

#2749

#### Heather Macbeth (May 21 2020 at 03:29):

This is really exciting!

#### Heather Macbeth (May 21 2020 at 03:29):

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

#### 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?

#### Yury G. Kudryashov (May 21 2020 at 03:34):

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

#### 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.

#### Yury G. Kudryashov (May 21 2020 at 03:35):

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

#### Heather Macbeth (May 21 2020 at 03:44):

(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

#### Heather Macbeth (May 21 2020 at 03:45):

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

#### 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.

#### Yury G. Kudryashov (May 21 2020 at 03:47):

AFAIR, we don't have is_linear_equiv predicate.

#### Heather Macbeth (May 21 2020 at 03:48):

Yes, just seeing that.

#### Heather Macbeth (May 21 2020 at 03:48):

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

#### Yury G. Kudryashov (May 21 2020 at 03:48):

I can write f'.comp inr, yes.

#### 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.

#### Heather Macbeth (May 21 2020 at 03:55):

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

#### 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\times F\to G$, right?

#### Heather Macbeth (May 21 2020 at 04:08):

(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)

#### 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?

#### 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.

#### 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\times F\to G$, right?

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

#### Heather Macbeth (May 21 2020 at 05:06):

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

#### Heather Macbeth (May 21 2020 at 05:18):

It seems a bit strange to think of the function $f(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 $\mathbb{R}^2\to C^\infty(\mathbb{R})$, defined by $(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 ....

#### Yury G. Kudryashov (May 21 2020 at 05:28):

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

#### Yury G. Kudryashov (May 21 2020 at 05:29):

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

#### Yury G. Kudryashov (May 21 2020 at 05:30):

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

#### Yury G. Kudryashov (May 21 2020 at 05:31):

Or just drop it for now.

#### Yury G. Kudryashov (May 21 2020 at 05:31):

And see what we'll really need.

#### Yury G. Kudryashov (May 21 2020 at 07:54):

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

#### Patrick Massot (May 21 2020 at 11:36):

Do we already have a version where we consider $f : E \to F$ and a isomorphism $\varphi : K \times H \simeq E$, unrelated to $f$, such that, under the appropriate assumptions, there is $g : K \to H$ such that, for $(k, h)$ in a neighborhood of $(k_0, h_0)$, $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 "$y$ not being the last coordinate".

#### 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 $\mathbb S^n$ and $O_n(\mathbb R)$ are submanifolds.

Last updated: May 07 2021 at 17:36 UTC