## Stream: maths

### Topic: free module

#### Reid Barton (Feb 13 2019 at 22:56):

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 (Feb 13 2019 at 22:57):

Unfortunately there \b needs to be a module or something

oh, I see...

#### Kenny Lau (Feb 13 2019 at 22:57):

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

#### Reid Barton (Feb 13 2019 at 22:57):

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

#### Reid Barton (Feb 13 2019 at 22:58):

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

then very good

#### Reid Barton (Feb 13 2019 at 22:58):

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

#### Reid Barton (Feb 13 2019 at 22:58):

because it's finsupp.to_module

#### Kenny Lau (Feb 13 2019 at 22:58):

nothing uses the module structure on \b

#### Kenny Lau (Feb 13 2019 at 22:59):

it's just lc that requires it

#### Reid Barton (Feb 13 2019 at 23:00):

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

#### Reid Barton (Feb 13 2019 at 23:09):

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

#### Kenny Lau (Feb 13 2019 at 23:11):

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

#### Reid Barton (Feb 13 2019 at 23:11):

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

#### Reid Barton (Feb 13 2019 at 23:42):

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 (Feb 13 2019 at 23:46):

can you use smul_right for as inv_fun?

oh, nice

edited

#### Reid Barton (Feb 14 2019 at 00:03):

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 (Feb 14 2019 at 00:03):

is this definition too weird

#### Johan Commelin (Feb 14 2019 at 05:53):

I don't think mathematicians will recognise it

#### Johan Commelin (Feb 14 2019 at 05:53):

I think lc is somewhat unintuitive to use there

#### Reid Barton (Feb 14 2019 at 05:54):

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

#### Reid Barton (Feb 14 2019 at 05:56):

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

#### Reid Barton (Feb 14 2019 at 05:58):

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

#### Reid Barton (Feb 14 2019 at 06:00):

maybe I should give in and use category theory

#### Johan Commelin (Feb 14 2019 at 06:00):

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 (Feb 14 2019 at 06:01):

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

#### Mario Carneiro (Feb 14 2019 at 06:12):

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

#### Mario Carneiro (Feb 14 2019 at 06:18):

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

#### Mario Carneiro (Feb 14 2019 at 06:19):

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 (Feb 14 2019 at 07:56):

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 (Feb 14 2019 at 07:57):

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 (Feb 14 2019 at 07:59):

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 (Feb 14 2019 at 08:02):

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 (Feb 14 2019 at 08:03):

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 (Feb 14 2019 at 08:04):

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

#### Mario Carneiro (Feb 14 2019 at 08:04):

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

#### Mario Carneiro (Feb 14 2019 at 08:05):

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

#### Kevin Buzzard (Feb 14 2019 at 08:05):

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

#### Kevin Buzzard (Feb 14 2019 at 08:05):

I was told "locally free" was the definition once

#### Kevin Buzzard (Feb 14 2019 at 08:06):

Ie all localisations were free modules

#### Kevin Buzzard (Feb 14 2019 at 08:06):

Neither of these involve quantifying over all modules

#### Mario Carneiro (Feb 14 2019 at 08:07):

direct summand of free quantifies over all modules

#### Mario Carneiro (Feb 14 2019 at 08:07):

dunno what locally free means

#### Kevin Buzzard (Feb 14 2019 at 08:07):

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

#### Johan Commelin (Feb 14 2019 at 08:07):

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

#### Mario Carneiro (Feb 14 2019 at 08:08):

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 (Feb 14 2019 at 08:08):

In ZFC we only use one universe

#### Mario Carneiro (Feb 14 2019 at 08:08):

yeah, then it's an impredicative definition

#### Kevin Buzzard (Feb 14 2019 at 08:08):

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

#### Mario Carneiro (Feb 14 2019 at 08:09):

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

#### Kevin Buzzard (Feb 14 2019 at 08:09):

That all surjections in M's universe split

Hmm

#### Kevin Buzzard (Feb 14 2019 at 08:10):

Or is that R's universe?

#### Mario Carneiro (Feb 14 2019 at 08:10):

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

#### Mario Carneiro (Feb 14 2019 at 08:11):

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

#### Kevin Buzzard (Feb 14 2019 at 08:11):

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 (Feb 14 2019 at 08:11):

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

