free module

Stream: maths

[Reid Barton]

The module `lc α β` of linear combinations over `β` (`α` is the scalar ring)
This is what I would call the free module on a set, right?

[Kenny Lau]

Unfortunately there \b needs to be a module or something

[Reid Barton]

oh, I see...

[Kenny Lau]

if you want module over a set you would want either direct_sum or finsupp

[Reid Barton]

Okay, I was wondering if there was something more specific than direct_sum.

[Reid Barton]

Actually, in my case the set does happen to be a module

[Kenny Lau]

then very good

[Reid Barton]

the module structure on lc is the one that doesn't use the module structure on \b right?

[Reid Barton]

because it's finsupp.to_module

[Kenny Lau]

nothing uses the module structure on \b

[Kenny Lau]

it's just lc that requires it

[Reid Barton]

oh wait, I lied. I have a subset of a module, not a module. Never mind

[Kenny Lau]

sadness

[Reid Barton]

Do we already have M → (R →ₗ[R] M)?

[Kenny Lau]

how about M \equiv\_l (R \to\_l[R] M)

[Reid Barton]

I think specializing direct_sum to the free module on a set would be worthwhile

[Reid Barton]

Here's what I ended up writing. I'm sure it could be golfed more.

universes u v

variables {R : Type u} [comm_ring R]

def lself (M : Type v) [add_comm_group M] [module R M] : (R →ₗ[R] M) ≃ₗ[R] M :=
{ to_fun := λ f, f 1,
  inv_fun := λ m, linear_map.id.smul_right m,
  left_inv := λ f, by ext r; simpa using (f.smul r 1).symm,
  right_inv := λ m, one_smul _ m,
  add := λ f g, rfl,
  smul := λ r f, rfl }

[Johannes Hölzl]

can you use smul_right for as inv_fun?

[Reid Barton]

oh, nice

[Reid Barton]

edited

[Reid Barton]

oh wait, I lied. I have a subset of a module, not a module. Never mind

Except actually I can also just use the entire module.

def projective (M : Type v) [add_comm_group M] [module R M] : Prop :=
∃ (f : M →ₗ[R] lc R M), (lc.total R M).comp f = linear_map.id

[Reid Barton]

is this definition too weird

[Johan Commelin]

I don't think mathematicians will recognise it

[Johan Commelin]

I think lc is somewhat unintuitive to use there

[Reid Barton]

do you mean because of the weird name, or because the definition itself is weird in a math way

[Johan Commelin]

I guess both :sad:

[Reid Barton]

I agree it's not very recognizable, and doing similar things for injective or flat modules will probably be worse

[Reid Barton]

On the other hand the usual definitions become not very pretty due to unbundled objects

[Reid Barton]

maybe I should give in and use category theory

[Johan Commelin]

I guess if it was called formal_lin_comb and didn't require \b to be a subset of a module, then it would be better.

[Johan Commelin]

Or at least the docstring could say that we are talking of formal linear combinations

[Mario Carneiro]

I am confused by this conversation. How can lc A B be a module if B isn't a module?

[Mario Carneiro]

Oh, I see, the B and A get flipped in the definition

[Mario Carneiro]

In finsupp, we have

def to_module {R:ring γ} [add_comm_group β] [module γ β] : module γ (α →₀ β)

I think this can be an instance now, and that can replace/generalize much of lc

[Kevin Buzzard]

That definition of projective is no weirder than Neil's definition of a localisation or mathlib's definition of a compact topological space

[Kevin Buzzard]

Who cares about weird definitions, use the definition that works best and write a useful interface relating it to other definitions people use in practice

[Kevin Buzzard]

I remember the first time I tried to use continuous functions, about a year ago, to prove something like multiplication by an element of a topological group was continuous. I thought "I can prove this from first principles" and started unfolding everything. Then Kenny saw what I was doing and said "you're not supposed to do it like that" and it began to dawn on me how this whole thing is supposed to work

[Kevin Buzzard]

We shouldn't ever really care about which definition we're using, we just need good docs which point us to all the theorems saying that the internal definition is equivalent to whichever definition we find is most convenient for us at the time. I don't even have a definition of projective in my head. I have 3 definitions and would claim that something is true "by definition" when I mean "by the definition which is most convenient for me at this point"

[Kevin Buzzard]

I have a proposition-definition of projective. "The following three concepts are equivalent -- so let's say a module is projective if it satisfies any one of them"

[Kevin Buzzard]

I'm happy to add Reid's more exotic one to the list

[Mario Carneiro]

In https://en.wikipedia.org/wiki/Projective_module it seems like all the definitions involve quantifying over all modules

[Mario Carneiro]

you didn't list any of wikipedia's definitions, but I like yours better

[Kevin Buzzard]

I was told "direct summand of a free" was the definition once

[Kevin Buzzard]

I was told "locally free" was the definition once

[Kevin Buzzard]

Ie all localisations were free modules

[Kevin Buzzard]

Neither of these involve quantifying over all modules

[Mario Carneiro]

direct summand of free quantifies over all modules

[Mario Carneiro]

dunno what locally free means

[Kevin Buzzard]

It means that for all prime ideals P of R, M tensor R_P is free

[Johan Commelin]

Just like you can localise rings, you can also localise modules (and you get a module over the localised ring)

[Mario Carneiro]

I guess with localizations it's a large quantification if you use Neil's localization and small if you use Kenny's localization

[Kevin Buzzard]

In ZFC we only use one universe

[Mario Carneiro]

yeah, then it's an impredicative definition

[Kevin Buzzard]

And so one definition of localisation I have been using for decades is

[Mario Carneiro]

not that it's usually a big problem, but sometimes it complicates size arguments

[Kevin Buzzard]

That all surjections in M's universe split

[Kevin Buzzard]

Hmm

