# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: R^m is finite dimensional over R

#### Bhavik Mehta (Mar 24 2021 at 01:59):

```
import data.real.basic
import linear_algebra.finite_dimensional
example {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
begin
apply_instance
end
```

I presume I'm just missing imports, but which ones?

#### Yakov Pechersky (Mar 24 2021 at 02:06):

#### Bhavik Mehta (Mar 24 2021 at 02:06):

```
import data.real.basic
import linear_algebra.finite_dimensional
import ring_theory.noetherian
example {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
begin
apply_instance
end
```

Doesn't work

#### Adam Topaz (Mar 24 2021 at 02:16):

Is finite dimensional map even a class?

#### Bhavik Mehta (Mar 24 2021 at 02:18):

Most of the lemmas about it in linear_algebra.finite_dimensional take `finite_dimensional K V`

as a typeclass argument, so I assume that's how it's meant to be used

#### Adam Topaz (Mar 24 2021 at 02:19):

Right. I got confused because the API docs just lists it as a def

#### Bhavik Mehta (Mar 24 2021 at 02:20):

```
import data.real.basic
import linear_algebra.finite_dimensional
example {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
@is_noetherian_pi _ _ _ _ _ _ _ (λ i, infer_instance)
```

This works but it's weird that there's no nicer way - why is it that I need to look at the implemention of finite_dimensional and look through noetherian lemmas to get a linear algebra result

#### Adam Topaz (Mar 24 2021 at 02:22):

Does it work if you replace fin n with a type with a Fintype instance?

#### Adam Topaz (Mar 24 2021 at 02:23):

I mean, it shouldn't. But might be worth checking anyway

#### Bhavik Mehta (Mar 24 2021 at 02:24):

Yup it doesn't work

#### Adam Topaz (Mar 24 2021 at 02:28):

Sounds like a missing instance :expressionless:

#### Bhavik Mehta (Mar 24 2021 at 02:35):

```
import data.real.basic
import linear_algebra.finite_dimensional
example {K : Type*} [field K] {i : ℕ} : finite_dimensional K (fin i → K) :=
begin
apply_instance
end
```

But this works...

#### Adam Topaz (Mar 24 2021 at 02:36):

Oooh... The mystery deepens

#### Shing Tak Lam (Mar 24 2021 at 05:22):

Seems like `local attribute [-instance] real.semiring real.ring`

"fixes" it and `apply_instance`

works

```
import data.real.basic
import linear_algebra.finite_dimensional
local attribute [-instance] real.semiring real.ring
example {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) := by apply_instance
```

#### Shing Tak Lam (Mar 24 2021 at 05:30):

Here's the original failure and the case for `field K`

minimised

```
import data.real.basic
import linear_algebra.finite_dimensional
-- These both find `finite_dimensional.finite_dimensional_self`
example {K : Type*} [field K] (m : ℕ) : ∀ (i : fin m), is_noetherian K K :=
by show_term {apply_instance}
example (m : ℕ) : ∀ (i : fin m), finite_dimensional ℝ ℝ :=
by show_term {apply_instance}
-- But this fails
example (m : ℕ) : ∀ (i : fin m), is_noetherian ℝ ℝ := by apply_instance
```

If I turn on `set_option pp.all`

, the goal for `finite_dimensional ℝ ℝ`

is like so

```
@finite_dimensional.{0 0} real real real.field real.add_comm_group
(@semiring.to_semimodule.{0} real
(@ring.to_semiring.{0} real (@division_ring.to_ring.{0} real (@field.to_division_ring.{0} real real.field))))
```

and for `is_noetherian ℝ ℝ`

it's

```
@is_noetherian.{0 0} real real real.semiring real.add_comm_monoid (@semiring.to_semimodule.{0} real real.semiring)
```

and as the instance it found for `finite_dimensional ℝ ℝ`

uses a `finite_dimensional`

lemma, and not a `is_noetherian`

lemma, I guessed that maybe the short circuit instances are causing issues, so I added `local attribute [-instance] real.semiring real.ring`

and then the instance search worked.

#### Alex J. Best (Mar 24 2021 at 05:34):

Just getting rid of `real.ring`

is enough even

#### Mario Carneiro (Mar 24 2021 at 05:35):

hm, this works:

```
example (m : ℕ) (i : fin m) : is_noetherian ℝ ℝ := by apply_instance
```

#### Mario Carneiro (Mar 24 2021 at 05:38):

The only difference:

```
[class_instances] (0) ?x_0 i :
@is_noetherian ℝ ℝ real.semiring real.add_comm_monoid (@semiring.to_semimodule ℝ real.semiring) :=
@finite_dimensional.finite_dimensional_self (?x_42 i) (?x_43 i)
failed is_def_eq
```

vs

```
[class_instances] (0) ?x_0 :
@is_noetherian ℝ ℝ real.semiring real.add_comm_monoid (@semiring.to_semimodule ℝ real.semiring) :=
@finite_dimensional.finite_dimensional_self ?x_42 ?x_43
(works)
```

#### Bhavik Mehta (Mar 25 2021 at 00:03):

So what's the fix in mathlib? Or should I be saying `local attribute [-instance] real.ring`

#### Bhavik Mehta (Mar 25 2021 at 04:25):

Alright, now I've additionally used the import analysis.convex.topology and the local attribute fixes no longer work:

```
import data.real.basic
import linear_algebra.finite_dimensional
import analysis.convex.topology
local attribute [-instance] real.semiring real.ring
example {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
begin
apply_instance
end
```

What am I meant to do with this now?

#### Yakov Pechersky (Mar 25 2021 at 04:27):

```
local attribute [-instance] real.nondiscrete_normed_field real.normed_field real.semiring real.ring
```

#### Yakov Pechersky (Mar 25 2021 at 04:28):

I think there's probably an issue somewhere with `is_R_or_C`

#### Yakov Pechersky (Mar 25 2021 at 04:30):

Ah. It might have to do with `real.linear_ordered_field`

#### Bhavik Mehta (Mar 25 2021 at 04:33):

It's so bizarre to me that mathlib is set up so that I can't show R^m is finite dimensional out of the box!

#### Yakov Pechersky (Mar 25 2021 at 04:35):

I don't know enough about diamond discovery to figure out what's wrong here, will have to wait for the real sleuths

#### Bryan Gin-ge Chen (Mar 25 2021 at 04:51):

Whatever is going on, I doubt the troubles you're having here are intentional. Something needs to be fixed; maybe some instances need to be put in locales?

#### Mario Carneiro (Mar 25 2021 at 04:54):

yeah, those `local attribute [-instance]`

lines are definitely not a proper solution. It looks like a lean bug

#### Mario Carneiro (Mar 25 2021 at 04:57):

For a mathlib workaround, you can just declare `instance {m : ℕ} : finite_dimensional ℝ (fin m → ℝ)`

#### Patrick Massot (Apr 23 2021 at 14:00):

It seems this issue is still not solved in mathlib master. I think this is a very serious issue. @Mario Carneiro are you suggesting we put

```
import data.real.basic
import linear_algebra.finite_dimensional
instance {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
@is_noetherian_pi ℝ _ _ _ _ _ _ (λ i, finite_dimensional.finite_dimensional_self _)
```

somewhere? It feels like the underlying issue will get more opportunities to strike elsewhere if we ignore it.

#### Mario Carneiro (Apr 23 2021 at 14:03):

I don't think it's a great solution but it should help for the time being

#### Mario Carneiro (Apr 23 2021 at 14:04):

I don't know what's wrong in lean and I'm not especially motivated to try to patch typeclass inference

#### Johan Commelin (Apr 23 2021 at 14:05):

If we add the instance, we should probably replace `fin m`

by an arbitrary fintype.

#### Eric Wieser (Apr 23 2021 at 14:13):

This works:

```
/-- non-dependent version of `is_noetherian_pi` -/
instance is_noetherian_pi' {R ι : Type*} {M : Type*} [ring R]
[add_comm_group M] [semimodule R M] [fintype ι]
[is_noetherian R M] : is_noetherian R (ι → M) :=
is_noetherian_pi
```

#### Eric Wieser (Apr 23 2021 at 14:13):

Then `apply_instance`

can close the original goal

#### Johan Commelin (Apr 23 2021 at 14:14):

Did you check that it closes the original goal?

#### Johan Commelin (Apr 23 2021 at 14:14):

Because this thread seems to show that it doesn't always work as expected...

#### Eric Wieser (Apr 23 2021 at 14:14):