#### Kevin Buzzard (Feb 14 2019 at 08:11):

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

#### Mario Carneiro (Feb 14 2019 at 08:12):

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

#### Kevin Buzzard (Feb 14 2019 at 08:12):

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

#### Mario Carneiro (Feb 14 2019 at 08:12):

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

It can happen

R + S is a ring

#### Kevin Buzzard (Feb 14 2019 at 08:13):

Making S a projective R module

#### Kevin Buzzard (Feb 14 2019 at 08:13):

So take R and S rings in different universes

#### Kevin Buzzard (Feb 14 2019 at 08:14):

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

clearly

#### Kevin Buzzard (Feb 14 2019 at 08:14):

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

#### Mario Carneiro (Feb 14 2019 at 08:15):

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

#### Kevin Buzzard (Feb 14 2019 at 08:15):

I'm not qualified to answer that

#### Mario Carneiro (Feb 14 2019 at 08:15):

The commutative diagram suggests non-uniqueness, so maybe not

#### Mario Carneiro (Feb 14 2019 at 08:15):

is it "canonical"?

No

#### Kevin Buzzard (Feb 14 2019 at 08:16):

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

#### Mario Carneiro (Feb 14 2019 at 08:17):

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

#### Mario Carneiro (Feb 14 2019 at 08:18):

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

#### Kevin Buzzard (Feb 14 2019 at 08:18):

All surjections split is one definition of a projective module

#### Kevin Buzzard (Feb 14 2019 at 08:19):

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

#### Kevin Buzzard (Feb 14 2019 at 08:19):

If that splits, they all do

#### Kevin Buzzard (Feb 14 2019 at 08:21):

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

#### Mario Carneiro (Feb 14 2019 at 08:22):

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 (Feb 14 2019 at 08:23):

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

#### Kevin Buzzard (Feb 14 2019 at 08:24):

I can't work out the details :-/

#### Kevin Buzzard (Feb 14 2019 at 08:25):

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

#### Kevin Buzzard (Feb 14 2019 at 08:27):

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 (Feb 14 2019 at 08:28):

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 (Feb 14 2019 at 08:29):

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 (Feb 14 2019 at 08:29):

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

#### Kevin Buzzard (Feb 14 2019 at 08:30):

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

#### Kevin Buzzard (Feb 14 2019 at 08:31):

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 (Feb 14 2019 at 08:31):

May we please have short exact sequences in Lean?

#### Johan Commelin (Feb 14 2019 at 08:31):

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

#### Kevin Buzzard (Feb 14 2019 at 08:31):

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 (Feb 14 2019 at 08:32):

(a) and (b) are equivalent statements

#### Johan Commelin (Feb 14 2019 at 08:32):

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 (Feb 14 2019 at 08:33):

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

#### Johan Commelin (Feb 14 2019 at 08:33):

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

#### Kevin Buzzard (Feb 14 2019 at 08:33):

Why is that ugly?

#### Kevin Buzzard (Feb 14 2019 at 08:33):

I agree that it's one approach

#### Mario Carneiro (Feb 14 2019 at 08:33):

I think drawing a picture every time is tiresome

#### Kevin Buzzard (Feb 14 2019 at 08:33):

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

#### Kevin Buzzard (Feb 14 2019 at 08:34):

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

#### Johan Commelin (Feb 14 2019 at 08:34):

"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 (Feb 14 2019 at 08:34):

like I said, drawing a picture

#### Kevin Buzzard (Feb 14 2019 at 08:34):

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

#### Kevin Buzzard (Feb 14 2019 at 08:34):

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

#### Kevin Buzzard (Feb 14 2019 at 08:35):

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

#### Mario Carneiro (Feb 14 2019 at 08:36):

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


#### Johan Commelin (Feb 14 2019 at 08:38):

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 (Feb 14 2019 at 08:38):

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

#### Johan Commelin (Feb 14 2019 at 08:39):

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 (Feb 14 2019 at 08:39):

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

#### Johan Commelin (Feb 14 2019 at 08:40):

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

#### Mario Carneiro (Feb 14 2019 at 08:40):

this is a ridiculous notation