[Kevin Buzzard]

Or is that R's universe?

[Mario Carneiro]

the surjections aren't in a universe, they are bounded by the given modules

[Mario Carneiro]

but I guess the N and M in the commutative triangle live in some universe

[Kevin Buzzard]

I was going to say that by some general nonsense one can deduce that if all surjections in a sensible universe split then all surjections spilt

[Mario Carneiro]

yes, that should be the case, but you want to start from a small definition to prove that

[Kevin Buzzard]

But I'm suddenly not sure what the sensible universe is

[Mario Carneiro]

I think it's the universe of P, the projective module itself

[Kevin Buzzard]

Because in this silly place R and M can be in different universes

[Mario Carneiro]

I'm not sure what happens if a large ring acts on a small module

[Kevin Buzzard]

It can happen

[Kevin Buzzard]

R + S is a ring

[Kevin Buzzard]

Making S a projective R module

[Kevin Buzzard]

So take R and S rings in different universes

[Kevin Buzzard]

S is projective because it's clearly locally free :-)

[Mario Carneiro]

clearly

[Kevin Buzzard]

It's free rank 1 over Spec (S) and free rank 0 over Spec(R)

[Mario Carneiro]

I wonder if the function f in Reid's definition should be data

[Kevin Buzzard]

I'm not qualified to answer that

[Mario Carneiro]

The commutative diagram suggests non-uniqueness, so maybe not

[Mario Carneiro]

is it "canonical"?

[Kevin Buzzard]

No

[Kevin Buzzard]

I'm glad to see you're learning the lingo

[Mario Carneiro]

huh, I just noticed that all 5 of the wikipedia definitions involve some existence statement

[Mario Carneiro]

oh, I get it, Reid's definition is the "dual basis" one

[Kevin Buzzard]

All surjections split is one definition of a projective module

[Kevin Buzzard]

Reid is using the universal surjection [EDIT: this is not quite true -- I resolve this issue about 30 posts down]

[Kevin Buzzard]

If that splits, they all do

[Kevin Buzzard]

I say this without any clear understanding of the details, which I'm currently trying to work out :-)

[Mario Carneiro]

My understanding is that lc is dumb and ever since the multiple-rings-on-a-module thing the previous definition of modules over finsupp is typeclassable, and can replace lc as the theory of free modules

[Mario Carneiro]

and we want projective, and to prove that free modules are projective

[Kevin Buzzard]

I can't work out the details :-/

[Kevin Buzzard]

My posts just above starting at "all surjections split" sound appealing but I can't make them rigorous

[Kevin Buzzard]

I'm finally at a computer. Reid's definition is related to "A module P is projective if and only if there is another module Q such that the direct sum of P and Q is a free module. "

[Kevin Buzzard]

If F is a module with a surjection F -> M, then this R-module map has a one-sided inverse if and only if "F is isomorphic to M plus kernel of the surjection"

[Kevin Buzzard]

This is not quite rigorous -- one should say the isomorphism between F and the direct sum identifies the surjection F -> M with the projection

[Kevin Buzzard]

Reid's definition is that M is projective iff a certain surjection from a certain explicit free module splits

[Kevin Buzzard]

so it's equivalent to saying that M is a direct summand of that very explicit free module

[Kevin Buzzard]

I guess that's a key thing that should be flagged for people who might not know this stuff back to front -- if M and N are modules and we have a surjection M -> N, then this surjection splitting is equivalent to M being isomorphic to N + kernel and the surjection being the projection

[Johan Commelin]

May we please have short exact sequences in Lean?

[Johan Commelin]

Once we have a good encoding for them, we can prove lots of interesting stuff.

[Kevin Buzzard]

Random surjections are harder than this, e.g. Z/4Z surjects onto Z/2Z but (a) this doesn't split and (b) Z/4Z is not Z/2Z + anything

[Kevin Buzzard]

(a) and (b) are equivalent statements

[Johan Commelin]

It's one of the things where I really don't know how to encode them in a nice way so that they are still intuitive to use. The mathematical notation is very compact.

[Kevin Buzzard]

A short exact sequence is surely just a predicate on three modules and two maps

[Johan Commelin]

I fear we will end up with short_exact f g. Which is really ugly.

[Kevin Buzzard]

Why is that ugly?

[Kevin Buzzard]

I agree that it's one approach

[Mario Carneiro]

I think drawing a picture every time is tiresome

[Kevin Buzzard]

OTOH a morphism of short exact sequences is maps on the modules

[Kevin Buzzard]

and I'm finding it hard to see the modules in Johan's proposal

[Johan Commelin]

"Let $0 \longrightarrow A \stackrel{f}{\longrightarrow} B \stackrel{g}{\longrightarrow} C \longrightarrow 0$ be a short exact sequence" is much nicer to read.

[Mario Carneiro]

like I said, drawing a picture

[Kevin Buzzard]

That's just the notation we should use :-)

[Kevin Buzzard]

I think unicode notation is rubbish. We need LaTeX notation.

[Kevin Buzzard]

I heard that @Patrick Massot was working on this in between his 16 hours / week of teaching ;-)

[Mario Carneiro]

notation `[0→ ` A ` →[` f `] ` B `→[` g `] ` C ` →0]` := short_exact f g

[Johan Commelin]

Ok... too bad we can use that to introduce them...

variables ([0→ A →[f] B →[g] C →0] : short_exact_sequence (Mod R))

[Mario Carneiro]

oh wait, this isn't even enough, I have to annotate that this is about linear maps somewhere

[Johan Commelin]

oh wait, this isn't even enough, I have to annotate that this is about linear maps somewhere

That's hidden in short_exact I guess.

[Mario Carneiro]

yes but if you want the same notation for group homs then it will be overloaded

[Johan Commelin]

I guess I want it for objects of an additive category?

