finite free modules

Stream: maths

[Johan Commelin]

For LTE we need some stuff about finite free abelian groups. Since the int_smul refactor, we can completely transparently treat those as finite free $\Z$-modules. Ergo: we want a theory of finite free modules. It seems best from a Lean perspective to split this into finitely generated modules (we already have those) and free modules.

universe u

class module.free (R : Type*) (M : Type u) [comm_semiring R] [add_comm_monoid M] [module R M] :=
(exists_basis : ∃ {I : Type u), nonempty (basis I R M))

We can then have an instance saying that modules (i.e., vector spaces) over a field are always free.

I also suggest replacing [finite_dimensional K V] everywhere by [module.finite K V]

I would also like to generalize finrank from fields to rings. It could assume module.finite and module.free as assumptions, but we might as well just definite it to be 0 on nonsense input.

[Johan Commelin]

Feedback on this proposal is very welcome

[Johan Commelin]

(cc: @Anne Baanen @Mario Carneiro)

[Kevin Buzzard]

One caveat about finrank -- people sometimes talk about the rank of a projective module. Over an integral domain (say), a projective module has a well-defined rank, equal to the dimension of the vector space you get by tensoring up to the field of fractions, and this rank is well-behaved (e.g. under short exact sequences of projective modules. direct sums etc). For example the fractional ideals of a Dedekind domain are just (up to isomorphism) the projective rank 1 modules.

[Scott Morrison]

I wonder if we could call this one projective_rank?

[Anne Baanen]

A typeclass of free modules sounds like a good idea!

My main suggestion would be to have the index type and basis be directly accessible as (noncomputable?) definitions. In the bundled-basis refactor, I found that making the index type and basis a "real" definition, rather than an exists which you have to destructure, gets rid of some annoyances. So you can turn

begin
  obtain \<ι, b, hι\> := module.free_finite.exists_basis_fintype R M,
  letI : fintype ι := hι,
  exact whatever b
end

into

whatever (module.free_finite.basis_fintype R M)

and have the fintype instance be automatically inferred.

[Johan Commelin]

I guess we can even have module.free.basis_type R M, and infer a fintype instance for it in the presence of module.finite R M.

[Johan Commelin]

So we can decouple free and finite

[Johan Commelin]

@Riccardo Brasca there was a small discussion here

[Riccardo Brasca]

So the idea is to have something like

class free : Prop := (exists_basis : ∃ (I : Type), nonempty (basis I R M))
def basis_type : Type := classical.some hf.exists_basis

Or something different?

[Johan Commelin]

@Riccardo Brasca lgtm, and then instance : fintype (free.basis_type R M) under the assumption [module.finite R M]

[Johan Commelin]

etc

[Adam Topaz]

Why even have basis_type? I feel like the user should be made painfully aware whenever they choose a basis

[Riccardo Brasca]

Anne Baanen said:

A typeclass of free modules sounds like a good idea!

My main suggestion would be to have the index type and basis be directly accessible as (noncomputable?) definitions. In the bundled-basis refactor, I found that making the index type and basis a "real" definition, rather than an exists which you have to destructure, gets rid of some annoyances. So you can turn

begin
  obtain \<ι, b, hι\> := module.free_finite.exists_basis_fintype R M,
  letI : fintype ι := hι,
  exact whatever b
end

into

whatever (module.free_finite.basis_fintype R M)

and have the fintype instance be automatically inferred.

I was following Anne's suggestion, but maybe I misunderstood it.

[Anne Baanen]

Adam Topaz said:

Why even have basis_type? I feel like the user should be made painfully aware whenever they choose a basis

While I'm all in favour of punishing non-constructivists, think about the poor people who refactor something to do with bases and suffer the pain of having to fix up other people's usages of the axiom of choice :P

[Adam Topaz]

Anne Baanen said:

Adam Topaz said:

Why even have basis_type? I feel like the user should be made painfully aware whenever they choose a basis

While I'm all in favour of punishing non-constructivists, think about the poor people who refactor something to do with bases and suffer the pain of having to fix up other people's usages of the axiom of choice :P

Fair enough :smile:

[Anne Baanen]

Although I wouldn't mind having module.free contain data (in the form of a trunc (Σ ι, basis ι R M) I guess?)

[Adam Topaz]

Yea, I was just about to suggest that!

[Adam Topaz]

This makes it easier to obtain the type and basis at the same time

[Adam Topaz]

Although why trunc over nonempty?

[Adam Topaz]

class free : Prop :=
(exists_basis : nonempty (Σ (I : Type*), basis I R M))