#### Kevin Buzzard (Feb 14 2019 at 08:41):

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

#### Mario Carneiro (Feb 14 2019 at 08:41):

the variables notation won't work

#### Mario Carneiro (Feb 14 2019 at 08:41):

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

#### Kevin Buzzard (Feb 14 2019 at 08:41):

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

#### Mario Carneiro (Feb 14 2019 at 08:41):

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

#### Kevin Buzzard (Feb 14 2019 at 08:42):

Mathematicians reason by drawing diagrams sometimes.

#### Kevin Buzzard (Feb 14 2019 at 08:42):

This is hard to do in Lean.

#### Mario Carneiro (Feb 14 2019 at 08:42):

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

#### Kevin Buzzard (Feb 14 2019 at 08:42):

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

#### Kevin Buzzard (Feb 14 2019 at 08:42):

and hence explicable to Lean

#### Mario Carneiro (Feb 14 2019 at 08:43):

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

#### Kevin Buzzard (Feb 14 2019 at 08:43):

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

#### Kevin Buzzard (Feb 14 2019 at 08:43):

they would just draw a picture

#### Johan Commelin (Feb 14 2019 at 08:43):

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 (Feb 14 2019 at 08:43):

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

#### Kevin Buzzard (Feb 14 2019 at 08:44):

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.

choice of sense?

#### Kevin Buzzard (Feb 14 2019 at 08:45):

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

#### Kevin Buzzard (Feb 14 2019 at 08:45):

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

#### Kevin Buzzard (Feb 14 2019 at 08:45):

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

#### Kevin Buzzard (Feb 14 2019 at 08:45):

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

#### Kevin Buzzard (Feb 14 2019 at 08:46):

-- but not necessarily uniquely

#### Kevin Buzzard (Feb 14 2019 at 08:46):

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

#### Mario Carneiro (Feb 14 2019 at 08:47):

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

#### Kevin Buzzard (Feb 14 2019 at 08:47):

oh did I screw up?

#### Kevin Buzzard (Feb 14 2019 at 08:47):

Oh, there are two different lifting definitions

#### Mario Carneiro (Feb 14 2019 at 08:47):

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

#### Kevin Buzzard (Feb 14 2019 at 08:48):

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

#### Kevin Buzzard (Feb 14 2019 at 08:48):

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

#### Mario Carneiro (Feb 14 2019 at 08:48):

okay, so you are halfway there

#### Kevin Buzzard (Feb 14 2019 at 08:48):

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

#### Kevin Buzzard (Feb 14 2019 at 08:49):

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

#### Kevin Buzzard (Feb 14 2019 at 08:50):

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

#### Kevin Buzzard (Feb 14 2019 at 08:58):

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 (Feb 14 2019 at 09:01):

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 (Feb 14 2019 at 09:06):

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

#### Kevin Buzzard (Feb 14 2019 at 09:06):

no but that's just more standard maths

#### Kevin Buzzard (Feb 14 2019 at 09:08):

Which way do you want to see?

#### Kevin Buzzard (Feb 14 2019 at 09:08):

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

#### Kevin Buzzard (Feb 14 2019 at 09:10):

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

#### Kevin Buzzard (Feb 14 2019 at 09:10):

Whereas Reid's most definitely does not

#### Mario Carneiro (Feb 14 2019 at 09:13):

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

#### Kevin Buzzard (Feb 14 2019 at 09:13):

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 (Feb 14 2019 at 09:14):

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

#### Mario Carneiro (Feb 14 2019 at 09:14):

is that what surjectivity does?

#### Kevin Buzzard (Feb 14 2019 at 09:14):

And we have P -> P + K

#### Mario Carneiro (Feb 14 2019 at 09:14):

do we have AC for Mod(R)?

#### Kevin Buzzard (Feb 14 2019 at 09:14):

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

#### Kevin Buzzard (Feb 14 2019 at 09:15):

I don't know what AC is

#### Mario Carneiro (Feb 14 2019 at 09:15):

oh, I guess we have it: exists_right_inverse_linear_map_of_surjective

#### Mario Carneiro (Feb 14 2019 at 09:15):

I mean every surjection splits in Mod(R)

#### Johan Commelin (Feb 14 2019 at 09:16):