[Mario Carneiro]

how about no

[Mario Carneiro]

this is a ridiculous notation

[Kevin Buzzard]

Will that notation work? We want A to be the domain of f.

[Mario Carneiro]

the variables notation won't work

[Mario Carneiro]

for the rest of it, sure, if you stick a _l at the end or something

[Kevin Buzzard]

It's not a ridiculous notation, it's just an example of how mathematicians think -- in a non-CS-y way.

[Mario Carneiro]

or use local notations... actually please use local notations for this

[Kevin Buzzard]

Mathematicians reason by drawing diagrams sometimes.

[Kevin Buzzard]

This is hard to do in Lean.

[Mario Carneiro]

You can't introduce five variables in a diagram in lean

[Kevin Buzzard]

So it's interesting, because there must be some underlying thing we're doing which is completely rigorous

[Kevin Buzzard]

and hence explicable to Lean

[Mario Carneiro]

Yes, it's equivalent to a whole stack of variables definitions

[Kevin Buzzard]

but if you were to ask any mathematician to state the snake lemma

[Kevin Buzzard]

they would just draw a picture

[Johan Commelin]

We'll end up writing

λ ⟨A, f, B, g, C, h_short_exact⟩, foobar

only to realise that this gives problems later on, because of _match-issues.

[Mario Carneiro]

if we had a bit more lean support (aka a fork) we could make a tactic that introduces a bunch of variables

[Kevin Buzzard]

I figured out the "universal surjection" claim above. Reid's surjection is not universal in the usual sense, because there is more than one choice.

[Mario Carneiro]

choice of sense?

[Kevin Buzzard]

Reid wrote down an explicit free module F (free with basis the elements of M)

[Kevin Buzzard]

and said that projective was equivalent to F -> M splitting

[Kevin Buzzard]

The reason for this is that now if N is a random R-module and we have a surjection N -> M

[Kevin Buzzard]

then because F is free, F -> M lifts to F -> N

[Kevin Buzzard]

-- but not necessarily uniquely

[Kevin Buzzard]

and I can now split N -> M by going from M to F and then down to N

[Mario Carneiro]

in wiki you want to split a surjection in a different module though

[Kevin Buzzard]

oh did I screw up?

[Kevin Buzzard]

Oh, there are two different lifting definitions

[Mario Carneiro]

like your projective module is P and you have a surjection N ->> M and a linear map P -> M

[Kevin Buzzard]

Yeah yeah, there's another one -- "P is projective iff all surjections to P split"

[Kevin Buzzard]

That's what I'm trying to check, not the more general one. They're equivalent you know ;-)

[Mario Carneiro]

okay, so you are halfway there

[Kevin Buzzard]

I know this because they're both the definition of a projective module

[Kevin Buzzard]

I'm proving that if P satisfies Reid's property then every short exact sequence 0 -> M -> N -> P -> 0 splits

[Kevin Buzzard]

and I'm doing it by writing down a morphism of short exact sequences

[Kevin Buzzard]

It's just like alg closure, I'm now a little uncomfortable with this argument even though I've known it for years. Start with P which is Reid-projective. Reid then conjures up a free module which is isomorphic to K + P. Now say N -> P is a surjection. I said "Reid's module is universal, so..." but there is actually no uniqueness in this claim: the projection K + P -> P now lifts (not necessarily uniquely) to a map K + P -> N, because you simply choose a basis for K + P and lift each element randomly and then use universal property of free objects. We now have maps K + P -> N -> P with the composite being the projection, so if P -> K + P is the inclusion then P -> K + P -> N -> P is the identity, hence P -> K + P -> N splits N -> P. Thinking that Reid's object was "universal" leads you to this argument, but the map K + P -> N is not at all canonical.

[Kevin Buzzard]

Anyway, the reason this is somehow one of the more interesting parts of the equivalence from Lean's point of view is that Reid's definition has no universe issues, whereas I am quantifying over all N in the "all surjections split" definition.

[Mario Carneiro]

But this still doesn't answer how to change the codomain of the surjection away from P

[Kevin Buzzard]

no but that's just more standard maths

[Kevin Buzzard]

Which way do you want to see?

[Kevin Buzzard]

I was just interested in one argument which had as a conclusion that you can quantify over all universes

[Kevin Buzzard]

For decades all these definitions were equivalent to me but now I see that some, in my language, have set-theoretic issues

[Kevin Buzzard]

Whereas Reid's most definitely does not

[Mario Carneiro]

Assume it is Reid surjective, show that every surjection M ->> N splits over P -> N

[Kevin Buzzard]

Ok so the more general statement is just the same principle. Reid's definition shows that there's some K such that P + K is free. Now say A->B is surjective and we have P -> B. We extend this to P+ K to B via the projection P + K -> P

[Kevin Buzzard]

Now by surjectivity the map P + K to B lifts to P + K to A

[Mario Carneiro]

is that what surjectivity does?

[Kevin Buzzard]

And we have P -> P + K

[Mario Carneiro]

do we have AC for Mod(R)?

[Kevin Buzzard]

and on a good day with a following wind the diagram will commute

[Kevin Buzzard]

I don't know what AC is

[Mario Carneiro]

oh, I guess we have it: exists_right_inverse_linear_map_of_surjective

[Mario Carneiro]

I mean every surjection splits in Mod(R)

[Johan Commelin]

@Kevin Buzzard AC = axiom of choice :lol:

[Kevin Buzzard]

The diagram commutes. We think of the map P -> B as P -> P + K -> P -> B

[Kevin Buzzard]

and then as P -> P + K -> B

[Kevin Buzzard]

And that's the map we can lift

[Mario Carneiro]

when you say P + K do you mean lc(P)?

[Mario Carneiro]

like is that K needed at all?

[Kevin Buzzard]

