finite_dimensional and finite

Stream: maths

[Riccardo Brasca]

We currently have docs#finite_dimensional (that is defined as is_noetherian over a division ring) and docs#module.finite. The two notion coincide (over a division ring), and mathlib essentially know this. Should we try to get rid of finite_dimensional? A lot of results in linear_algebra.finite_dimensional hold for finitely generated free modules, and should be stated in that generality. This is in the same spirit as throwing away vector_space.

[Riccardo Brasca]

I am pretty sure this has already been discussed, but I don't find the conversation.

[Johan Commelin]

Related, but even less mathematical: all the names talk about dim but the Lean function is called finrank. I propose making both shorter by replacing them by rk.

[Riccardo Brasca]

Totally agree.

[Riccardo Brasca]

Here is the previous discussion.

[Eric Wieser]

That's not true is it? I thought dim referred to module.rank not finrank

[Eric Wieser]

I made a branch to rename them, but ran into a clash with docs#rank

[Johan Commelin]

Ooh, maybe I misremembered. At least, the names don't line up well, and we should fix this.

[Eric Wieser]

Should we rename docs#rank to linear_map.rank?

[Johan Commelin]

Yes! That doesn't belong in _root_, I think.

[Riccardo Brasca]

And f.rank is nice!

[Riccardo Brasca]

The problem with finite and finite_dimensional is that we cannot have an instance saying that, over a division ring, finite implies finite_dimensional, since the latter is by definition is_noetherian, that implies finite, we have a loop.
A possible solution is to get rid completely of finite_dimensional, and not having finite → is_noetherian as an instance, but only as a lemma. Theorems about vector spaces should have finite as assumption, rather than is_noetherian.

[Anne Baanen]

That seems to be the correct pattern: if we have A → B always and C → (A ↔ B), then A → B is an instance, C → B → A a lemma, and anything that needs both C and B assumes C and A instead. In this case, A is finite_dimensional = is_noetherian, B is module.finite and C is division_ring.

[Riccardo Brasca]

I've created #9854. I modified the definition of finite_dimensional as

@[reducible] def finite_dimensional (K V : Type*) [division_ring K]
  [add_comm_group V] [module K V] := module.finite K V

(of course the goal is to get rid of finite_dimensional, but let me start with this). Now I have to modify quite a lot of proofs. For example

instance finite_dimensional_submodule [finite_dimensional K V] (S : submodule K V) :
  finite_dimensional K S :=
is_noetherian.iff_dim_lt_omega.2 (lt_of_le_of_lt (dim_submodule_le _) (dim_lt_omega K V))

becomes

instance finite_dimensional_submodule [finite_dimensional K V] (S : submodule K V) :
  finite_dimensional K S :=
begin
  letI : is_noetherian K V := iff_fg.2 _,
  exact iff_fg.1
    (is_noetherian.iff_dim_lt_omega.2 (lt_of_le_of_lt (dim_submodule_le _) (dim_lt_omega K V))),
  apply_instance,
end

Does someone see a better way of doing this? I mean, without starting every new proof with letI : is_noetherian K V := iff_fg.2 _, and using iff_fg.1 at the end. I can do it without problems, I just want to check I am not wasting time...

[Riccardo Brasca]

Nonsense

[Anne Baanen]

Riccardo Brasca said:

I've created #9854. I modified the definition of finite_dimensional as

@[reducible] def finite_dimensional (K V : Type*) [division_ring K]
  [add_comm_group V] [module K V] := module.finite K V

(of course the goal is to get rid of finite_dimensional, but let me start with this). Now I have to modify quite a lot of proofs. For example

instance finite_dimensional_submodule [finite_dimensional K V] (S : submodule K V) :
  finite_dimensional K S :=
is_noetherian.iff_dim_lt_omega.2 (lt_of_le_of_lt (dim_submodule_le _) (dim_lt_omega K V))

becomes

instance finite_dimensional_submodule [finite_dimensional K V] (S : submodule K V) :
  finite_dimensional K S :=
begin
  letI : is_noetherian K V := iff_fg.2 _,
  exact iff_fg.1
    (is_noetherian.iff_dim_lt_omega.2 (lt_of_le_of_lt (dim_submodule_le _) (dim_lt_omega K V))),
  apply_instance,
end

Does someone see a better way of doing this? I mean, without starting every new proof with letI : is_noetherian K V := iff_fg.2 _, and using iff_fg.1 at the end. I can do it without problems, I just want to check I am not wasting time...

I believe that is the best option, and the hope is you eventually prove enough stuff for module.finite that you don't need is_noetherian anymore.

[Riccardo Brasca]

#9854 should now compile. finite_dimensional is still there, but now is by definition module.finite. I will upgrade the doc before marking the PR ready for review (in any case it depends on #9860).
The next step will be to remove finite_dimensional completely.