@Kevin Buzzard AC = axiom of choice :lol:

#### Kevin Buzzard (Feb 14 2019 at 09:16):

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

#### Kevin Buzzard (Feb 14 2019 at 09:17):

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

#### Kevin Buzzard (Feb 14 2019 at 09:17):

And that's the map we can lift

#### Mario Carneiro (Feb 14 2019 at 09:17):

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

#### Mario Carneiro (Feb 14 2019 at 09:17):

like is that K needed at all?

Yes

#### Mario Carneiro (Feb 14 2019 at 09:18):

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

#### Kevin Buzzard (Feb 14 2019 at 09:18):

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

Right

#### Kevin Buzzard (Feb 14 2019 at 09:19):

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 (Feb 14 2019 at 09:20):

being a projection doesn't mean much to me

#### Mario Carneiro (Feb 14 2019 at 09:20):

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

#### Kevin Buzzard (Feb 14 2019 at 09:21):

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

#### Kevin Buzzard (Feb 14 2019 at 09:21):

You just let it be 0 on K

Wait

#### Kevin Buzzard (Feb 14 2019 at 09:22):

It's more than an extension

#### Mario Carneiro (Feb 14 2019 at 09:22):

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 (Feb 14 2019 at 09:22):

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

That's the key

#### Kevin Buzzard (Feb 14 2019 at 09:23):

f^-1 might not be linear

#### Mario Carneiro (Feb 14 2019 at 09:23):

I mean the inverse coming from that theorem

#### Mario Carneiro (Feb 14 2019 at 09:23):

every surjection splits

Wait

#### Kevin Buzzard (Feb 14 2019 at 09:24):

A random surjection does not split

#### Kevin Buzzard (Feb 14 2019 at 09:24):

This is exactly what we're trying to work around

#### Mario Carneiro (Feb 14 2019 at 09:24):

oh crap that theorem's in vector spaces

Those are free

#### Johan Commelin (Feb 14 2019 at 09:25):

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

#### Kevin Buzzard (Feb 14 2019 at 09:25):

Every vector space has a basis.

#### Mario Carneiro (Feb 14 2019 at 09:25):

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 (Feb 14 2019 at 09:25):

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

#### Kevin Buzzard (Feb 14 2019 at 09:25):

but the integers are not so forgiving.

#### Kevin Buzzard (Feb 14 2019 at 09:26):

Z-modules are abelian groups

#### Kevin Buzzard (Feb 14 2019 at 09:26):

and Z/2Z is not free

#### Mario Carneiro (Feb 14 2019 at 09:26):

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 (Feb 14 2019 at 09:26):

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 (Feb 14 2019 at 09:26):

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 (Feb 14 2019 at 09:27):

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

#### Johan Commelin (Feb 14 2019 at 09:27):

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 (Feb 14 2019 at 09:27):

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 (Feb 14 2019 at 09:28):

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

#### Kevin Buzzard (Feb 14 2019 at 09:28):

Or maybe it's the definition, who knows

#### Kevin Buzzard (Feb 14 2019 at 09:29):

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 (Feb 14 2019 at 09:30):

okay, so exists_left_inverse_linear_map_of_injective needs generalizing

#### Kevin Buzzard (Feb 14 2019 at 09:30):

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 (Feb 14 2019 at 09:31):

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 (Feb 14 2019 at 09:31):

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

#### Kevin Buzzard (Feb 14 2019 at 09:32):

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

#### Mario Carneiro (Feb 14 2019 at 09:32):

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 (Feb 14 2019 at 09:32):

I think that's the only basis in the argument

You have lost me

#### Mario Carneiro (Feb 14 2019 at 09:32):

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

#### Mario Carneiro (Feb 14 2019 at 09:33):

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 (Feb 14 2019 at 09:33):

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 (Feb 14 2019 at 09:34):

oh, oops wrong proof

#### Mario Carneiro (Feb 14 2019 at 09:34):

exists_right_inverse_linear_map_of_surjective

#### Mario Carneiro (Feb 14 2019 at 09:34):

ah, this one only needs one basis

#### Mario Carneiro (Feb 14 2019 at 09:35):

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 (Feb 14 2019 at 09:36):

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 (Feb 14 2019 at 09:36):

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