Yes

[Mario Carneiro]

so pi1 : P + K -> P is lc.total and P -> P+K is Reid's inverse

[Kevin Buzzard]

Reid's definition is that lc(P) is isomorphic to P + K (K the kernel of the canonical map lc(P) -> P)

[Kevin Buzzard]

Right

[Kevin Buzzard]

And I'm using this basic but fundamental fact that a surjection having an inverse is equivalent to the surjection being a projection

[Mario Carneiro]

being a projection doesn't mean much to me

[Mario Carneiro]

but I understand the first thing, so if it's equivalent I'm happy

[Kevin Buzzard]

Being a projection is a way of extending a map P -> M to a map P + K -> M

[Kevin Buzzard]

You just let it be 0 on K

[Kevin Buzzard]

Wait

[Kevin Buzzard]

It's more than an extension

[Mario Carneiro]

So we split f : A ->> B to f^-1 : B -> A, and the desired map comes from P -> lc(P) -> P -> B -> A

[Kevin Buzzard]

It's the fact that we can factor any map P -> M as P -> P + K -> M

[Kevin Buzzard]

That's the key

[Kevin Buzzard]

f^-1 might not be linear

[Mario Carneiro]

I mean the inverse coming from that theorem

[Mario Carneiro]

every surjection splits

[Kevin Buzzard]

Wait

[Kevin Buzzard]

A random surjection does not split

[Kevin Buzzard]

This is exactly what we're trying to work around

[Mario Carneiro]

oh crap that theorem's in vector spaces

[Johan Commelin]

Those are free

[Johan Commelin]

Sorry, I wasn't paying attention. Should have warned you when you started talking about AC

[Kevin Buzzard]

Every vector space has a basis.

[Mario Carneiro]

okay, so then I'm still stuck on

Now by surjectivity the map P + K to B lifts to P + K to A

[Kevin Buzzard]

That says that every k-module is free, if k is a field

[Kevin Buzzard]

but the integers are not so forgiving.

[Kevin Buzzard]

Z-modules are abelian groups

[Kevin Buzzard]

and Z/2Z is not free

[Mario Carneiro]

yeah, I get that not all modules are free, although I don't see immediately what this has to do with inverting surjections, but I can believe it

[Kevin Buzzard]

and Z/4Z -> Z/2Z is a surjection which does not split, because Z/4Z is not isomorphic to Z/2Z + Z/2Z

[Kevin Buzzard]

The key definition is that a surjection M -> N splits if there's a linear injection N -> M which is a one-sided inverse

[Kevin Buzzard]

The lemma is that a surjection splits iff it's isomorphic to a projection

[Johan Commelin]

yeah, I get that not all modules are free, although I don't see immediately what this has to do with inverting surjections, but I can believe it

Free => projective => surjections split

[Kevin Buzzard]

If M->N has kernel K and M -> N splits, then choose a splitting i: N -> M. We now get a map N + K -> M and this is an isomorphism

[Kevin Buzzard]

The theorem is that if P is projective then all surjections onto P split

[Kevin Buzzard]

Or maybe it's the definition, who knows

[Kevin Buzzard]

okay, so then I'm still stuck on

Now by surjectivity the map P + K to B lifts to P + K to A

This is where we use that P + K is free. We construct a completely non-canonical lift of P+K->B to P+K->A

[Mario Carneiro]

okay, so exists_left_inverse_linear_map_of_injective needs generalizing

[Kevin Buzzard]

by saying "pick a basis of P+K, because it's free. Choose a random basis element. It gets mapped to an element of A which we know lifts (via a completely random non-linear set-theoretic splitting A -> B) to an element of B. Send the basis element here. Extend by linearity"

[Kevin Buzzard]

The "extend by linearity" line is exactly where you assume that something is free. If I have a random module M and a random generating subset, I can't be defining maps M -> N by saying "send the generators to random things and extend linearly" because the generators might satisfy random relations which won't work in N

[Mario Carneiro]

the proof constructs a basis C extending the image of a basis of the domain basis

[Kevin Buzzard]

I am using the obvious basis of lc(P) in my head

[Mario Carneiro]

both sides need vector space assumption, but the basis on the domain follows if the domain is free, and the basis on the target comes from... where?

[Kevin Buzzard]

I think that's the only basis in the argument

[Kevin Buzzard]

You have lost me

[Mario Carneiro]

the second basis is used for the "extend by linearity" part

[Mario Carneiro]

each basis element of lc(P) goes somewhere, so you take these elements and throw more in to make a basis of B

[Kevin Buzzard]

exists_left_inverse_linear_map_of_injective generalises to the statement that if M is a random module and P is a projective module then every injection M -> P has a one-sided inverse.

[Mario Carneiro]

oh, oops wrong proof

[Mario Carneiro]

exists_right_inverse_linear_map_of_surjective

[Mario Carneiro]

ah, this one only needs one basis

[Mario Carneiro]

oh, it's actually a zero cost generalization, there is no need to assume beta is a vector space , except that alpha is a field anyway in the theorem statement

[Kevin Buzzard]

exists_right_inverse_linear_map_of_surjective generalizes to the assertion that if P is a projective module then every surjection P -> M has a right inverse

[Kevin Buzzard]

Every module over a field is a vector space, hence has a basis, hence is free, hence is projective

[Kevin Buzzard]

Over a general ring you get two new phenomena which stop things from being free.

[Kevin Buzzard]

The first is that modules over the ring can "wrap around themselves" -- e.g. Z/10Z is a module over Z but {1} isn't a basis because it's linearly dependent -- 10 * 1 = 0

[Kevin Buzzard]

The second is that you can have abelian groups like Q which have no torsion as Z-modules but which aren't free anyway, because any two elements are linearly dependent

[Kevin Buzzard]

