Zulip Chat Archive

Stream: new members

Topic: f.g. free modules


view this post on Zulip Sam Lichtenstein (May 28 2020 at 15:56):

How do I construct the free R-module RnR^n (including its R-module structure) for a natural number nn? 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 RnR^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 i1,ij0i\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 RR-linear map

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

where the source is the ii th copy of RR in {R}i:n\{R \}_{i:n} and the target is the product i:nRRnHomSet(n,R)=\prod_{i:n}R \cong R^n \cong \mathrm{ Hom}_\mathrm{Set}(n, R)= n→ R. Namely this map is the section to the ii th projection which is zero on all the jij\neq i factors, so the image of 1 under it is indeed the ii 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?

view this post on Zulip Bryan Gin-ge Chen (May 28 2020 at 16:01):

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.

view this post on Zulip Sam Lichtenstein (May 28 2020 at 16:02):

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

view this post on Zulip Sam Lichtenstein (May 28 2020 at 16:02):

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

view this post on Zulip Sam Lichtenstein (May 28 2020 at 16:03):

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

view this post on Zulip Sam Lichtenstein (May 28 2020 at 16:08):

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?

view this post on Zulip Bryan Gin-ge Chen (May 28 2020 at 16:14):

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.

view this post on Zulip Johan Commelin (May 28 2020 at 16:36):

@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.

view this post on Zulip Johan Commelin (May 28 2020 at 16:37):

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

view this post on Zulip Johan Commelin (May 28 2020 at 16:38):

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.

view this post on Zulip Johan Commelin (May 28 2020 at 16:39):

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

view this post on Zulip Sam Lichtenstein (May 30 2020 at 21:22):

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?

view this post on Zulip Sam Lichtenstein (May 30 2020 at 21:29):

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.

view this post on Zulip Kenny Lau (May 30 2020 at 21:31):

why not just use \io \to\0 R

view this post on Zulip Kevin Buzzard (May 30 2020 at 21:32):

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

view this post on Zulip Sam Lichtenstein (May 30 2020 at 21:33):

@Kenny Lau :

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

view this post on Zulip Kenny Lau (May 30 2020 at 21:34):

noncomputable example

view this post on Zulip Sam Lichtenstein (May 30 2020 at 21:35):

@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

view this post on Zulip Sam Lichtenstein (May 31 2020 at 17:44):

@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?

view this post on Zulip Sam Lichtenstein (May 31 2020 at 17:47):

(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.)

view this post on Zulip Kevin Buzzard (May 31 2020 at 19:10):

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?

view this post on Zulip Sam Lichtenstein (May 31 2020 at 21:12):

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.

view this post on Zulip Sam Lichtenstein (May 31 2020 at 21:16):

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)

view this post on Zulip Kevin Buzzard (May 31 2020 at 22:06):

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

view this post on Zulip Kevin Buzzard (May 31 2020 at 22:07):

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

view this post on Zulip Sam Lichtenstein (May 31 2020 at 22:16):

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.

view this post on Zulip Kevin Buzzard (May 31 2020 at 22:29):

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

view this post on Zulip Johan Commelin (Jun 01 2020 at 03:02):

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

view this post on Zulip Johan Commelin (Jun 01 2020 at 03:03):

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

view this post on Zulip Johan Commelin (Jun 01 2020 at 03:07):

@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.

view this post on Zulip Kevin Buzzard (Jun 01 2020 at 11:32):

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.

view this post on Zulip Sam Lichtenstein (Jun 01 2020 at 11:47):

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

view this post on Zulip Kevin Buzzard (Jun 01 2020 at 11:56):

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

view this post on Zulip Kevin Buzzard (Jun 01 2020 at 12:39):

OK so I'm catching up with the issues raised in this thread. direct_sum is for an arbitrary direct sum of RR-modules (and in particular is a dependent finsupp). This specific case of free RR-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?

view this post on Zulip Johan Commelin (Jun 01 2020 at 12:41):

We could define free in terms of ι →₀ R

view this post on Zulip Johan Commelin (Jun 01 2020 at 12:41):

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

view this post on Zulip Sam Lichtenstein (Jun 01 2020 at 13:09):

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?

view this post on Zulip Notification Bot (Jun 01 2020 at 13:57):

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


Last updated: May 12 2021 at 04:19 UTC