#### Kevin Buzzard (Feb 14 2019 at 09:37):

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

#### Kevin Buzzard (Feb 14 2019 at 09:37):

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 (Feb 14 2019 at 09:38):

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 (Feb 14 2019 at 09:38):

Neither Q nor Z/10Z is free over Z

right

#### Kevin Buzzard (Feb 14 2019 at 09:38):

But Q is flat over Z :-)

#### Kevin Buzzard (Feb 14 2019 at 09:39):

but that's probably a story for another day

#### Mario Carneiro (Feb 14 2019 at 09:39):

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

#### Kevin Buzzard (Feb 14 2019 at 09:40):

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

not Z?

#### Kevin Buzzard (Feb 14 2019 at 09:40):

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

#### Mario Carneiro (Feb 14 2019 at 09:41):

oh right Z is free

#### Kevin Buzzard (Feb 14 2019 at 09:41):

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

#### Kevin Buzzard (Feb 14 2019 at 09:41):

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

#### Kevin Buzzard (Feb 14 2019 at 09:42):

and all of these are primes

#### Mario Carneiro (Feb 14 2019 at 09:42):

aside: How do you check stuff like that?

#### Kevin Buzzard (Feb 14 2019 at 09:43):

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 (Feb 14 2019 at 09:43):

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 (Feb 14 2019 at 09:43):

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 (Feb 14 2019 at 09:44):

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

#### Kevin Buzzard (Feb 14 2019 at 09:44):

Normal prime numbers can factor, yes

#### Mario Carneiro (Feb 14 2019 at 09:44):

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

#### Kevin Buzzard (Feb 14 2019 at 09:44):

Oh wait, I am using incorrect notation.

#### Kevin Buzzard (Feb 14 2019 at 09:45):

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

#### Kevin Buzzard (Feb 14 2019 at 09:45):

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

#### Mario Carneiro (Feb 14 2019 at 09:45):

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

Yeah.

#### Kevin Buzzard (Feb 14 2019 at 09:46):

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

#### Kevin Buzzard (Feb 14 2019 at 09:46):

(C the complexes)

#### Mario Carneiro (Feb 14 2019 at 09:46):

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

#### Mario Carneiro (Feb 14 2019 at 09:47):

a^2 + 5b^2 or something

#### Kevin Buzzard (Feb 14 2019 at 09:47):

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

#### Kevin Buzzard (Feb 14 2019 at 09:47):

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

#### Kevin Buzzard (Feb 14 2019 at 09:47):

so for this example the stories are the same.

#### Mario Carneiro (Feb 14 2019 at 09:48):

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

#### Mario Carneiro (Feb 14 2019 at 09:48):

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

#### Kevin Buzzard (Feb 14 2019 at 09:48):

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 (Feb 14 2019 at 09:49):

dedekind, I presume?

#### Kevin Buzzard (Feb 14 2019 at 09:49):

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 (Feb 14 2019 at 09:49):

so you need tricks to cut your search space down

#### Kevin Buzzard (Feb 14 2019 at 09:49):

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

#### Mario Carneiro (Feb 14 2019 at 09:49):

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

#### Kevin Buzzard (Feb 14 2019 at 09:50):

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 (Feb 14 2019 at 09:50):

even though they're "coprime"

#### Mario Carneiro (Feb 14 2019 at 09:50):

lol sorry for the distractions

#### Kevin Buzzard (Feb 14 2019 at 09:50):

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

#### Kevin Buzzard (Feb 14 2019 at 09:50):

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

#### Kevin Buzzard (Feb 14 2019 at 09:51):

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

#### Kevin Buzzard (Feb 14 2019 at 09:51):

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 (Feb 14 2019 at 09:52):

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

#### Kevin Buzzard (Feb 14 2019 at 09:52):

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

#### Mario Carneiro (Feb 14 2019 at 09:52):

what does that statement mean here?

#### Kevin Buzzard (Feb 14 2019 at 09:52):

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

and 2=I^2

#### Kevin Buzzard (Feb 14 2019 at 09:53):

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

#### Kevin Buzzard (Feb 14 2019 at 09:53):

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

#### Kevin Buzzard (Feb 14 2019 at 09:54):

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)