looks reasonable to me

[Anne Baanen]

trunc is basically nonempty but you can still do limited computations with it (e.g. #print axioms trunc.lift contains no axioms)

[Adam Topaz]

Sure, I agree, but that's another universe variable one has to keep track of...

[Adam Topaz]

I don't know, I guess one should also decide what the universe level of I should be!

[Kevin Buzzard]

bleurgh if module.free contains data then you're looking at diamonds later on. This is punishing non-constructivists, which I am not at all in favour of!

[Kevin Buzzard]

Hmm, or maybe this is Ok if it's not a class?

[Johan Commelin]

It should be a class!

[Kevin Buzzard]

well then I am definitely against trunc. I vote for Prop. I was in the middle of writing a blog post about trunc and bases but then marking hit :-(

[Adam Topaz]

What about universes? I guess this works?

import linear_algebra.basis

universes u1 u2

variables (R : Type u1) (M : Type u2) [ring R] [add_comm_group M] [module R M]

class free : Prop :=
(exists_basis : nonempty (Σ (I : Type (max u1 u2)), basis I R M))

[Riccardo Brasca]

I like nonempty (Σ (I : Type (max u1 u2)), basis I R M) (and I don't understand trunc...)

[Johan Commelin]

The I should live in the same universe as M, I think

[Johan Commelin]

Because in principle a basis should be able to be a subtype of M.

[Riccardo Brasca]

Are you really against def basis_type := (nonempty.some hf.exists_basis).1? I get that choosing a base is evil, but here we are just naming it... mathematically this seems ok

[Johan Commelin]

I would be fine with that def'n

[Adam Topaz]

I think either max u1 u2 or just u2 is fine. We need the existence of a basis as a subtype as part of the API anyway

[Adam Topaz]

I mean we should just have something like this:

import linear_algebra.basis

universes u1 u2

variables (R : Type u1) (M : Type u2) [ring R] [add_comm_group M] [module R M]

def basis_to_subtype {I} (b : basis I R M) : basis (set.range b) R M := sorry

[Riccardo Brasca]

This is exactly basis.reindex_range :grinning:

[Adam Topaz]

I just asked library search and it didn't work, but good to know that we have it!

[Riccardo Brasca]

Probably because you need nontrivial R

[Adam Topaz]

So in this case i think using u2 as the universe of I would be better, since it would be easier to construct an instance of free given a basis using this reindex_range

[Adam Topaz]

Ah

[Adam Topaz]

Why is that needed for reindex_range?

[Adam Topaz]

docs#basis.reindex_range

[Riccardo Brasca]

It comes from docs#basis.injective

[Adam Topaz]

But that's also true over the trivial ring, isn't it?

[Riccardo Brasca]

I am thinking about what is a basis over the trivial ring

[Adam Topaz]

Oh I guess anything is a basis over the trivial ring

[Riccardo Brasca]

Now I am thinking about what is a module over the trivial ring...

[Adam Topaz]

The trivial module

[Riccardo Brasca]

And I think there is only the ring itself

[Adam Topaz]

Since 1 equals 0 in the ring

[Adam Topaz]

Yeah but think about what linear independence says... If a linear combination is zero then the scalars in the linear combination are all zero, but that's always true :rolling_on_the_floor_laughing:

[Adam Topaz]

And clearly any collection spans the trivial module

[Adam Topaz]

I guess if one adds the condition that the elements of a basis must be nonzero, then a basis over the trivial ring would have to be empty, and everything works

[Riccardo Brasca]

Ahahah, linear independence is really different

[Riccardo Brasca]

OK, I am going to add this

[Riccardo Brasca]

The correct way of saying that M is trivial is subsingleton M?

[Riccardo Brasca]

Ah, there is docs#module.subsingleton good to know

[Anne Baanen]

Kevin Buzzard said:

bleurgh if module.free contains data then you're looking at diamonds later on. This is punishing non-constructivists, which I am not at all in favour of!

trunc _ is a subsingleton so the diamond issue is only as bad as it is for decidable_eq. (I will not take a position as to whether decidable_eq unduly punishes non-constructivists :grinning:)

[Kevin Buzzard]

The reason Jason XY and I spent hours and hours writing finsum was precisely because of decidable_eq diamonds with finsets.

[Riccardo Brasca]

#7642 to get rid of nontrivial R.

[Scott Morrison]

I'm in favour of basis_type. If we want to make non-constructivists suffer just the right amount we could call it choose_basis or some_basis.

[Mario Carneiro]

How about exposing that it is a subset of the carrier set?

[Mario Carneiro]

instead of just being an arbitrary type (in an arbitrary universe!)

[Mario Carneiro]

IIRC that's how the vector basis theorem is stated anyway

[Mario Carneiro]

That is:

class free : Prop :=
(exists_basis : nonempty (Σ (I : set M), basis I R M))

[Scott Morrison]

I wrote exactly that on a branch yesterday. :-)

[Scott Morrison]

While we're on the topic of finite modules, why does finite_dimensional even exist? We should just be using module.finite throughout.

[Mario Carneiro]

what's the difference?

[Scott Morrison]

module.finite just says finitely generated. finite_dimensional is just a synonym for is_noetherian over a field.

[Scott Morrison]

src#finite_dimensional.iff_fg says these are equivalent

[Scott Morrison]

So I think it's just duplication at this point.

[Kevin Buzzard]

IIRC the point of being able to say that a vector space was finite dimensional is because that is what is being taught to first year mathematics undergraduates all over the world. I am a little unhappy that vector space disappeared and now this. Is there no way we can keep these things as abbreviations somehow? We're just making lean less accessible to mathematics undergraduates this way, although I wholly understand the reasons for it. I would just love there to be a way which we can switch on a way of saying finite dimensional vector space so we don't have to start telling them that they need to be proving theorems about ranks of Noetherian modules

[Johan Commelin]

@Kevin Buzzard would it be ok for you if vector_space were notation for module?

[Johan Commelin]

Of course that means that every module over every semiring is suddenly a vector_space...

[Damiano Testa]

Maybe I am saying something silly, since I do not really know what open_locale does, but could the name vector_space be a synonym of module only if open_locale vectors is present?

[Johan Commelin]

Certainly.

[Johan Commelin]

@Damiano Testa open_locale is just a way to execute a little bit of prerecorded code, typically of the form local notation blabla

[Kevin Buzzard]

Yes, I don't want everyone to be forced to eat vector spaces over rings!

[Scott Morrison]

There is a bit of an implementation issue to get rid of finite_dimensional in favour of module.free.

[Scott Morrison]

The problem is just that both is_noetherian and module.free are typeclasses, and in the presence of [field R] (or even [division_ring R]) they are equivalent. So the situation is highly prone to cycles...

[Scott Morrison]

But both are useful independently.

[Anne Baanen]

(I assume it would be module.free and module.finite together being equivalent to noetherian, since free can also imply infinite-dimensional, no?)

[Anne Baanen]

It would be cool if we introduced [[double_brackets]] syntax for "add this instance parameter and all the (missing) instance parameters it depends on", e.g. so that {R M : Type*} [[module R M]] stands for {R M : Type*} [semiring R] [add_comm_monoid M] [module R M].

Then we could do the following: define is_noetherian (R M : Type*) [[module R M]] [module.finite R M] := _ and use [[is_noetherian R M]] as parameters. The Noetherian -> finite implication (which should always hold, unless I misinterpret the meaning of module.finite) is provided syntactically and we can safely add the finite -> Noetherian implication as an instance assuming field/division_ring.

[Johan Commelin]

Why would that not create loops?

- I need `module.finite R M`
- Let's look for `module.noetherian`
- Ooh, we are over a field, might as well look for `module.finite`
- ...

[Anne Baanen]

I tried a while ago to hack up double brackets, but as I recall I had issues where adding more parameters made the elaborator angry because the De Bruijn numbering changed.

[Johan Commelin]

Ooh, angry elaborators are scary!

[Anne Baanen]

Here's a quick example:

class foo (R : Type*). -- E.g. `ring`
class bar (R : Type*) extends foo R. -- E.g. `division_ring`

class rel (R M : Type*) [foo R]. -- E.g. `module.finite`
class rel2 (R M : Type*) [foo R] [rel R M]. -- E.g. `is_noetherian`

def uses_rel2 (R M : Type*) [foo R] [rel R M] [rel2 R M] := 0

instance rel_to_rel2 (R M : Type*) [bar R] [rel R M] : rel2 R M := ⟨⟩

set_option trace.class_instances true

example (R M : Type) [bar R] [rel R M] := uses_rel2 R M

[Anne Baanen]

Instance trace:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : @rel2 R M (@bar.to_foo R _inst_1) _inst_2 := @rel_to_rel2 ?x_1 ?x_2 ?x_3 ?x_4
[class_instances] cached instance for bar R
_inst_1
[class_instances] caching instance for @rel2 R M (@bar.to_foo R _inst_1) _inst_2
@rel_to_rel2 R M _inst_1 _inst_2

[Anne Baanen]

This also works when there are no instance parameters to the declaration itself:

instance : bar ℕ := {}
instance : rel ℕ ℤ := ⟨⟩

set_option trace.class_instances true

example := uses_rel2 ℕ ℤ

[Johan Commelin]

ooh, I see, noetherian assumes finite. So there is no instance going from noeth to finite.

[Johan Commelin]

But with all those mixins, I agree that the need for [[]] becomes higher and higher

[Scott Morrison]

My preference would not be to replace finite_dimensional with is_noetherian, but rather to replace finite_dimensional with module.finite. Hopefully this is much more manageable for undergraduates. (Further, I agree it would be good to add abbreviations back in for vector_space := module and finite_dimensional := module.finite if this can be done cleanly.)

This would require a good mechanism to promote module.finite to is_noetherian whenever we're working over a field (even a division ring), and this is what I'm unhappy about at the moment. We can't have a global instance, as it causes typeclass search loops. Perhaps a local instance is okay, or just manually invoking it, if it turns out it isn't needed too many times.

[Riccardo Brasca]

After a small break to work on LTE I am coming back to free modules (not necessarily finite). What do you think of the following?

class module.free : Prop :=
(exists_basis : nonempty (Σ (I : Type*), basis I R M))

[Riccardo Brasca]

There was some discussion about trunc, but even if I understand it better now (thank's Kevin!) I still don't if it is worth to use it

[Anne Baanen]

nonempty is fine for now, it would be nice to use trunc instead but that probably causes enough issues for you that it's not worth it.

[Kevin Buzzard]

trunc just has diamond risks which nonempty hasn't got

[Kevin Buzzard]

As a mathematician if someone said to me "you know it's free, now do you need the axiom of choice to get a basis" I would reply "of course". But that's only my mental model of what freeness means

[Riccardo Brasca]

And we want a lemma saying that this is equivalent to having a base in the same universe as the module, right?

[Anne Baanen]

Hmm, actually now that I look at it again, I'm worried that the Type* will cause extra universe parameters to pop up. One moment while I do some testing...

[Anne Baanen]

Yes, I : Type* gives unexpected errors:

import linear_algebra.basis

variables (R M : Type*) [semiring R] [add_comm_monoid M] [module R M]

class module.free : Prop :=
(exists_basis : nonempty (Σ (I : Type*), basis I R M))

open module.free

def choose_basis_index [module.free R M] : Type* := module.free.exists_basis.some.1
-- Error: Don't know how to synthesize placeholder : Type ?

def choose_basis [module.free R M] : basis (choose_basis_index R M) R M := module.free.exists_basis.some.2
-- Error: Type mismatch, has type _ : Type (max ?l_1 ?l_2 ?l_3) expected _ : Type (max ?l_1 u_1 u_2)

[Anne Baanen]

Fixed:

import linear_algebra.basis

variables (R M : Type*) [semiring R] [add_comm_monoid M] [module R M]

class module.free : Prop :=
(exists_basis [] : nonempty (Σ (I : set M), basis I R M))

open module.free

def choose_basis_index [module.free R M] : set M :=
(module.free.exists_basis R M).some.1

noncomputable def choose_basis [module.free R M] : basis (choose_basis_index R M) R M :=
(module.free.exists_basis R M).some.2

[Riccardo Brasca]

My idea was to prove first of all that the two defs are equivalent, using basis.reindex_range

[Riccardo Brasca]

But if we will never use the general one we can just go with the latter

[Anne Baanen]

Sure, that sounds like a good idea. The issue with the Type* formulation is that Lean can't figure out which universe I is supposed to belong to.

[Anne Baanen]

So you get infinitely many copies of module.free R M, one for each universe level. (And, while I don't think you can construct an explicit counterexample in mathlib's, in certain models of type theory there might not be a basis for M : Type 2 and I : Type 1, while there is one for M : Type 2 and I : Type 2. In other words, you might not be able to prove the equivalence of module.free.{1 2 2} and module.free.{2 2 2}.)

[Eric Wieser]

I can't even work out how to write the explicit universe version, despite it not being what we want anyway.

[Eric Wieser]

Ah, got it:

import linear_algebra.basis

class {w u v} module.free (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] :
  Prop :=
(exists_basis : nonempty (Σ (I : Type w), basis I R M))

open module.free

universes u v
variables (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M]

def {w} choose_basis_index [module.free.{w} R M] : Type w :=
(module.free.exists_basis : nonempty (Σ (I : Type w), basis I R M)).some.1

noncomputable def {w} choose_basis [module.free.{w} R M] : basis (choose_basis_index R M) R M :=
module.free.exists_basis.some.2

[Eric Wieser]

The elaborator needed a hand

[Anne Baanen]

import linear_algebra.basis

universes uI uR uM

variables (R : Type uR) (M : Type uM) [semiring R] [add_comm_monoid M] [module R M]

class module.free : Prop :=
(exists_basis [] : nonempty (Σ (I : Type uI), basis I R M))

open module.free

def choose_basis_index [module.free.{uI} R M] : Type uI := (module.free.exists_basis R M).some.1

noncomputable def choose_basis [module.free.{uI} R M] : basis.{uI} (choose_basis_index.{uI} R M) R M :=
(module.free.exists_basis R M).some.2

[Riccardo Brasca]

Indeed I am not able to prove

lemma module.free_def : module.free R M ↔ ∃ (I : Type v), nonempty (basis I R M)

v here is the universe of M

[Riccardo Brasca]

The first implication is easy, but not the other

[Anne Baanen]

Exactly, if I's universe in on the left hand side is lower than v, there are models where that implication does not hold.

[Riccardo Brasca]

Hm, I don't really understand all the problems here, but it seems to me that requiring the base to be in the same universe as the module is the easiest thing to do

[Johan Commelin]

Yes, I would make the universes of I the same as that of M.

[Kevin Buzzard]

What Johan said. Riccardo, here is a way of thinking about universes. We have the Prop universe, where every type has 0 or 1 terms! Now there is not a "finite" universe of finite types, but you could pretend that there was, because fintype satisfies most of the axioms which universes have to satisfy. And then there is Type which is a proper mathematical universe, big enough to have things in like the real numbers and more generally the sort of things we need to do mathematics (and for those people who don't use category theory in their work, this universe is big enough for everything they do). Now clearly if you have a free module in Type you don't want to start looking for a basis in Fintype because it might not be finitely generated. Similarly there might well be free modules in Type 2 which don't have a basis in Type -- mathematically you might say that any "module" which is not actually a set (e.g. the real "vector space" with a basis equal to all ordinals or whatever your favourite class which is not a set is) can't have a basis which is a set.

It's almost never right to put extra universe variables in definitions, i.e. a new universe variable which appears in the term of a definition but not the type of the definition.

The one thing to be careful of with set is that it is not quite the right notion for the zero ring. I don't know how much of an issue this is. The zero module has got a basis of size 37, namely the ordered 37-tuple (0,0,0,...,0). This basis cannot be expressed with the set trick. However, because you are only defining a Prop this should not be an issue, and the zero ring has to be treated separately in much of the theory of bases anyway.

[Eric Wieser]

One thing that I noticed when looking at the module.finite stuff is that if you do want free universes, you usually don't care about having them in an iff. That is, you usually want something like:

from_some_universe : ∃ (I : Type w), nonempty (basis I R M) → module.free R M
to_set : module.free R M → ∃ (I : set M), nonempty (basis I R M)

What's convenient when going in one direction is very different to what's convenient going in the other direction

[Riccardo Brasca]

This seems reasonable to me

import linear_algebra.basis

universes u v w

variables (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M]

class module.free : Prop :=
(exists_basis [] : nonempty (Σ (I : Type v), basis I R M))

lemma module.free_def : module.free R M ↔ ∃ (I : Type v), nonempty (basis I R M) :=
⟨λ h, ⟨set.range h.exists_basis.some.2, ⟨basis.reindex_range h.exists_basis.some.2⟩⟩,
    λ h, ⟨nonempty_sigma.2 h⟩⟩

lemma module.free_iff_set : module.free R M ↔ ∃ (S : set M), nonempty (basis S R M) :=
⟨λ h, ⟨set.range h.exists_basis.some.2, ⟨basis.reindex_range h.exists_basis.some.2⟩⟩,
    λ ⟨S, hS⟩, ⟨nonempty_sigma.2 ⟨S, hS⟩⟩⟩

lemma of_basis {ι : Type w} (b : basis ι R M) : module.free R M :=
(module.free_def R M).2 ⟨set.range b, ⟨b.reindex_range⟩⟩

[Riccardo Brasca]

So in practice to prove that something is free it is enough to have a basis (regardless of the universe), and if something is free we have the index type in the same universe of the module, or the index set if we prefer

[Eric Wieser]

This might also be a nice way to write it, using doc#small to promise that the w used is one that M fits into, even if its not the same universe as v

import logic.small

lemma module.free_def [small.{w} M] : module.free R M ↔ ∃ (I : Type w), nonempty (basis I R M) :=
⟨ λ h, ⟨shrink (set.range h.exists_basis.some.2),
    ⟨(basis.reindex_range h.exists_basis.some.2).reindex (equiv_shrink _)⟩⟩,
  λ h, ⟨(nonempty_sigma.2 h).map $ λ ⟨i, b⟩, ⟨set.range b, b.reindex_range⟩⟩⟩

[Riccardo Brasca]

Nice!

[Eric Wieser]

But even with that definition, your of_basis is still needed, I think

[Anne Baanen]

It's at least a nice piece of glue code for the common case where there is an explicit basis.

[Riccardo Brasca]

Sure, that is more general. If you have a basis, indexed by a type in any universe, then the module is free

[Riccardo Brasca]

But the converse is indeed false

[Eric Wieser]

is the the case that the existence of a basis indexed by I : type wimplies M : type v is w-small?

[Eric Wieser]

That is, can this sorry be filled?

lemma module.free_def : (∃ [small.{w} M], module.free R M) ↔ ∃ (I : Type w), nonempty (basis I R M) :=
⟨ λ h, by casesI h with _ h; exact (let b := h.exists_basis.some.2 in ⟨shrink (set.range b),
    ⟨(basis.reindex_range b).reindex (equiv_shrink _)⟩⟩),
  λ h, ⟨sorry, ⟨(nonempty_sigma.2 h).map $ λ ⟨i, b⟩, ⟨set.range b, b.reindex_range⟩⟩⟩⟩

[Anne Baanen]

We have that M is in bijection with I →₀ R, which is in universe max w u

[Anne Baanen]

So it should be possible to show M is max w u-small

[Anne Baanen]

(I don't know the API around docs#small well though.)

[Eric Wieser]

No, me neither, nor is it probably worth spending too much time worrying about it

[Anne Baanen]

Untested, but should work:

theorem small_of_basis {R : Type u} {M : Type v} {I : Type w} (b : basis I R M) : small.{max w u} M := small.mk' b.repr.to_equiv

[Eric Wieser]

Then the question becomes "can I replace [small.{w} M] with [small.{max w u} M] in the above lemma, or does that make the other direction false?". It certainly makes my proof not work any more

[Anne Baanen]

Hmm, can't think of any easy counterexamples (e.g. if u is big and w is small, then M := I →₀ R shows I can live in a smaller universe than M, but the converse is still OK), though I wouldn't be surprised if max w u is too big for the implication to hold.

[Kevin Buzzard]

If R is the zero ring (in any universe) then it doesn't matter which universe I lives in, I →₀ R can be descended to Type (and even to Prop).

[Kevin Buzzard]

Another way of putting it : if R : Prop then I →₀ R : Prop, which makes me wonder whether imax is relevant.

[Riccardo Brasca]

I've opened the WIP PR #7722. If you have some comments and/or request for any features don't hesitate to write there!

[Riccardo Brasca]

The linter complains about

def choose_basis_index := (exists_basis R M).some.1

saying

/- The `has_inhabited_instance` linter reports: -/
/- TYPES ARE MISSING INHABITED INSTANCES: -/
#print module.free.choose_basis_index /- inhabited instance missing -/

Is it telling me something I I should care about or can I just disable it? The basis index can be empty (for the trivial module).

[Kevin Buzzard]

Did you prove that e.g. a subsingleton module has an empty basis, or that R has a basis of size 1? You can just use such an example to satisfy the linter

[Johan Commelin]

In case you want to disable it: put @[nolint has_inhabited_instance] above it.

[Riccardo Brasca]

I mean,

instance foo : inhabited (choose_basis_index R M) := sorry

is false in general. I can prove

instance foo [nontrivial M] : inhabited (choose_basis_index R M) := sorry

that make the linter happy, so my question is whether I should provide this instance or disable the linter.

[Kevin Buzzard]

Right, but instance foo : inhabited (choose_basis_index int int) is true and this will also make the linter happy.

[Kevin Buzzard]

I have never understood the point of this linter

[Riccardo Brasca]

I am also confused. I thought it was telling me "this type can be empty, are you sure do you want to work with it?". So I am surprised that telling him that sometimes it's not empty makes it happy

[Kevin Buzzard]

I think it just needs a proof that it's not globally empty, for some reason. Quite what happens when you define the empty type I don't know.

[Riccardo Brasca]

Ah, you mean empty as Pi type or whatever

[Kevin Buzzard]

right

[Eric Wieser]

I think the goal is mainly to prevent you declaring a structure whose proof fields result in a contradiction. It doesn't protect against your fields only being compatible in a degenerate case

[Bryan Gin-ge Chen]

My understanding is that the intention of the linter is to nudge contributors to provide some basic instances of new types whenever possible. If adding an inhabited instance with an extra typeclass assumption is possible and potentially useful / instructive for future mathlib users, great! However, I don't think it's a big deal if you choose to disable it with the nolint attribute.

[Riccardo Brasca]

I understand it for classes, I provided module.free and of course I want to have some instance of it (I already have). It is complaining about the type that indexes the basis of a free module. I think I will just disable it, I feel a little uncomfortable in calling "default" a random element in a random module over a random ring

[Riccardo Brasca]

Adding the instance [module.free] for polynomial rings I noticed that we have docs#mv_polynomial.basis_monomials but there is no version for polynomial R, so I wanted to provide it. Because of the structure of the import, it seems to me a little complicated to do it directly, so I thought to use docs#mv_polynomial.punit_alg_equiv (polynomials are mv_polynomial indexed by punit). So far so good, so I tried to prove this

import ring_theory.mv_polynomial.basic

universe u

variables {R : Type u} [comm_ring R]

def polynomial.basis_monomials : basis ℕ R (polynomial R) :=
begin
  refine basis.map _ (mv_polynomial.punit_alg_equiv R).to_linear_equiv,
  refine basis.reindex _ ((equiv.punit_arrow_equiv ℕ)),
--  refine basis.reindex _ finsupp.equiv_fun_on_fintype,
--  exact mv_polynomial.basis_monomials punit R,
end

But I get the error

type mismatch at application
  ?m_1.reindex (equiv.punit_arrow_equiv ℕ)
term
  equiv.punit_arrow_equiv ℕ
has type
  equiv.{(max ?l_1 1) 1} (punit.{?l_1} → nat) nat : Sort (max ?l_1 1)
but is expected to have type
  equiv.{?l_1+1 1} (punit.{?l_2} → nat) nat : Type ?l_1

I think that the problem is that equiv.punit_arrow_equiv ℕ : Sort (max ? 1), but basis.reindex wants a Type. Is there a simple way to avoid this ? Thank's!

[Anne Baanen]

I believe the issue is that Lean can't figure out that max ? 1 is always at least 1 until the ? becomes a "real" universe variable. It works if you do the definition in opposite order:

import ring_theory.mv_polynomial.basic

universe u

variables {R : Type u} [comm_ring R]

noncomputable def polynomial.basis_monomials : basis ℕ R (polynomial R) :=
begin
  refine ((mv_polynomial.basis_monomials punit R).reindex _).map _,
  { exact finsupp.equiv_fun_on_fintype.trans ((equiv.punit_arrow_equiv ℕ))},
  { exact (mv_polynomial.punit_alg_equiv R).to_linear_equiv },
end

[Anne Baanen]

Although I would avoid using a tactic block for data:

noncomputable def polynomial.basis_monomials : basis ℕ R (polynomial R) :=
((mv_polynomial.basis_monomials punit R).reindex
  (finsupp.equiv_fun_on_fintype.trans (equiv.punit_arrow_equiv ℕ))).map
  (mv_polynomial.punit_alg_equiv R).to_linear_equiv

[Anne Baanen]

A more general solution is to turn the Type* parameters in linear_algebra.basis into Sort*. I expect that nothing, or very little, will break if we do so.

[Riccardo Brasca]

Your proof works, thank's! I am seeing what happens using Sort*

[Riccardo Brasca]

Do we have something like the direct sum of free modules is free? I mean, using basis...

[Anne Baanen]

On the direct sum of copies of M you can go via finsupp: docs#finsupp_lequiv_direct_sum and docs#finsupp.basis

[Anne Baanen]

I can't find anything for the direct sum of different modules or dfinsupp, though it shouldn't be hard to define it directly using basis.of_repr.

[Riccardo Brasca]

Thank's !

[Anne Baanen]

Something like this in linear_algebra/dfinsupp.lean:

def basis {η : ι → Type*} (b : Π i, basis (η i) R (M i)) :
  basis (Σ i, η i) R (Π₀ i, M i) :=
basis.of_repr ((map_range.linear_equiv (λ i, (b i).repr)).trans
  sorry)

[Anne Baanen]

Where the sorry is (Π₀ (i : ι), η i →₀ R) ≃ₗ[R] (Σ (i : ι), η i) →₀ R (which doesn't seem to exist yet, but should be true...)

[Riccardo Brasca]

I will take care of this later today or tomorrow (watching Kevin's talk right now)

[Eric Wieser]

What's that equivalence called for the non-finsupp version? Is it docs#equiv.Pi_curry?

[Riccardo Brasca]

Sorry for the late reply, I've been a little bit sick in the last few days.

I am trying to prove (Π₀ (i : ι), η i →₀ R) ≃ₗ[R] (Σ (i : ι), η i) →₀ R, but I am having troubles even in stating it. Indeed, Lean seems unable to find the instance module R (Π₀ (i : ι), η i →₀ R). I think that the problem is that in general, to have an instance module R (Π₀ (i : ι), β i) we want an instance [Π (i : ι), module R (β i)]. In this case β i = η i →₀ R and of course Lean is able to find [module R (η i →₀ R)] for a fixed i : ι, but I guess is not able to produce [Π (i : ι), module R (η i →₀ R)].

Any help is appreciated :)

[Anne Baanen]

First of all, I hope you feel better soon!

[Riccardo Brasca]

Thank's, it's nothing serious!

[Anne Baanen]

I think I had the same problem with finding Π i, module R (M i) instances before, let me see if I can find it somewhere...

[Eric Wieser]

I've usually had to restate dfinsupp.module locally with my precise assumptions

[Eric Wieser]

Typically it's something like you have add_comm_group (M i) but the definition mathlib has wants only add_comm_monoid (M i), and typeclass search gets confused by all the binders

[Anne Baanen]

Found the thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Inference.20faiing.2C.20but.20not.20inside.20a.20.CE.BB

[Anne Baanen]

The issue is that the elaborator doesn't figure out that finsupp.has_zero _ can be unified with finsupp.add_zero_class.to_has_zero _.. Here's a hack that seems to work:

import linear_algebra.finsupp

local attribute [-instance] mul_zero_class.to_has_zero finsupp.has_zero finsupp.add_zero_class finsupp.add_monoid

example {ι R : Type*} [semiring R] {η : ι → Type*} [Π i, add_comm_monoid (η i)] [Π i, module R (η i)] :
  (Π₀ (i : ι), η i →₀ R) ≃ₗ[R] (Σ (i : ι), η i) →₀ R :=
  _

[Anne Baanen]

(I went through the pp.all output of the failing instance and the definition of dfinsupp.add_comm_monoid and disabled all instances that appeared in the failing instances but not in the definition.)

[Riccardo Brasca]

Ah thank you! I was trying to understand what was going on, but it seems a little more advanced for me

[Riccardo Brasca]

So I am trying to prove

import linear_algebra.dfinsupp

variables {ι : Type*} {R : Type*} {η : ι → Type*} {N : Type*}
variables [semiring R] [add_comm_monoid N] [module R N]

noncomputable theory
open_locale classical

local attribute [-instance] mul_zero_class.to_has_zero finsupp.has_zero
  finsupp.add_zero_class finsupp.add_monoid

def sigma_finsupp_lequiv_dfinsupp : ((Σ i, η i) →₀ N) ≃ₗ[R] (Π₀ i, (η i →₀ N)) :=
{ to_fun := λ f, dfinsupp.mk (finsupp.split_support f) (λ i, finsupp.split f _),
  map_add' := sorry,
  map_smul' := sorry,
  inv_fun := sorry,
  left_inv := sorry,
  right_inv := sorry }

But map_add' seems quite painful: I can do it (I think) by several by_cases, looking at f.split_support, g.split_support and (f + g).split_support. Do someone see a better way of doing this?

[Riccardo Brasca]

Hmm, I will open a new topic with this problem, it is not directly related to free modules.

[Riccardo Brasca]

Is the following

lemma finprod {ι : Type*} [fintype ι] {M : ι → Type*} [Π (i : ι), add_comm_monoid (M i)]
[Π (i : ι), module R (M i)] [Π (i : ι), module.free R (M i)] : module.free R (Π i, M i) :=

the correct way of saying that a finite product of free modules is free? Or should I use some finset directly?

[Anne Baanen]

That matches the phrasing in docs#pi.basis, so sounds good to me.

[Johan Commelin]

Yes , and you could even make it an instance. I would call it free.pi (the fintype assumption is implicit in the name)

[Eric Wieser]

pi.module.free might be better

[Eric Wieser]

To match pi.module

[Eric Wieser]

Lean doesn't generate good names for typeclasses containing a dot as far as I know