Instances for is_R_or_C

Stream: maths

[Heather Macbeth]

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]

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]

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

[Frédéric Dupuis]

Ah, right!

[Frédéric Dupuis]

Do you know where those two instances are defined?

[Heather Macbeth]

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

[Heather Macbeth]

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]

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]

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

[Frédéric Dupuis]

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

[Heather Macbeth]

(the latter is docs#finite_dimensional.complex_to_real apparently)

[Frédéric Dupuis]

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]

Great, thank you!

[Heather Macbeth]

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]

Hmm... good question!

[Heather Macbeth]

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]

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

[Frédéric Dupuis]

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

[Heather Macbeth]

#5466