interesting

#### Kevin Buzzard (Feb 14 2019 at 09:54):

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

#### Kevin Buzzard (Feb 14 2019 at 09:54):

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

#### Mario Carneiro (Feb 14 2019 at 09:55):

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

#### Kevin Buzzard (Feb 14 2019 at 09:55):

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

#### Kevin Buzzard (Feb 14 2019 at 09:55):

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

#### Kevin Buzzard (Feb 14 2019 at 09:55):

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

lol figures

#### Kevin Buzzard (Feb 14 2019 at 09:56):

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 (Feb 14 2019 at 09:57):

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

#### Kevin Buzzard (Feb 14 2019 at 09:57):

Or maybe Johan PR'ed it

#### Kevin Buzzard (Feb 14 2019 at 09:57):

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

#### Mario Carneiro (Feb 14 2019 at 09:57):

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

#### Kevin Buzzard (Feb 14 2019 at 09:57):

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

#### Mario Carneiro (Feb 14 2019 at 09:57):

or dedekind domains at all

Right.

#### Mario Carneiro (Feb 14 2019 at 09:58):

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

#### Kevin Buzzard (Feb 14 2019 at 09:58):

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 (Feb 14 2019 at 09:58):

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 (Feb 14 2019 at 09:58):

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

#### Kevin Buzzard (Feb 14 2019 at 09:59):

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

#### Kevin Buzzard (Feb 14 2019 at 09:59):

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

#### Kevin Buzzard (Feb 14 2019 at 09:59):

You can make everything trivial if you choose your definitions carefully

#### Kevin Buzzard (Feb 14 2019 at 09:59):

PID -> UFD and UFD's are integrally closed

that's my hope

#### Kevin Buzzard (Feb 14 2019 at 10:00):

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 (Feb 14 2019 at 10:00):

But again we have it in mathlib

#### Kenny Lau (Feb 14 2019 at 10:00):

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 (Feb 14 2019 at 10:00):

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

(and a domain)

#### Kevin Buzzard (Feb 14 2019 at 10:02):

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 (Feb 14 2019 at 10:03):

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

#### Kevin Buzzard (Feb 14 2019 at 10:03):

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 (Feb 14 2019 at 10:04):

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

#### Mario Carneiro (Feb 14 2019 at 10:04):

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

#### Kevin Buzzard (Feb 14 2019 at 10:04):

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

#### Kevin Buzzard (Feb 14 2019 at 10:04):

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

#### Kevin Buzzard (Feb 14 2019 at 10:05):

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

#### Kevin Buzzard (Feb 14 2019 at 10:05):

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

#### Mario Carneiro (Feb 14 2019 at 10:05):

oh you are using the P + K free version

size 2? Not 1?

#### Kevin Buzzard (Feb 14 2019 at 10:06):

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

#### Kevin Buzzard (Feb 14 2019 at 10:06):

$I$ is "locally free of rank 1"

#### Mario Carneiro (Feb 14 2019 at 10:06):

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

#### Kevin Buzzard (Feb 14 2019 at 10:06):

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

oh I+I not I*I

#### Kevin Buzzard (Feb 14 2019 at 10:06):

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

#### Mario Carneiro (Feb 14 2019 at 10:07):

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

#### Kevin Buzzard (Feb 14 2019 at 10:07):

That's not obvious

#### Kevin Buzzard (Feb 14 2019 at 10:08):

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

#### Mario Carneiro (Feb 14 2019 at 10:08):

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

or both?

both

#### Kevin Buzzard (Feb 14 2019 at 10:09):

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

#### Kevin Buzzard (Feb 14 2019 at 10:10):

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 (Feb 14 2019 at 10:10):

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

#### Kevin Buzzard (Feb 14 2019 at 10:10):

I'm sure there will be an elementary argument

#### Mario Carneiro (Feb 14 2019 at 10:10):

wow you have high powered theorems up all your sleeves

#### Kevin Buzzard (Feb 14 2019 at 10:12):

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

#### Mario Carneiro (Feb 14 2019 at 10:13):

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

#### Kevin Buzzard (Feb 14 2019 at 10:14):

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 (Feb 14 2019 at 10:14):

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

