euclidean_space error

Stream: new members

[Hans Parshall]

I am trying to define a linear isometry from a submodule of euclidean_space, but I run into an error. How should I read/debug?

import analysis.inner_product_space.basic
import analysis.inner_product_space.pi_L2
import linear_algebra.basis

variables {𝕜 : Type*}
[is_R_or_C 𝕜]

variables {n : ℕ} (S : submodule 𝕜 (euclidean_space 𝕜 (fin n)))

variable (L : S →ₗᵢ[𝕜] (euclidean_space 𝕜 (fin n))) -- errors
/--
failed to synthesize type class instance for
𝕜 : Type u_1,
_inst_1 : is_R_or_C 𝕜,
n : ℕ,
S : submodule 𝕜 (euclidean_space 𝕜 (fin n))
⊢ module 𝕜 (euclidean_space 𝕜 (fin n))
--/

[Hans Parshall]

I can explicitly include the line:

[module 𝕜 (euclidean_space 𝕜 (fin n))]

before I define the variable S, which resolves the error. Is this the right fix? I thought euclidean_space was already understood to be a module, and so I worry that this is messing with how it will be processed later on.

[Reid Barton]

I agree that the "fix" you suggest isn't a good idea.

[Reid Barton]

The error is very confusing, do you really get this error with ℂ with the code you posted? In the online web editor I get an error about needing module 𝕜 (euclidean_space 𝕜 (fin n)), which makes somewhat more sense.

[Reid Barton]

I think the instance might really not exist.

[Hans Parshall]

Sorry, I agree the previous error was confusing and from a different typo. I've updated the above.

[Reid Barton]

Because it will try to use pi_Lp.normed_space, but this needs a fact (1 ≤ 2) that isn't there.

[Hans Parshall]

Am I correct that the bad idea "fix" I mentioned above replaces the correct module structure with an arbitrary one?

[Reid Barton]

It works if you add local attribute [instance] fact_one_le_two_real somewhere. It should be fixed in mathlib, though.

[Reid Barton]

Yes that's right

[Reid Barton]

Well, it doesn't exactly replace anything in the sense that the correct module structure isn't there.

[Reid Barton]

It says something like "Suppose we have an arbitrary module structure on euclidean_space 𝕜 (fin n)."

[Hans Parshall]

I can confirm that including the local attribute line resolves my error. How do I help get this fixed this in mathlib?

[Hans Parshall]

I'm also curious about your process for finding the fix of fact_one_le_two_real

[Eric Rodriguez]

we're "not allowed" a global fact instance, I wonder if this marks an exception

[Reid Barton]

Maybe best to post an issue, there could be other instances that are missing for the same reason.
We can also ping the people listed in the authors line: @Joseph Myers @Heather Macbeth @Sebastien Gouezel

[Reid Barton]

Basically I simulated instance search by reading the source: hmm there are no results for module, but there is an instance for finite_dimensional which depends on module so it must nevertheless exist somehow, notice euclidean_space is reducible so look for instances for its definition pi_Lp, see that this one has an instance for normed_group which extends module, but it involves a fact hypothesis so it won't work globally

[Hans Parshall]

That makes sense, thanks!

[Heather Macbeth]

Reid Barton said:

Maybe best to post an issue, there could be other instances that are missing for the same reason.
We can also ping the people listed in the authors line: Joseph Myers Heather Macbeth Sebastien Gouezel

In practice, for this and similar things (this file, this file, this file, this file, this file) we just put the

local attribute [instance] fact_one_le_two_real

at the top of every file. Is this not recommended practice?

[Reid Barton]

hmm, I guess euclidean_space is reducible, but it feels like breaking encapsulation to me

[Reid Barton]

Why should the user of euclidean_space need to care about the fact that the implementation of the module instance relies on fact_one_le_two_real

[Heather Macbeth]

I see your point. I've sometimes wondered why we have the instance docs#measure_theory.Lp.normed_space_L2 (and similar) recorded given that in the presence of local attribute [instance] fact_one_le_two_ennreal it can be found by typeclass inference. Maybe for it's for exactly this reason. But we still seem to need to assume local attribute [instance] fact_one_le_two_ennreal in every file using it.

[Sebastien Gouezel]

I'd vote for registering fact_one_le_two as a global instance (as well as those for one_le_one and one_le_top): the user of euclidean spaces has absolutely no way to guess that she should include it, and it's important enough that we can make an exception to the no global fact rule.

[Johan Commelin]

cc @Mario Carneiro

[Sebastien Gouezel]

(And I'd also register the fact that 2 and 3 are prime, by the way :-)

[Mario Carneiro]

It's probably fine to have a small number of global fact instances with no assumptions. I'm not sure how often they come up in failed searches but I guess we have worse problems anyway

[Reid Barton]

The alternative is to add more lines like the already-existing

instance : finite_dimensional 𝕜 (euclidean_space 𝕜 ι) := by apply_instance
instance : inner_product_space 𝕜 (euclidean_space 𝕜 ι) := by apply_instance

(and ideally, put local attribute [instance] fact_one_le_two_ennreal in a small section with these instances, so that you already notice in the same file if there are more missing instances for euclidean_space)

[Sebastien Gouezel]

#11749

[Johan Commelin]

Should we time this, to measure the impact?

[Johan Commelin]

cc @Jannis Limperg

[Jannis Limperg]

I'll do a timing in the evening (when I'm at a PC with enough RAM to compile mathlib).

[Jannis Limperg]

Benchmark says no difference whatsoever.

[Johan Commelin]

@Jannis Limperg Thanks for doing this!

[Johan Commelin]

Is it posted somewhere?

[Johan Commelin]

Then we can link to it in the PR page, and kick it on the queue