A module with a finite basis is finite

Stream: general

[Riccardo Brasca]

In linear_algebra.free_module.finite.basic (how can I link a file and not a declaration?!) we have docs#module.finite.of_basis

lemma _root_.module.finite.of_basis {R : Type*} {M : Type*} {ι : Type*} [comm_ring R]
  [add_comm_group M] [module R M] [fintype ι] (b : basis ι R M) : module.finite R M :=

I wrote this, but I don't remember why I made it a lemma and not an instance. The easiest reason is that if it is an instance we get an error in docs#module.End.supr_generalized_eigenspace_eq_top

eigenspace.lean:526:4
maximum class-instance resolution depth has been reached

I don't see the problem, I tried with set_option trace.class_instances true, but the output is too long. Does someone see what is going wrong?

[Johan Commelin]

module.finite R M doesn't mention the basis b.

[Johan Commelin]

So the TC system has no way to find it.

[Johan Commelin]

If there was also some form of forward search, which sees basis ι R M in your context, and finds [fintype ι] and consequently invokes this instance, then that would be great. But that's not how TC inference works in Lean 3. It only works backwards from the goal.

[Riccardo Brasca]

Ah, I see, I thought it was somehow creating a loop.

[Riccardo Brasca]

In #10757 I've added the instance at least for fin n → R, that seems very reasonable. (Indeed it golfs at least one proof.)

[Johan Commelin]

Yeah, you can certainly add instances for special cases.

[Johan Commelin]

You can even generalize fin n to ι + [fintype ι].

[Yury G. Kudryashov]

Do we have an instance for Π i, M i with [fintype ι] [∀ i, module.finite R (M i)]?

[Yury G. Kudryashov]

We already have https://leanprover-community.github.io/mathlib_docs/linear_algebra/finite_dimensional.html#finite_dimensional.finite_dimensional_pi

[Riccardo Brasca]

finite_dimensional is now defined to be module.finite, so in #10757 I generalize docs#finite_dimensional.finite_dimensional_pi (that is for division_ring to any comm_ring. It is a Prop, so I don't think it is a problem to have both of them.
Sooner or later I will refactor linear_algebra.finite_dimensional to move all the generalizable results to linear_algebra.free_module.finite.* but it is quite a bit of work because of some problems with the import structure.

[Riccardo Brasca]

I wanted to do it one or two months ago but then I got absorbed by flt-regular...

[Riccardo Brasca]

OMG I forgot to update the docstring of docs#finite_dimensional, that still says "finite_dimensional vector spaces are defined to be noetherian modules"?! :scream:

[Riccardo Brasca]

Let me fix it.

[Riccardo Brasca]

#10758 (this PR is just a couple of lines)

[Floris van Doorn]

Riccardo Brasca said:

linear_algebra.free_module.finite.basic (how can I link a file and not a declaration?!)

file#linear_algebra/free_module/finite/basic

[Riccardo Brasca]

Thanks!