#### Kevin Buzzard (Feb 14 2019 at 10:16):

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 (Feb 14 2019 at 10:16):

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 (Feb 14 2019 at 10:17):

lol I'm pretty sure this is your fault

#### Kevin Buzzard (Feb 14 2019 at 10:17):

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 (Feb 14 2019 at 10:17):

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

#### Kevin Buzzard (Feb 14 2019 at 10:17):

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

#### Mario Carneiro (Feb 14 2019 at 10:18):

in metamath vector spaces are over a division ring

#### Mario Carneiro (Feb 14 2019 at 10:18):

literally the whole theory goes through

#### Kevin Buzzard (Feb 14 2019 at 10:18):

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 (Feb 14 2019 at 10:18):

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

until you do

#### Kevin Buzzard (Feb 14 2019 at 10:19):

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

#### Kevin Buzzard (Feb 14 2019 at 10:20):

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 (Feb 14 2019 at 10:20):

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

#### Kevin Buzzard (Feb 14 2019 at 10:20):

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 (Feb 14 2019 at 10:21):

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 (Feb 14 2019 at 10:21):

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

#### Kevin Buzzard (Feb 14 2019 at 10:21):

It means abstractly isomorphic as modules

#### Kevin Buzzard (Feb 14 2019 at 10:22):

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

#### Kevin Buzzard (Feb 14 2019 at 10:22):

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 (Feb 14 2019 at 10:23):

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

#### Mario Carneiro (Feb 14 2019 at 10:23):

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

#### Mario Carneiro (Feb 14 2019 at 10:23):

nonzero elements of the field, I assume

#### Kevin Buzzard (Feb 14 2019 at 10:23):

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

#### Kevin Buzzard (Feb 14 2019 at 10:24):

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

#### Kevin Buzzard (Feb 14 2019 at 10:24):

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

#### Kevin Buzzard (Feb 14 2019 at 10:24):

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

#### Kevin Buzzard (Feb 14 2019 at 10:24):

A fractional ideal is an "ideal with denominator"

#### Kevin Buzzard (Feb 14 2019 at 10:25):

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 (Feb 14 2019 at 10:25):

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

#### Mario Carneiro (Feb 14 2019 at 10:25):

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

#### Kevin Buzzard (Feb 14 2019 at 10:26):

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

#### Kevin Buzzard (Feb 14 2019 at 10:26):

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 (Feb 14 2019 at 10:27):

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

#### Kevin Buzzard (Feb 14 2019 at 10:27):

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

#### Kevin Buzzard (Feb 14 2019 at 10:27):

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

#### Kevin Buzzard (Feb 14 2019 at 10:27):

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

#### Kevin Buzzard (Feb 14 2019 at 10:28):

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 (Feb 14 2019 at 10:29):

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 (Feb 14 2019 at 10:29):

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 (Feb 14 2019 at 10:29):

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

#### Mario Carneiro (Feb 14 2019 at 10:30):

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

#### Kevin Buzzard (Feb 14 2019 at 10:30):

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

#### Kevin Buzzard (Feb 14 2019 at 10:30):

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 (Feb 14 2019 at 10:31):

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

#### Johan Commelin (Feb 14 2019 at 10:31):

And you have Pic(X) for any scheme X

#### Kevin Buzzard (Feb 14 2019 at 10:31):

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 (Feb 14 2019 at 10:32):

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

#### Johan Commelin (Feb 14 2019 at 10:32):

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

#### Kevin Buzzard (Feb 14 2019 at 10:32):

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

#### Johan Commelin (Feb 14 2019 at 10:32):

It's certainly not defeq (-;

#### Kevin Buzzard (Feb 14 2019 at 10:33):

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

#### Kevin Buzzard (Feb 14 2019 at 10:33):

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

#### Johan Commelin (Feb 14 2019 at 10:33):

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

#### Kevin Buzzard (Feb 14 2019 at 10:34):

lemme say one moer thing first

#### Kevin Buzzard (Feb 14 2019 at 10:34):

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 (Feb 14 2019 at 10:34):

I don't think that this is at all obvious

#### Kevin Buzzard (Feb 14 2019 at 10:34):

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

#### Mario Carneiro (Feb 14 2019 at 10:35):

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