~~Huh, I guess I screwed up~~

#### Eric Wieser (Apr 23 2021 at 14:15):

Yes, it does:

```
import data.real.basic
import linear_algebra.finite_dimensional
/-- non-dependent version of `is_noetherian_pi` -/
instance is_noetherian_pi' {R ι : Type*} {M : Type*} [ring R]
[add_comm_group M] [semimodule R M] [fintype ι]
[is_noetherian R M] : is_noetherian R (ι → M) :=
is_noetherian_pi
instance {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
by apply_instance -- works fine
```

#### Eric Wieser (Apr 23 2021 at 14:16):

I've seen something very similar for all the `dfinsupp`

instances, where it can't seem to work out how to provide `M : ι → Type*`

when it's a constant function

#### Patrick Massot (Apr 23 2021 at 14:19):

This doesn't seem to be enough

#### Eric Wieser (Apr 23 2021 at 14:19):

As in, that example fails for you, or there's a wider use case that still fails?

#### Patrick Massot (Apr 23 2021 at 14:23):

I have a hard time minimizing...

#### Patrick Massot (Apr 23 2021 at 17:05):

I returned to this but gave up on true minimization. It seems to be a really subtle elaboration order issue. The next piece of code works only if you uncomment the specialized instance:

```
import analysis.calculus.times_cont_diff
/-- non-dependent version of `is_noetherian_pi`, because typeclass inference struggles to infer `M` in the non-dependent case. -/
instance is_noetherian_pi' {R ι : Type*} {M : Type*} [ring R]
[add_comm_group M] [semimodule R M] [fintype ι]
[is_noetherian R M] : is_noetherian R (ι → M) :=
is_noetherian_pi
--instance {m : ℕ} : finite_dimensional ℝ (fin m → ℝ) :=
--by apply_instance -- works fine
open_locale topological_space
variables {E : Type*} [normed_group E] [normed_space ℝ E]
{F : Type*} [normed_group F] [normed_space ℝ F] [finite_dimensional ℝ F]
def smooth_at (f : E → F) (x : E) : Prop := ∃ s ∈ 𝓝 x, times_cont_diff_on ℝ ⊤ f s
lemma smooth_surrounding {x : F} {d} {p : fin d → F} :
∃ W : F × (fin d → F) → (fin d → ℝ),
∀ᶠ y in 𝓝 x, ∀ᶠ q in 𝓝 p, smooth_at W (y, q) :=
sorry
```

#### Eric Wieser (Apr 23 2021 at 17:24):

The failing lemma can be reduced to

```
lemma smooth_fails {d} (W : F → (fin d → ℝ)) (y : F) : smooth_at W y :=
sorry
```

#### Eric Wieser (Apr 23 2021 at 17:31):

Some more investigation:

```
import analysis.calculus.times_cont_diff
/-- non-dependent version of `is_noetherian_pi`, because typeclass inference struggles to infer `M` in the non-dependent case. -/
instance is_noetherian_pi' {R ι : Type*} {M : Type*} [ring R]
[add_comm_group M] [semimodule R M] [fintype ι]
[is_noetherian R M] : is_noetherian R (ι → M) :=
is_noetherian_pi
-- if this is an instance the original works
def missing (ι : Type*) [fintype ι] : is_noetherian ℝ (ι → ℝ) :=
by apply_instance -- works fine
open_locale topological_space
variables {E : Type*} [normed_group E] [normed_space ℝ E]
{F : Type*} [normed_group F] [normed_space ℝ F] [is_noetherian ℝ F]
def smooth_at (f : E → F) (x : E) : Prop := ∃ s ∈ 𝓝 x, times_cont_diff_on ℝ ⊤ f s
set_option pp.implicit true
lemma smooth_fails {d} (W : F → (fin d → ℝ)) (y : F) :
@smooth_at _ _ _ _ _ _ (missing _) W y :=
sorry
lemma smooth_ok1 {d} (W : F → (fin d → ℝ)) (y : F) :
@smooth_at _ _ _ _ _ _ (missing $ fin d) W y :=
sorry
lemma smooth_ok2 {d} (W : F → (fin d → ℝ)) (y : F) :
@smooth_at _ _ _ _ _ _ (by exact missing _) W y :=
sorry
```

Last updated: May 07 2021 at 23:11 UTC