Neither Q nor Z/10Z is free over Z

[Mario Carneiro]

right

[Kevin Buzzard]

But Q is flat over Z :-)

[Kevin Buzzard]

but that's probably a story for another day

[Mario Carneiro]

okay, I am convinced that projective modules are interesting enough to have a few theorems in mathlib

[Kevin Buzzard]

A nice example of a projective module that isn't free is a non-zero ideal in the integers of a number field.

[Mario Carneiro]

not Z?

[Kevin Buzzard]

If R = Z[sqrt(-5)] then numbers do not factor uniquely into primes

[Mario Carneiro]

oh right Z is free

[Kevin Buzzard]

All ideals of Z are principal, and a non-zero ideal is hence free -- the generator is a basis

[Kevin Buzzard]

But for R you have 2*3=(1+sqrt(-5))*(1-sqrt(-5))

[Kevin Buzzard]

and all of these are primes

[Mario Carneiro]

aside: How do you check stuff like that?

[Kevin Buzzard]

However uniqueness of factorization is restored if you have the amazing insight to invent "ideal numbers", generalisations of numbers which do have unique factorization, and which historically I believe is the reason that ideals are called ideal.

[Kevin Buzzard]

The incredibly tedious proof that 2,3, etc are all primes is "embed everything in the complexes and observe that if r in R is non-zero then |r|>=1"

[Kevin Buzzard]

and so an algorithm for checking to see if x is prime is to consider the finitely many elements of R whose norm is <= |x| and see if any of them go into x

[Mario Carneiro]

Don't some primes factor in number fields like that?

[Kevin Buzzard]

Normal prime numbers can factor, yes

[Mario Carneiro]

oh, did you mean something other than 2,3, etc

[Kevin Buzzard]

Oh wait, I am using incorrect notation.

[Kevin Buzzard]

I should say that if R=Z[sqrt(-5)] then elements of R do not in general factor uniquely into irreducibles

[Kevin Buzzard]

And the tedious proof I gave you above is that 2,3,1+sqrt(-5) and 1-sqrt(-5) are all irreducible

[Mario Carneiro]

aha, not the same because Z{sqrt(-5)] is not a UFD, yes?

[Kevin Buzzard]

Yeah.

[Kevin Buzzard]

For Z[sqrt(-5)] you can use the embedding into C as an algorithm for checking for irreducibility.

[Kevin Buzzard]

(C the complexes)

[Mario Carneiro]

When you talk about the norm, you mean the norm on C, not that funny number field norm?

[Mario Carneiro]

a^2 + 5b^2 or something

[Kevin Buzzard]

Well using the funny number field norm is a bit saner for this example

[Kevin Buzzard]

because it's nat-valued and is the square of the complex norm

[Kevin Buzzard]

so for this example the stories are the same.

[Mario Carneiro]

I guess as long as you have Z[sqrt(-n)] the norm is positive definite so this list is finite

[Mario Carneiro]

but for Z[sqrt(n)] it's some kind of pell's equation

[Kevin Buzzard]

So some German mathematician 150 years ago had the idea that 2 and 1+sqrt(-5) seemed to be coprime in the sense that they couldn't find anything dividing both of them

[Mario Carneiro]

dedekind, I presume?

[Kevin Buzzard]

For Z[sqrt(n)] you'd be better off using the funny number field norm, but now there are issues because there are infinitely many elements of norm <= B

[Kevin Buzzard]

so you need tricks to cut your search space down

[Kevin Buzzard]

the first of which is that you need a good way to solve Pell's equation

[Mario Carneiro]

is there a reason to believe that the large ones don't matter?

[Kevin Buzzard]

So dammit 2 and 1+sqrt(-5) seem to be distinct "primes" i.e. irreducible, but we can't solve lambda * 2 + mu * 1+sqrt(-5) = 1

[Kevin Buzzard]

even though they're "coprime"

[Mario Carneiro]

lol sorry for the distractions

[Kevin Buzzard]

and then they were left with this big pile of elements of the form lambda * 2 + mu * (1+sqrt(-5))

[Kevin Buzzard]

and they left them under a microscope and there was some chemical reaction or something

[Kevin Buzzard]

and when they came back they realised they'd invented ideals

[Kevin Buzzard]

and that instead of trying to find 1 in this set, they should just let this entire set be the model for the highest common factor

[Kevin Buzzard]

and then it turned out that they could multiply two sets of this form

[Kevin Buzzard]

and after the dust had cleared, uniqueness of factorization had been restored!

[Mario Carneiro]

what does that statement mean here?

[Kevin Buzzard]

So if I=(2,1+sqrt(-5)) and J = (3,1+sqrt(-5)) then I and J are prime ideals

[Kevin Buzzard]

and 2=I^2

[Kevin Buzzard]

and if K = (3,1-sqrt(-5)) then K is prime too and 3 = J*K

[Kevin Buzzard]

and (1+sqrt(-5)) is I*K

[Kevin Buzzard]

and the non-unique 2*3=(1+sqrt(-5))(1-sqrt(-5)) now can be written as (I^2)*(J*K)=(I*J)*(I*K)

[Mario Carneiro]

interesting

[Kevin Buzzard]

which becomes the unique (6)=I^2*J*K

[Kevin Buzzard]

so these sets were behaving better than numbers, so they called them ideal numbers

[Mario Carneiro]

so why isn't this the even more fundamental theorem of arithmetic?

[Kevin Buzzard]

and the principal ideal (6) is factoring uniquely into prime ideals

[Kevin Buzzard]

The correct theorem is that for a Dedekind domain, every non-zero ideal is uniquely the product of prime ideals.

[Kevin Buzzard]

The proof is that this is true by one of the definitions of a Dedekind domain

[Mario Carneiro]

lol figures

[Kevin Buzzard]

