f.g. free modules

Stream: new members

[Sam Lichtenstein]

How do I construct the free R-module $R^n$ (including its R-module structure) for a natural number $n$? Ideally this would be done in a way that I can keep around n : ℕ for doing things like induction, should I wish to.

(The motivation is that I am trying to formalize the lemma that a torsion-free f.g. module over a domain injects into a f.g. free module. I might not actually need the standard f.g. free modules $R^n$ for this purpose, but in thinking about this I realized that it might be nice to know how to do things with them.)

Given a [fintype n] instance, the material in linear_algebra/basic.lean (in the pi section) produces the canonical R-module structure on n → R.

But when I attempted to work with the standard basis elements indexed by (i : n) corresponding to the maps $i\mapsto 1, i\neq j\mapsto 0$, I ran into what I think are universe issues. (Which seems funny because set-theoretic considerations cannot possibly be relevant when working with finite products, can they?) Here is a #mwe of what I am working on:

import linear_algebra.basic tactic linear_algebra.basis

universes u
variables {n : Type u} [fintype n]

variables (R : Type*) (M : Type*)
variables [comm_ring R] [add_comm_group M] [module R M]

def free := ∃B : set M, is_basis R (λ b, b : B → M)

lemma free_of_fg_free : free R (n → R) := sorry

-- From linear_algebra/matrix.lean, it seems to me I want to use the following in the proof:
variables (i : n)
 -- #check linear_map.std_basis R (λ_:n, R) i

The commented out #check statement mostly "works" but it raises the error

failed to synthesize type class instance for
n : Type u,
_inst_1 : fintype n,
R : Type u_1,
M : Type u_2,
_inst_2 : comm_ring R,
_inst_3 : add_comm_group M,
_inst_4 : module R M,
i : n
⊢ decidable_eq n

From unravelling the definitions, it seems that linear_map.std_basis R (λ_:n, R) i is indeed the canonical $R$-linear map

(λ (_x : n), R) i →ₗ[R] Π (i : n), (λ (_x : n), R) i

where the source is the $i$ th copy of $R$ in $\{R \}_{i:n}$ and the target is the product $\prod_{i:n}R \cong R^n \cong \mathrm{ Hom}_\mathrm{Set}(n, R)=$ n→ R. Namely this map is the section to the $i$ th projection which is zero on all the $j\neq i$ factors, so the image of 1 under it is indeed the $i$ th standard basis element.

Hence I think my ultimate question is really the following:

If I promise only to ever care about finitely generated modules over Noetherian rings, can I somehow set things up so that things like decidable_eq n "just work" and I never need to care or think about universes at all?

[Bryan Gin-ge Chen]

Putting open_locale classical right after your imports may work. decidable_eq doesn't have to do with universes, by the way. It's basically asking for an algorithm to decide equality of elements. If you don't care about "computing" with the objects you construct, then working with classical logic will make these all go away.

[Sam Lichtenstein]

Shouldn't equality of elements of a finite type be decidable in non-classical logic too?

[Sam Lichtenstein]

But thanks for that suggestion, it does sound like a pragmatic solution!

[Sam Lichtenstein]

Yes, that does indeed fix it, thanks @Bryan Gin-ge Chen !

[Sam Lichtenstein]

Aha, I had missed the fact that linear_algebra/basic.lean has open_locale classical buried in various places, and uses the classical tactic in others. Is another solution simply to put variables [deciable_eq n] somewhere in my file?

[Bryan Gin-ge Chen]

If open_locale classical is active, then you should be able to delete the occurrences of the classical tactic. I think we prefer using open_locale classical in most of mathlib. I don't have too much experience here, but I think you can run into situations where Lean gets two different decidable_eq assumptions and then gets confused.

[Johan Commelin]

@Sam Lichtenstein You can use (fin n) → R if you want to use a natural number n. The type fin n is the "canonical" type of cardinality n.

[Johan Commelin]

But probably you want to do as much as possible for general fintypes

[Johan Commelin]

If you want an example of how to do induction in such a setting, you can look at the proof of the Hilbert basis theorem, or the fact that R[X_1,...X_n] is an integral domain.

[Johan Commelin]

https://leanprover-community.github.io/mathlib_docs/ring_theory/polynomial.html#mv_polynomial.integral_domain_fintype

[Sam Lichtenstein]

I still have a basic question tangentially related to the above. Suppose I want to introduce the notation free R ι for the free module on a discrete type ι, i.e. direct_sum ι (λ _:ι, R). (For example, because I want to avoid typing (λ _:ι, R) over and over.) If I want Lean to "know" about my chosen notation, I figured out (eventually) that I can write:

import linear_algebra.basic linear_algebra.direct_sum_module

universes u v w u₁
variables (R : Type u) [ring R]
variables (ι : Type v) [decidable_eq ι]

def free := direct_sum ι (λ _:ι, R)
instance : add_comm_group (free R ι) := direct_sum.add_comm_group
instance : module R (free R ι) := direct_sum.module

-- these now work:
example (x y : free R ι) : free R ι := x + y
variables (r : R)
example (x : free R ι) : free R ι := r • x

Here are my questions:

Question 1a: Is this the "right" way to express the fact that I want to use some externally-defined structures with my own notation?
Question 1b: Is there a way I can "skip" specifying the add_comm_group instance, and have direct_sum.module infer it automatically (this boils down to inferring the additive structure on each copy of R, which direct_sum.add_comm_group seems to be perfectly able to do on its own).

Question 2: What if I want to work with this R-module structure without defining my free R ι notation for direct_sum ι (λ _:ι, R)? Consider these examples:

-- This works
example (x : direct_sum ι (λ _:ι, R)) : free R ι := r • x
-- This fails:
example (x : direct_sum ι (λ _:ι, R)) : direct_sum ι (λ _:ι, R) := r • x
-- these fail, complaining that "a declaration named 'direct_sum.add_comm_group' has already been declared"
instance : add_comm_group ( direct_sum ι (λ _:ι, R)) := direct_sum.add_comm_group
instance : module R ( direct_sum ι (λ _:ι, R)) := direct_sum.module

What exactly am I supposed to do to get example (x : direct_sum ι (λ _:ι, R)) : direct_sum ι (λ _:ι, R) := r • x to work?

[Sam Lichtenstein]

BTW, for Question 2, I know that I can do:

example (x : direct_sum ι (λ _:ι, R)) (r : R): direct_sum ι (λ _:ι, R) :=
begin
haveI := @direct_sum.module R _ ι _ (λ _:ι, R) _ _,
from r • x
end

I want to know what the analogue of the haveI is at the top level.

[Kenny Lau]

why not just use \io \to\0 R

[Kevin Buzzard]

It probably already has an R-module structure if you import the right thing

[Sam Lichtenstein]

@Kenny Lau :

example (x : ι →₀ R) (r : R) : ι →₀ R := r • x -- definition '_example' is noncomputable, it depends on 'finsupp.has_scalar'

[Kenny Lau]

noncomputable example

[Sam Lichtenstein]

@Kevin Buzzard yes, I assume I just need to know the right thing to import. I thought the instance direct_sum.module was the right thing, though

[Sam Lichtenstein]

@Johan Commelin Given s : finset x for an arbitrary type x, what's the right way to produce a bijection from s to fin s.card? It seems like there is a lemma finset.mono_of_fin that I could use if I somehow were to invoke the axiom of choice to put a decidable linear order on x, but that shouldn't be necessary, should it?

[Sam Lichtenstein]

