# Zulip Chat Archive

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

#### Yury G. Kudryashov (May 21 2020 at 02:16):

#### 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):

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

#### 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):

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)

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