Another definition is that it's an integrally closed integral domain for which all non-zero prime ideals are maximal. We have all of those notions in Lean.

[Kevin Buzzard]

Assuming Kenny PR'ed integrally closed and someone accepted it, which might not be true

[Kevin Buzzard]

Or maybe Johan PR'ed it

[Kevin Buzzard]

I know they were both thinking about it but it was when I was mired in teaching hell

[Mario Carneiro]

We don't have this factorization statement in mathlib, right?

[Kevin Buzzard]

No, but I did consider setting it as an undergraduate project

[Mario Carneiro]

or dedekind domains at all

[Kevin Buzzard]

Right.

[Mario Carneiro]

but I guess you can also unfold the statement PID => DD using this definition

[Kevin Buzzard]

The reason that such a theorem would be important for mathlib, is that the ring of integers of a number field is by definition an integral closure

[Kevin Buzzard]

and it is not hard to go from that to checking that the ring of integers of a number field is a Dedekind domain

[Mario Carneiro]

oh wait PID => DD is trivial isn't it

[Kevin Buzzard]

However there are other examples, for example $\mathbb{C}[X,Y]/(Y^2-X^3-1)$

[Kevin Buzzard]

Well, it depends on which definition of DD you use I guess

[Kevin Buzzard]

You can make everything trivial if you choose your definitions carefully

[Kevin Buzzard]

PID -> UFD and UFD's are integrally closed

[Mario Carneiro]

that's my hope

[Kevin Buzzard]

I think I might have missed out a Noetherian hypothesis in one of my definitions of Dedekind domain; I don't have Cassels-Froehlich to hand

[Kevin Buzzard]

But again we have it in mathlib

[Kenny Lau]

Assuming Kenny PR'ed integrally closed and someone accepted it, which might not be true

it's still being gradually PR'ed ~ the current one is #679 ~

[Kevin Buzzard]

Maybe I need Noetherian, integrally closed, and all non-zero primes are maximal

[Kevin Buzzard]

(and a domain)

[Kevin Buzzard]

But if you use the definition that all non-zero ideals factor uniquely into prime ideals then PID -> DD should be very easy. I'm a mathematician, I have no idea what "the" definition of a DD is. I believe that in Cassels-Froehlich it's exactly one of these proposition-definitions.

[Kevin Buzzard]

The two definitions I've suggested above and I think there's a third one too.

[Kevin Buzzard]

The reason I mention these things it that if R = Z[sqrt(-5)] then the principal ideals are the free submodules of R, but every ideal is projective.

[Kevin Buzzard]

So it's a good concrete example of a projective non-free module.

[Mario Carneiro]

is this easy to see concretely with Reid's definition?

[Kevin Buzzard]

If I=(2,1+sqrt(-5)) as above, then $I^2=2$

[Kevin Buzzard]

and this implies that $I\oplus I$ is free

[Kevin Buzzard]

I have no idea at all how to see it from Reid's definition

[Kevin Buzzard]

But I bet that, after a struggle, I could come up with a basis for $I\oplus I$, of size 2

[Mario Carneiro]

oh you are using the P + K free version

[Mario Carneiro]

size 2? Not 1?

[Kevin Buzzard]

Yeah, projective modules have dimension even though they don't have bases

[Kevin Buzzard]

$I$ is "locally free of rank 1"

[Mario Carneiro]

I mean (2) is principal so it should have dimension 1

[Kevin Buzzard]

Yes, but $I\oplus I$ is the abstract direct sum

[Mario Carneiro]

oh I+I not I*I

[Kevin Buzzard]

it's not $I^2$ which is an ideal-theoretic multiplication

[Mario Carneiro]

okay so why does I^2 = 2 imply I+I free?

[Kevin Buzzard]

That's not obvious

[Kevin Buzzard]

An unhelpful answer is that this is how the picard group of a Dedekind domain works

[Mario Carneiro]

Are you asserting it from experience or from a high powered theorem?

[Mario Carneiro]

or both?

[Kevin Buzzard]

both

[Kevin Buzzard]

I would rather argue that $I$ is projective because by definition a module is projective iff it is locally free

[Kevin Buzzard]

and $I$ is locally free because the localisations of a Dedekind domain are 1-dimensional regular local rings and over such a ring all projective modules are free

[Kevin Buzzard]

I think that argument uses less machinery but it's still hopeless

[Kevin Buzzard]

I'm sure there will be an elementary argument

[Mario Carneiro]

wow you have high powered theorems up all your sleeves

[Kevin Buzzard]

meaning that I've forgotten all the low-level proofs :-/

[Mario Carneiro]

It's not necessarily a bad thing, I'd rather have the high powered theorem than an ad hoc argument

[Kevin Buzzard]

Geometrically, what we are doing is analysing 1-dimensional rings. This is not dimension in the sense of number of basis elements, this is a different use of the word

[Kevin Buzzard]

If R is a Dedekind domain then Spec(R) is a smooth curve

[Kevin Buzzard]

and nowadays I think about algebra using R as being geometric statements about this curve

[Kevin Buzzard]

In fact I should say that in some sense this is a bad thing about the current status of mathlib. this Spec trick absolutely relies on the fact that R is commutative.

[Kevin Buzzard]

So all of the theory of modules which we are building up all has these inbuilt assumptions that R is commutative because it's the only case I've ever cared about, and I know how to steer it really well, and I point people like Kenny to books about commutative rings

[Mario Carneiro]

lol I'm pretty sure this is your fault

[Kevin Buzzard]

But some of the more basic stuff, like all the foundational work I was looking at yesterday in mathlib about how modules over a commutative ring form a lattice etc

[Mario Carneiro]

I would have left comm out everywhere and you would have called me crazy

[Kevin Buzzard]

all of that works for modules over a non-commutative ring