#### Kevin Buzzard (Feb 14 2019 at 10:35):

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

#### Kevin Buzzard (Feb 14 2019 at 10:35):

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

#### Mario Carneiro (Feb 14 2019 at 10:35):

any chance of a decision procedure?

#### Johan Commelin (Feb 14 2019 at 10:36):

Yes, there are algorithms for this.

#### Kevin Buzzard (Feb 14 2019 at 10:36):

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 (Feb 14 2019 at 10:36):

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 (Feb 14 2019 at 10:37):

but that's the last one

#### Kevin Buzzard (Feb 14 2019 at 10:37):

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

#### Mario Carneiro (Feb 14 2019 at 10:37):

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

Right

#### Kevin Buzzard (Feb 14 2019 at 10:37):

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

#### Kevin Buzzard (Feb 14 2019 at 10:37):

so the failure of unique factorization gets worse and worse

#### Kevin Buzzard (Feb 14 2019 at 10:38):

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

#### Kevin Buzzard (Feb 14 2019 at 10:38):

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

#### Mario Carneiro (Feb 14 2019 at 10:38):

so, worth it for mathlib?

#### Kevin Buzzard (Feb 14 2019 at 10:39):

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

#### Mario Carneiro (Feb 14 2019 at 10:39):

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

#### Kevin Buzzard (Feb 14 2019 at 10:39):

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 (Feb 14 2019 at 10:40):

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

#### Kevin Buzzard (Feb 14 2019 at 10:40):

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 (Feb 14 2019 at 10:40):

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

#### Mario Carneiro (Feb 14 2019 at 10:40):

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

#### Kevin Buzzard (Feb 14 2019 at 10:40):

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

#### Mario Carneiro (Feb 14 2019 at 10:41):

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

#### Kevin Buzzard (Feb 14 2019 at 10:41):

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 (Feb 14 2019 at 10:42):

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 (Feb 14 2019 at 10:42):

However the proofs all extend easily to Dedekind domains

#### Kevin Buzzard (Feb 14 2019 at 10:42):

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

#### Kevin Buzzard (Feb 14 2019 at 10:43):

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 (Feb 14 2019 at 10:44):

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 (Feb 14 2019 at 10:44):

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

#### Kevin Buzzard (Feb 14 2019 at 10:45):

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

#### Kevin Buzzard (Feb 14 2019 at 10:45):

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

#### Kevin Buzzard (Feb 14 2019 at 10:46):

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

#### Kevin Buzzard (Feb 14 2019 at 10:46):

oh shit and some integration

hmm

#### Kevin Buzzard (Feb 14 2019 at 10:46):

maybe we'd better make them meta algorithms

#### Kevin Buzzard (Feb 14 2019 at 10:47):

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

#### Patrick Massot (Feb 14 2019 at 15:47):

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

Epic quote.

#### Kevin Buzzard (Feb 14 2019 at 16:26):

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

#### Kevin Buzzard (Feb 14 2019 at 16:31):

Vector bundles even!

#### Kevin Buzzard (Feb 14 2019 at 16:32):

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

#### Reid Barton (Feb 14 2019 at 16:52):

Should we prove Swan's theorem?

#### Kevin Buzzard (Feb 14 2019 at 16:55):

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

#### Kevin Buzzard (Feb 14 2019 at 16:56):

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 (Feb 14 2019 at 17:00):

I was thinking of the version for compact Hausdorff spaces

#### Kevin Buzzard (Feb 14 2019 at 17:02):

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 (Feb 14 2019 at 17:03):

Is the proof straightforward?

#### Kevin Buzzard (Feb 14 2019 at 17:04):

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

#### Reid Barton (Feb 14 2019 at 17:05):

... 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 (Feb 14 2019 at 17:06):

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

#### Reid Barton (Feb 14 2019 at 17:11):

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 (Feb 14 2019 at 17:14):

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

#### Kevin Buzzard (Feb 14 2019 at 17:15):

I thought topology got reorganised?

#### Patrick Massot (Feb 14 2019 at 17:15):

only the very first step of the reorganization

#### Patrick Massot (Feb 14 2019 at 17:16):

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 (Feb 14 2019 at 17:16):

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

Last updated: May 14 2021 at 19:21 UTC