Zulip Chat Archive

Stream: maths

Topic: Instances for is_R_or_C


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Frédéric Dupuis (Dec 20 2020 at 23:39):

Ah, right!

view this post on Zulip Frédéric Dupuis (Dec 20 2020 at 23:39):

Do you know where those two instances are defined?

view this post on Zulip Heather Macbeth (Dec 20 2020 at 23:39):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Dec 20 2020 at 23:41):

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

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Dec 20 2020 at 23:43):

(the latter is docs#finite_dimensional.complex_to_real apparently)

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Dec 20 2020 at 23:44):

Great, thank you!

view this post on Zulip 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.

view this post on Zulip Frédéric Dupuis (Dec 21 2020 at 00:16):

Hmm... good question!

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Dec 21 2020 at 05:35):

#5466


Last updated: May 09 2021 at 10:11 UTC