[Mario Carneiro]

in metamath vector spaces are over a division ring

[Mario Carneiro]

literally the whole theory goes through

[Kevin Buzzard]

It would not surprise me if you could replace comm_ring by ring in some of those mathlib files and they would still compile

[Kevin Buzzard]

It's just that all us algebraic geometers know that there is no interesting example of a ring which isn't commutative :-)

[Mario Carneiro]

until you do

[Kevin Buzzard]

and one day an algebraist will stumble over this work and will be like "WTF have you idiots done??"

[Kevin Buzzard]

I should get to work. Let me finish with this. The class group of a Dedekind domain is the set of isomorphism classes of non-zero ideals!

[Mario Carneiro]

is that a group or is the word just for decoration?

[Kevin Buzzard]

Miraculously, this set is a group, because (and this needs checking) if I and J are isomorphic, then so are I*K and J*K

[Kevin Buzzard]

and this is because two ideals $I$ and $J$ are isomorphic iff there is an element $\lambda$ of the field of fractions of the Dedekind domain such that $\lambda I=J$

[Mario Carneiro]

isomorphism of ideals means an automorphism of R that sends I to J?

[Kevin Buzzard]

It means abstractly isomorphic as modules

[Kevin Buzzard]

but a much better definition of the equivalence relation would be the one using the field of fractions

[Kevin Buzzard]

For example all principal ideals are related (let me say "related" not "isomorphic") because to relate $(a)$ to $(b)$ you just multiply by $b/a$

[Kevin Buzzard]

This is an equivalence relation. The equivalence class of $R=(1)$ is all the principal ideals

[Mario Carneiro]

aha, so the field of fractions is a group action on the ideals?

[Mario Carneiro]

nonzero elements of the field, I assume

[Kevin Buzzard]

The best way to think about it is to define a fractional ideal to be a...let me set up notation

[Kevin Buzzard]

$R$ a Dedekind domain, $K$ its field of fractions

[Kevin Buzzard]

e.g. $R=\mathbb{Z}$ and $K=\mathbb{Q}$

[Kevin Buzzard]

or R=Z[sqrt(-5)] and K=Q(sqrt(-5))

[Kevin Buzzard]

A fractional ideal is an "ideal with denominator"

[Kevin Buzzard]

i.e. a subset $J$ of $K$ such that there exists some non-zero $r\in R$ such that $rJ$ is a regular non-zero ideal

[Kevin Buzzard]

For example $\frac{3}{7}\mathbb{Z}$ is a fractional ideal of $\mathbb{Z}$

[Mario Carneiro]

btw we definitely need a predicate version of "field of fractions", so you can say that

[Kevin Buzzard]

$\{\frac{3}{7}n\,:\,n\in\mathbb{Z}\,\}$

[Kevin Buzzard]

You can multiply fractional ideals together. A fractional ideal is an R-module, in fact it's a sub-R-module of K

[Mario Carneiro]

Isn't that the same as just saying $I/r$ for some nonzero $r\in R$?

[Kevin Buzzard]

There's an action of $K^\times$ on the fractional ideals. Yes, it's the same

[Kevin Buzzard]

A fractional ideal is principal if it's of the form $\kappa R$ for some $\kappa\in K^\times$

[Kevin Buzzard]

($K^\times$ is the group of non-zero element of $K$)

[Kevin Buzzard]

The group acts on the fractional ideals, one orbit is the principal fractional ideals, and if unique factorization fails in $R$ then there are other orbits

[Kevin Buzzard]

Say two ideals are equivalent if they're in the same orbit. Then the equivalence classes form a group, the so-called ideal class group.

[Johan Commelin]

The group acts on the fractional ideals, one orbit is the principal fractional ideals, and if unique factorization fails in $R$ then there are other orbits

iff

[Kevin Buzzard]

A mathematician would say that the ideal class group "measures" the failure of uniqueness of factorization

[Mario Carneiro]

Is the fact about I*K ~ J*K only valid in DDs?

[Kevin Buzzard]

i.e. the ideal class group of $R$ is the trivial group iff $R$ is a PID iff $R$ is a UFD

[Kevin Buzzard]

I have never seen the concept of fractional ideal used outside the theory of DD's but it would not surprise me at all if parts of the general theory could be set up for general ID's

[Johan Commelin]

Well, you have ClGr(R) = Pic(Spec(R))

[Johan Commelin]

And you have Pic(X) for any scheme X

[Kevin Buzzard]

In a DD it's true that two fractional ideals are abstractly isomorphic as R-modules if and only if they are in the same orbit under $K^\times$

[Kevin Buzzard]

So in algebraic geometry there is this vast generalisation of class groups, where you consider isomorphism classes of rank 1 projective modules

[Johan Commelin]

So in some sense there is a very big generalisation. It uses "fractional ideal" = "locally free of rank 1".

[Kevin Buzzard]

but I've never thought about how it translates into fractional ideals

[Johan Commelin]

It's certainly not defeq (-;

[Kevin Buzzard]

So for R=Z the class group is trivial because all fractional ideals are principal

[Kevin Buzzard]

but for R=Z[sqrt(-5)] the class group turns out to have size 2

[Johan Commelin]

Now comes a high-powered theorem... drum roll...

[Kevin Buzzard]

lemme say one moer thing first

[Kevin Buzzard]

and because of the group structure you can conclude the highly non-obvious fact that if $I$ is any random ideal of Z[sqrt(-5)] then $I^2$ is a principal ideal

[Kevin Buzzard]

I don't think that this is at all obvious

[Kevin Buzzard]

Anyway, class groups are cool, they're random abelian groups attached to Dedekind domains

[Mario Carneiro]

I get the sense that calculating class groups for Z[sqrt(-n)] is one of those things mathematicians like to do