[Riccardo Brasca]

finite_dimensional R M is now by definition module.finite R M. Do we want to delete it completely? Or should it be an abbreviation or something like that?

[Johan Commelin]

I'm inclined to remove it completely.

[Johan Commelin]

Maybe in Lean 4 we can have module K V pretty print as vector_space K V whenever there is an instance [field K] around. Similar for finite_dimensional etc... But in Lean 3 this all won't work.

[Yaël Dillies]

Gonna be a big bump for my branches :sweat_smile:

[Yakov Pechersky]

I have to change code of

-- An m × n matrix has some finite basis of cardinality m * n
example : ∃ (s : finset (matrix (fin m) (fin n) ℝ)) (b : basis s ℝ (matrix (fin m) (fin n) ℝ)),
            (finset.card s = m * n) :=
begin
  letI : is_noetherian ℝ (matrix (fin m) (fin n) ℝ) := is_noetherian.iff_fg.mpr (by apply_instance),
  let s_basis := is_noetherian.finset_basis ℝ (matrix (fin m) (fin n) ℝ),
  refine ⟨_, s_basis, _⟩,
  rw [←finite_dimensional.finrank_eq_card_finset_basis s_basis,
      matrix.finrank_matrix],
  repeat { rw [fintype.card, finset.card_fin] }
end

to start with

  letI : is_noetherian ℝ (matrix (fin m) (fin n) ℝ) := is_noetherian.iff_fg.mpr (by apply_instance),

Is this the best-practices approach now?

[Riccardo Brasca]

This is going to work. A better thing to do is to check which result needs is_noetherian and see if you can generalize it to finite. But of course this requires more work

[Riccardo Brasca]

But note that the standard basis of matrices is already there

[Riccardo Brasca]

I am on my phone so it's not easy to find it, but I guess is something like matrix.std_basis

[Yakov Pechersky]

Thanks for checking. The result needing the instance is the first is_noetherian.finset_basis line. Yup, std_basis would be the explicit basis that would satisfy this, but I'm also trying to demo how to make general linear algebra statements, so I was hoping to keep the example and proof close.

[Riccardo Brasca]

If you want the dimension we have the general result using module.rank (and cardinals). What you want is probably in #9832

[Riccardo Brasca]

@Andrew Yang is working on generalizing Mathlib.LinearAlgebra.FiniteDimensional to free modules. Currently the situation is a little mess, with results (sometimes suboptimal) in Mathlib.LinearAlgebra.FiniteDimensional, Mathlib.LinearAlgebra.FreeModule.*, Mathlib.LinearAlgebra.Dimension and Mathlib.RingTheory.Finiteness.

I really think we should clean up everything, to make clear which results hold in general (over any ring, maybe with the strong rank condition), which one for free modules, and which one for vector spaces (over division rings).

My first question is whether we want to keep docs#FiniteDimensional: currently it is a reducible def

@[reducible]
def FiniteDimensional (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V] :=
  Module.Finite K V

so we can easily get rid of it if we want.

[Riccardo Brasca]

#8912 for start

[Yaël Dillies]

Can we not rename Module.Finite to FiniteDimensional? This is not a very discoverable name.

[Johan Commelin]

But "dimension" suggests things like basis, and scalar fields, etc.

[Riccardo Brasca]