(I suppose that in the spirit of #xy I should mention: I am trying to convert the hypothesis (⊤ : submodule R M).fg to the existence of a surjective R-linear map from a finitely generated free R-module to M.)

[Kevin Buzzard]

I'm sorry I'm not giving this thread more attention, I'm very much interested in it but I don't have much time for Lean right now. Why not just use the f.g. free module generated by the generating set of M?

[Sam Lichtenstein]

yes, that's indeed the one I want to use. but it's a little awkward to "get your hands on" the generating set of M. You get it as s : finset M. So you can construct a corresponding free module, either using s itself as the index type, or possibly more conveniently replacing the index type by fin s.card. I think I prefer the latter? Maybe I shouldn't. I wanted to state the lemma as

lemma surj_free_of_fg
    (hfg : (⊤ : submodule R M).fg) :
    ∃ (n : ℕ), ∃ (π : free R (fin n) →ₗ[R] M), (function.surjective π) := sorry

(Note that free R ι is an abbreviation for direct_sum ι (λ _:ι, R) aka ι →₀ R.) Here the existential quantification is over ℕ, which is not so scary. If you rephrase this as

lemma surj_free_of_fg
    (hfg : (⊤ : submodule R M).fg) :
    ∃ ι [fintype ι] , ∃ (π : free R ι →ₗ[R] M), (function.surjective π) := sorry

then the advantage is that the s : finset M you get from hfg is precisely the ι you are looking for. But the disadvantage is that the conclusion involves existential quantification for the ι, which I was scared of doing (because it involves a fintype instance in the ∃, which I am not sure is even allowed, and I think we also need to worry about a decidable_eq instance unless we've done open_locale classical).

Thus for now I was preferring the formulation in terms of fin n. To get the surjection from this free module to M you can invoke the universal property of coproducts, which requires really "having" a collection of maps R --> M indexed by the index type in question, i.e. an object of type Π(i:fin s.card), R --> M or Π(i:s), R --> M. These are the obvious maps that send 1 to the chosen generators. But the Prop that M (or rather its ⊤ submodule) is finitely-generated just gives the s : finset M, not an enumeration of that set. So to get a collection of maps of type Π (i:fin s.card), R --> M I need to choose such a bijection s --> (fin s.card), which was the motivation for my question to Johan.

[Sam Lichtenstein]

BTW what I am really trying to do is prove the structure theorem for modules over a PID, starting with the lemma about torsion-free modules on p. 35 of Pete Clark's notes http://math.uga.edu/~pete/integral.pdf. And what I am really really trying to do is formalize the existence of Jordan canonical form (with an eye towards applications such as Johan's feature request for Sylvester's law of inertia)

[Kevin Buzzard]

I think all of this is on Amelia's job list but she still has exams. I am interested in having Jordan canonical form in lean because it's essentially the only thing in Imperial's second year algebra course which isn't in it (we also don't have generalised eigenspaces but these will come with it basically). We also state the classification of finite abelian groups so I figured if we had the structure theorem we'd be able to kill two birds with one stone

[Kevin Buzzard]

I'll try to take a look at this asap but I am snowed under for hopefully at most one more day

[Sam Lichtenstein]

I am certainly not trying to step on anyone's toes if you already have a student (?) working on this stuff. It just seemed like an obvious gap in the library to me which I felt vaguely qualified to try to fill as a learning project. I'd be happy to defer to her if she is waiting to PR the same material, or to collaborate if she is looking for a collaborator.

[Kevin Buzzard]

I'm loath to bother her right now but if you're learning lean by working on this then I would keep going and not worry too much. Amelia is also involved in a huge refactor of localisations so she has plenty on her plate right now and although I don't want to put words in her mouth, it would not surprise me if she would be happy to collaborate. We can alert her to this thread on Tuesday when she's done

[Johan Commelin]

@Sam Lichtenstein Coming back to your question, I think there is a lemma fintype.exists_equiv or something like that.

[Johan Commelin]

Voila: src/data/fintype/basic.lean:theorem exists_equiv_fin (α) [fintype α] : ∃ n, nonempty (α ≃ fin n) :=
I think that's what you want.

[Johan Commelin]

@Sam Lichtenstein You could prove both versions. Use the second version of surj_free_of_fg to prove the first one. The \exists \iota [fintype \iota] is definitely allowed. I think open_locale classical is unexpected (even encouraged?!) in this part of the library.

[Kevin Buzzard]

I'm trying to catch up with this thread. I am confused by this doesn't work:

import linear_algebra.basic tactic linear_algebra.basis linear_algebra.direct_sum_module

variable (ι : Type*)

open_locale classical

variables (R : Type*) [comm_ring R]

--noncomputable instance foo : module R (direct_sum ι (λ _:ι, R)) := by apply_instance

noncomputable example (x : direct_sum ι (λ _:ι, R)) (r : R) : direct_sum ι (λ _:ι, R) := r • x

If I comment out the instance, which apparently is already there, it works.

[Sam Lichtenstein]

I didn’t know I could fix this error by writing “noncomputable” before example

[Kevin Buzzard]

You still get the error with the smul, but if I comment out the instance it fixes it

[Kevin Buzzard]

OK so I'm catching up with the issues raised in this thread. direct_sum is for an arbitrary direct sum of $R$-modules (and in particular is a dependent finsupp). This specific case of free $R$-modules is somehow easier because it's not dependent, but there is a cost to introducing a new definition like free: Kenny's suggestion of just using ι →₀ R has advantages and disadvantages. On the other hand the concept of a free module is so ubiquitous that probably one has to make the definition.

The second point is that I suspect there's no coercion from finset to Type :-(

example (X : Type) : has_coe_to_sort (finset X) := by apply_instance -- fails

There's a coercion from finset X to set X and then from there to Type*, but I don't seem to be able to get there directly.

example (X : Type) (s : finset X) : Type := (↑s : set X)

Should there be a coercion from finset X to Type directly?

[Johan Commelin]

We could define free in terms of ι →₀ R

[Johan Commelin]

I often write { x // x \in s }. But of course that's a very roundabout way to make a Type out of a finset

[Sam Lichtenstein]

Kevin, how should I think about the "cost" of introducing a new definition? Is the point that this is just one more thing that needs to be unfolded, so it introduces some fixed amount of overhead for simp etc in all downstream code?

[Notification Bot]

This topic was moved by Rob Lewis to #maths > f.g. free modules