[Kevin Buzzard]

and the class group of the ring of integers of a number field is always finite :-)

[Kevin Buzzard]

Yes, mathematicians get very excited about class groups of Z[sqrt(-n)]

[Mario Carneiro]

any chance of a decision procedure?

[Johan Commelin]

Yes, there are algorithms for this.

[Kevin Buzzard]

If n is something like 27 then strictly speaking this is not a Dedekind domain because it's not the full ring of integers, but using this alg geom generalization you have some variant of the class group anyway

[Kevin Buzzard]

There have been really deep theorems proved about these class groups, for example the class group of the ring of integers of $\mathbb{Q}((-163)^{1/2})$ is trivial

[Kevin Buzzard]

but that's the last one

[Kevin Buzzard]

For $n<-163$ squarefree, the class group is never trivial

[Mario Carneiro]

I recall hearing about how Z[sqrt(-163)] is the last UFD

[Kevin Buzzard]

Right

[Kevin Buzzard]

An even stronger statement is true -- the size of the class group tends to infinity as $n$ tends to $-\infty$

[Kevin Buzzard]

so the failure of unique factorization gets worse and worse

[Kevin Buzzard]

This is pretty much the culmination (the statement, not the proof) of the algebraic number theory course at Imperial.

[Kevin Buzzard]

Chris and others proved most of the main theorems of the basic number theory course last summer.

[Mario Carneiro]

so, worth it for mathlib?

[Kevin Buzzard]

But we have not begun to scratch the surface of the algebraic number theory course.

[Mario Carneiro]

it's sometimes hard to tell how much is playing with examples and how much is big theorems

[Kevin Buzzard]

Who knows what's worth it for mathlib. But one definition I've been using is "if it's in a standard undergraduate curriculum, there is a case for it being in mathlib"

[Mario Carneiro]

In a perfect world, I would like to have all the big theorems and have decision procedures for all the examples

[Kevin Buzzard]

That's why I made the issue about Cauchy's theorem, to remind me, whenever I think "yay we have all of this 3rd year course, and most of that 3rd year course, and we're now ready to start on that 3rd year course"

[Kevin Buzzard]

I should then remember that there is a big 2nd year course that we are not even ready to start formalising

[Mario Carneiro]

I'm 100% with you on Cauchy's theorem, that's been a blocker for me forever

[Kevin Buzzard]

i.e. we can't even formalise the statement of the main theorem of that course

[Mario Carneiro]

I never managed it in metamath, got stuck debating how general to make it

[Kevin Buzzard]

We have enough comm alg in Lean now to formalise all the statements of the theorems in the algebraic number theory course, and in the correct generality too.

[Kevin Buzzard]

In the course at Imperial we only prove that all non-zero ideals are uniquely the product of prime ideals for integers of number fields

[Kevin Buzzard]

However the proofs all extend easily to Dedekind domains

[Kevin Buzzard]

The class group of $\mathbb{C}[X,Y]/(Y^2-X^3-1)$ is uncountably infinite however :-)

[Kevin Buzzard]

so the proof that the class group of the integers of a number field is finite is of arithmetic nature, and needs number fields.

[Kevin Buzzard]

All non-zero primes are maximal, but finiteness of class group is implied by the further finiteness assumption that if you quotient out by one of these maximal ideals, the field you get is a finite field.

[Kevin Buzzard]

There are algorithms for computing class groups, but it would not surprise me if none of them ever terminated in Lean.

[Kevin Buzzard]

Although one has to be optimistic that we could get as far as Q(sqrt(-5))

[Kevin Buzzard]

rofl we might need a better approximation for $\pi$ first :-)

[Kevin Buzzard]

The proofs that the algorithms are correct use embeddings into the complexes, and logarithms

[Kevin Buzzard]

oh shit and some integration

[Kevin Buzzard]

hmm

[Kevin Buzzard]

maybe we'd better make them meta algorithms

[Kevin Buzzard]

I know pi to 100 decimal places, I'd better start working on my decimal expansions PR

[Patrick Massot]

okay, I am convinced that projective modules are interesting enough to have a few theorems in mathlib

Epic quote.

[Kevin Buzzard]

yeah it made me snigger too. Apparently line bundles are an important feature in geometry :-)

[Kevin Buzzard]

Vector bundles even!

[Kevin Buzzard]

Now if only we had manifolds to put them on :P

[Reid Barton]

Should we prove Swan's theorem?

[Kevin Buzzard]

I think we might be a way off that. But sure, let's prove all the theorems.

[Kevin Buzzard]

I feel that maybe in the distant future when we have some cohomology we might be able to get Serre's version. To get the manifold version it might be best to have manifolds first.

[Reid Barton]

I was thinking of the version for compact Hausdorff spaces

[Kevin Buzzard]

Oh I'm just looking at Wikipedia, I'm not sure I knew about that version. This will convince Mario that projective modules are useful because it shows they're equivalent to something he's never heard of, right?

[Kevin Buzzard]

Is the proof straightforward?

[Kevin Buzzard]

"projective modules over commutative rings are like vector bundles on compact spaces".

[Reid Barton]

... kind of? I only took a quick look but it seems like the main facts it uses are things like the existence of partitions of unity and projective iff locally free

[Kevin Buzzard]

Oh, we only have Reid-projective at the minute :-)

[Reid Barton]

I'm not sure we need more big projects but this would tie together the active parts of mathlib in a neat way

[Patrick Massot]

I have a better big project: do this topology reorganization and file splitting :wink:

[Kevin Buzzard]

I thought topology got reorganised?

[Patrick Massot]

only the very first step of the reorganization

[Patrick Massot]

Then I drafted a less trivial step, but everybody was busy, and now many things have been added so we need to start over

[Patrick Massot]

This kind of reorganization has to be very quick from PR to merge