## Stream: maths

### Topic: Instances for is_R_or_C

#### Heather Macbeth (Dec 20 2020 at 22:38):

I learned the other day that typeclass inference finds the complete_space and proper_space instances for finite-dimensional normed spaces over both ℝ and ℂ by typeclass inference.

Sebastien Gouezel said:

Over the reals, it's already registered as an instance.

example {E : Type*} [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :
complete_space E := by apply_instance


(through docs#finite_dimensional.proper_real). It also applies over the complexes as all the instances to see a complex vector space as a real vector space are already there:

example {E : Type*} [normed_group E] [normed_space ℂ E] [finite_dimensional ℂ E] :
complete_space E := by apply_instance


question 1: It should be safe to register

variables {𝕜 : Type*} [is_R_or_C 𝕜]

instance {E : Type*} [normed_group E] [normed_space 𝕜 E] [finite_dimensional 𝕜 E] : complete_space E := ...


right? Since complete_space is Prop-valued, so there is no concern about duplicate instances. Same for proper_space.

question 2: Assuming it's safe, how do I do fill in the proof, since the proofs for ℝ and ℂ are a little different? Does is_R_or_C allow me to split into cases? @Frédéric Dupuis

#### Frédéric Dupuis (Dec 20 2020 at 23:38):

Yes, we definitely want the instance for is_R_or_C, otherwise we can't use it to prove results for both ℝ and ℂ that require complete_space. The challenge is going to be to make sure that this instance is defeq with the existing ones in both cases.

#### Heather Macbeth (Dec 20 2020 at 23:38):

But in this case it shouldn't matter about being defeq, right? Because complete_space is Prop-valued, no data.

Ah, right!

#### Frédéric Dupuis (Dec 20 2020 at 23:39):

Do you know where those two instances are defined?

#### Heather Macbeth (Dec 20 2020 at 23:39):

So how do I prove this? :). Can I break into cases somehow?

#### Heather Macbeth (Dec 20 2020 at 23:40):

Frédéric Dupuis said:

Do you know where those two instances are defined?

Taking proper first (since complete is deduced from that), it's just docs#finite_dimensional.proper_real.

#### Frédéric Dupuis (Dec 20 2020 at 23:40):

There's one of the axioms of is_R_or_C that can effectively be used to break into cases, but it won't be type equality.

#### Heather Macbeth (Dec 20 2020 at 23:41):

Using, for C, that a finite-dimensional space over C is also finite-dimensional over R.

#### Frédéric Dupuis (Dec 20 2020 at 23:42):

Ah, then we should be able to do this as well without needing to break in into cases.

#### Heather Macbeth (Dec 20 2020 at 23:43):

(the latter is docs#finite_dimensional.complex_to_real apparently)

#### Frédéric Dupuis (Dec 20 2020 at 23:44):

For instance this sort of trick is used here: https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/inner_product.html#exists_norm_eq_infi_of_complete_subspace

#### Heather Macbeth (Dec 20 2020 at 23:44):

Great, thank you!

#### Heather Macbeth (Dec 21 2020 at 00:06):

OK, I can do this:

import analysis.normed_space.finite_dimension
import data.complex.is_R_or_C

variables {𝕜 : Type*} [is_R_or_C 𝕜]
variables {E : Type*} [normed_group E] [normed_space 𝕜 E]

instance finite_dimensional.is_R_or_C_to_real : finite_dimensional ℝ 𝕜 := sorry

instance finite_dimensional.proper_is_R_or_C [finite_dimensional 𝕜 E] : proper_space E :=
begin
letI : normed_space ℝ E := restrict_scalars.normed_space ℝ 𝕜 E,
letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
letI : finite_dimensional ℝ E := finite_dimensional.trans ℝ 𝕜 E,
apply_instance
end


but how do I fill in the sorry? We don't seem to have that is_R_or_C is finite-dimensional over ℝ, and presumably this instance, though safe to add to the library, will have a proof involving breaking into cases.

#### Frédéric Dupuis (Dec 21 2020 at 00:16):

Hmm... good question!

#### Heather Macbeth (Dec 21 2020 at 00:40):

I could probably prove it directly from docs#is_R_or_C.re_add_im_ax, would that be a hack?

#### Frédéric Dupuis (Dec 21 2020 at 00:52):

I wouldn't say it's a hack, I think that's how it should be done!

#### Frédéric Dupuis (Dec 21 2020 at 00:53):

I think this together with finite_dimensional.iff_fg (and probably a lot of fiddling around...) will do the trick.

#### Heather Macbeth (Dec 21 2020 at 05:35):

#5466

Last updated: May 09 2021 at 10:11 UTC