The terminology is completely standard (probably because we rarely care about modules that finite as sets), and nobody says "dimension" for module that are not over a field (even if they're free)

[Yaël Dillies]

Then we should keep FiniteDimensional as an abbreviation for discoverability.

[Kevin Buzzard]

Yes, I really like that "ring-finite" and "module-finite" have taken off; in the 90s when you had an R-algebra A you had "finite (when viewed as an A-module)" and "finite (when viewed as an A-algebra)".

[Riccardo Brasca]

We use docs#Algebra.FiniteType for that

[Andrew Yang]

The docstring in Mathlib.LinearAlgebra.FiniteDimensional explains why we have FiniteDimensional instead of using Module.Finite. To summarize: FiniteDimensional is the combination of Module.Finite and IsNoetherian and Module.Free. We just arbitrarily chose the first as a definition.

[Riccardo Brasca]

Anyway I don't have anything against FiniteDimensional, it can stays in its own file where we put results that hold only over a division ring.

[Riccardo Brasca]

Andrew Yang said:

The docstring in Mathlib.LinearAlgebra.FiniteDimensional explains why we have FiniteDimensional instead of using Module.Finite. To summarize: FiniteDimensional is the combination of Module.Finite and IsNoetherian and Module.Free. We just arbitrarily chose the first as a definition.

BTW do we have the equivalences as instances? In Lean 3 it was impossible to have all of them (because they cycle), but it should be possible in Lean 4.

[Eric Rodriguez]

Andrew Yang said:

The docstring in Mathlib.LinearAlgebra.FiniteDimensional explains why we have FiniteDimensional instead of using Module.Finite. To summarize: FiniteDimensional is the combination of Module.Finite and IsNoetherian and Module.Free. We just arbitrarily chose the first as a definition.

To me the docstring doesn't capture why we need them. Also, I think some of the steps in this cycle don't require division rings, right? (I'm thinking basis -> fg for example). So having two separate definitions seems weird

[Kevin Buzzard]

One argument is "think of the undergraduates" but I'm no longer convinced about how good an argument this is (because I have turned my attention to getting other people addicted).

[Andrew Yang]

For example we use IsDedekindDomain R instead of UniqueFactorizationMonoid (Ideal R) because

1. We didn't choose it as the main definition.
2. Even if we chose it, this choice is non-canonical and should be hidden as a implementation detail.

I believe it is the same case here?

[Andrew Yang]

Anyway, I plan to:

1. Generalize current results on FiniteDimensional into finite, free, and/or noetherian modules when possible.
2. Keep the lemmas above in terms of FiniteDimensional for discoverability and usability.
3. Split and reorganize Mathlib.LinearAlgebra.FiniteDimensional, Mathlib.LinearAlgebra.FreeModule.Rank, Mathlib.LinearAlgebra.FreeModule.Finite.Rank, Mathlib.LinearAlgebra.Dimension and Mathlib.RingTheory.Finiteness into a folder under LinearAlgebra.

[Andrew Yang]

Using the "jump to definition" feature on lemmas in 2. should make it clear what hypotheses are actually needed?

[Johan Commelin]

Sounds good!

[Eric Rodriguez]

I don't like step 2, I'm strongly against duplicating lemmas; could this just be written as an alias in the finite dimensional namescape?

[Andrew Yang]

The plan is to keep them as one lemma proofs.

[Riccardo Brasca]

You mean one line proof?

[Riccardo Brasca]

Is there a real difference between alias and one line proofs?

[Ruben Van de Velde]

An alias wouldn't actually be about FiniteDimensional, would it?

[Ruben Van de Velde]

Unless it's strictly an abbreviation

[Yaël Dillies]

Riccardo Brasca said:

Is there a real difference between alias and one line proofs?

Yes, the size of the diff, hence the reviewability of the PR.

[Ruben Van de Velde]

Is an alias more than one line?

[Yaël Dillies]

It's much easier to generalise lemmas if you don't have to worry about the call sites. Those can be dealt with in a later PR.

[Eric Rodriguez]

An alias is also right next to the call site, whilst a one line proof is usually in another file; much harder to maintain in this way.

[Yaël Dillies]

I mean, we're talking about a short transition period here, right? Those one-line lemmas could be around for less than a day.

[Riccardo Brasca]

Are we? In this case we should stop worrying, but if we want to keep them (for discoverability) we should think about it

[Yaël Dillies]

For discoverability, I think that it's important to keep FiniteDimensional around, but with a big flashing stroboscopic warning saying "if you want lemmas about me, instead look for lemmas about Module.Finite in files such and such".

[Eric Rodriguez]

I think lemmas will be made in the wrong generality if we keep FiniteDimensional around, too

[Yaël Dillies]

That might be better than lemmas not being made at all because people were put off?

[Eric Rodriguez]

I think what would end up happening is people coming on Zulip, asking why their PR isn't progressing, being told it's done in the wrong generality and to rewrite it all (e.g. SVD)

[Andrew Yang]

I think we should keep FiniteDimensional so that there is a unified spelling of finite dimensional vector spaces over division rings.
If we can make finite -> IsNoetherian an instance for modules, I'm fine with not restating lemmas. But they will still be kept until the refactor is done and removed in the end.

[Andrew Yang]

It should be easy to generalize results on finite-dimensional vector spaces to finite free modules though. Usually the proof still works and one just need to change the typeclass.

[Yaël Dillies]

Eric Rodriguez said:

I think what would end up happening is people coming on Zulip, asking why their PR isn't progressing, being told it's done in the wrong generality and to rewrite it all (e.g. SVD)

Great example! SVD (#6042) has been completely stalled for the past two months and a half :grinning:

[Riccardo Brasca]

Andrew Yang said:

I think we should keep FiniteDimensional so that there is a unified spelling of finite dimensional vector spaces over division rings.
If we can make finite -> IsNoetherian an instance for modules, I'm fine with not restating lemmas. But they will still be kept until the refactor is done and removed in the end.

It seems it already is. docs#isNoetherian_of_finite

[Andrew Yang]

That Finite is _root_.Finite not Module.Finite.

[Riccardo Brasca]

Note that I just said two hours ago that this terminology is not a problem :rolling_on_the_floor_laughing:

[Riccardo Brasca]

#8999

[Riccardo Brasca]

It worked like a charm :)