Zulip Chat Archive

Stream: maths

Topic: free module


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Feb 13 2019 at 22:57):

Unfortunately there \b needs to be a module or something

view this post on Zulip Reid Barton (Feb 13 2019 at 22:57):

oh, I see...

view this post on Zulip Kenny Lau (Feb 13 2019 at 22:57):

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

view this post on Zulip Reid Barton (Feb 13 2019 at 22:57):

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

view this post on Zulip Reid Barton (Feb 13 2019 at 22:58):

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

view this post on Zulip Kenny Lau (Feb 13 2019 at 22:58):

then very good

view this post on Zulip 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?

view this post on Zulip Reid Barton (Feb 13 2019 at 22:58):

because it's finsupp.to_module

view this post on Zulip Kenny Lau (Feb 13 2019 at 22:58):

nothing uses the module structure on \b

view this post on Zulip Kenny Lau (Feb 13 2019 at 22:59):

it's just lc that requires it

view this post on Zulip Reid Barton (Feb 13 2019 at 23:00):

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

view this post on Zulip Kenny Lau (Feb 13 2019 at 23:00):

sadness

view this post on Zulip Reid Barton (Feb 13 2019 at 23:09):

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

view this post on Zulip Kenny Lau (Feb 13 2019 at 23:11):

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

view this post on Zulip Reid Barton (Feb 13 2019 at 23:11):

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

view this post on Zulip 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 }

view this post on Zulip Johannes Hölzl (Feb 13 2019 at 23:46):

can you use smul_right for as inv_fun?

view this post on Zulip Reid Barton (Feb 13 2019 at 23:53):

oh, nice

view this post on Zulip Reid Barton (Feb 14 2019 at 00:00):

edited

view this post on Zulip 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

view this post on Zulip Reid Barton (Feb 14 2019 at 00:03):

is this definition too weird

view this post on Zulip Johan Commelin (Feb 14 2019 at 05:53):

I don't think mathematicians will recognise it

view this post on Zulip Johan Commelin (Feb 14 2019 at 05:53):

I think lc is somewhat unintuitive to use there

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 14 2019 at 05:54):

I guess both :sad:

view this post on Zulip 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

view this post on Zulip Reid Barton (Feb 14 2019 at 05:58):

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

view this post on Zulip Reid Barton (Feb 14 2019 at 06:00):

maybe I should give in and use category theory

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 14 2019 at 06:01):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 14 2019 at 06:18):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:04):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:05):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:05):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:05):

I was told "locally free" was the definition once

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:06):

Ie all localisations were free modules

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:06):

Neither of these involve quantifying over all modules

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:07):

direct summand of free quantifies over all modules

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:07):

dunno what locally free means

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:07):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:08):

In ZFC we only use one universe

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:08):

yeah, then it's an impredicative definition

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:08):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:09):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:09):

That all surjections in M's universe split

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:09):

Hmm

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:10):

Or is that R's universe?

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:10):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:11):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:11):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:12):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:12):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:12):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:13):

It can happen

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:13):

R + S is a ring

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:13):

Making S a projective R module

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:13):

So take R and S rings in different universes

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:14):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:14):

clearly

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:14):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:15):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:15):

I'm not qualified to answer that

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:15):

The commutative diagram suggests non-uniqueness, so maybe not

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:15):

is it "canonical"?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:15):

No

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:16):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:17):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:18):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:18):

All surjections split is one definition of a projective module

view this post on Zulip 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]

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:19):

If that splits, they all do

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:23):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:24):

I can't work out the details :-/

view this post on Zulip 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

view this post on Zulip 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. "

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 14 2019 at 08:31):

May we please have short exact sequences in Lean?

view this post on Zulip Johan Commelin (Feb 14 2019 at 08:31):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:32):

(a) and (b) are equivalent statements

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:33):

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

view this post on Zulip Johan Commelin (Feb 14 2019 at 08:33):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:33):

Why is that ugly?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:33):

I agree that it's one approach

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:33):

I think drawing a picture every time is tiresome

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:33):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:34):

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

view this post on Zulip Johan Commelin (Feb 14 2019 at 08:34):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:34):

like I said, drawing a picture

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:34):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:34):

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

view this post on Zulip 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 ;-)

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:36):

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

view this post on Zulip 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))

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:39):

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

view this post on Zulip Johan Commelin (Feb 14 2019 at 08:40):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:40):

how about no

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:40):

this is a ridiculous notation

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:41):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:41):

the variables notation won't work

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:41):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:41):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:42):

Mathematicians reason by drawing diagrams sometimes.

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:42):

This is hard to do in Lean.

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:42):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:42):

and hence explicable to Lean

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:43):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:43):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:43):

they would just draw a picture

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:44):

choice of sense?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:45):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:45):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:45):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:46):

-- but not necessarily uniquely

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:47):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:47):

oh did I screw up?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:47):

Oh, there are two different lifting definitions

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:48):

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

view this post on Zulip 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 ;-)

view this post on Zulip Mario Carneiro (Feb 14 2019 at 08:48):

okay, so you are halfway there

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:48):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 08:50):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:06):

no but that's just more standard maths

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:08):

Which way do you want to see?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:10):

Whereas Reid's most definitely does not

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:13):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:14):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:14):

is that what surjectivity does?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:14):

And we have P -> P + K

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:14):

do we have AC for Mod(R)?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:14):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:15):

I don't know what AC is

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:15):

oh, I guess we have it: exists_right_inverse_linear_map_of_surjective

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:15):

I mean every surjection splits in Mod(R)

view this post on Zulip Johan Commelin (Feb 14 2019 at 09:16):

@Kevin Buzzard AC = axiom of choice :lol:

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:16):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:17):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:17):

And that's the map we can lift

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:17):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:17):

like is that K needed at all?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:17):

Yes

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:18):

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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:18):

Right

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:20):

being a projection doesn't mean much to me

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:20):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:21):

You just let it be 0 on K

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:21):

Wait

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:22):

It's more than an extension

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:22):

That's the key

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:23):

f^-1 might not be linear

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:23):

I mean the inverse coming from that theorem

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:23):

every surjection splits

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:23):

Wait

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:24):

A random surjection does not split

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:24):

This is exactly what we're trying to work around

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:24):

oh crap that theorem's in vector spaces

view this post on Zulip Johan Commelin (Feb 14 2019 at 09:24):

Those are free

view this post on Zulip Johan Commelin (Feb 14 2019 at 09:25):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:25):

Every vector space has a basis.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:25):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:25):

but the integers are not so forgiving.

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:26):

Z-modules are abelian groups

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:26):

and Z/2Z is not free

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:27):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:28):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:28):

Or maybe it's the definition, who knows

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:30):

okay, so exists_left_inverse_linear_map_of_injective needs generalizing

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:31):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:32):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:32):

I think that's the only basis in the argument

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:32):

You have lost me

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:32):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:34):

oh, oops wrong proof

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:34):

exists_right_inverse_linear_map_of_surjective

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:34):

ah, this one only needs one basis

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:37):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:38):

Neither Q nor Z/10Z is free over Z

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:38):

right

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:38):

But Q is flat over Z :-)

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:39):

but that's probably a story for another day

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:40):

not Z?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:40):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:41):

oh right Z is free

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:41):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:42):

and all of these are primes

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:42):

aside: How do you check stuff like that?

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:44):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:44):

Normal prime numbers can factor, yes

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:44):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:44):

Oh wait, I am using incorrect notation.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:45):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:46):

Yeah.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:46):

(C the complexes)

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:47):

a^2 + 5b^2 or something

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:47):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:47):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:47):

so for this example the stories are the same.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:48):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:49):

dedekind, I presume?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:49):

so you need tricks to cut your search space down

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:49):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:49):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:50):

even though they're "coprime"

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:50):

lol sorry for the distractions

view this post on Zulip 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))

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:50):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:51):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:52):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:52):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:52):

what does that statement mean here?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:53):

and 2=I^2

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:53):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:53):

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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:54):

interesting

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:54):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:54):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:55):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:55):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:55):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:56):

lol figures

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:57):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:57):

Or maybe Johan PR'ed it

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:57):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:57):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:57):

or dedekind domains at all

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:58):

Right.

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:58):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:58):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:59):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:59):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:59):

You can make everything trivial if you choose your definitions carefully

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 09:59):

PID -> UFD and UFD's are integrally closed

view this post on Zulip Mario Carneiro (Feb 14 2019 at 09:59):

that's my hope

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:00):

But again we have it in mathlib

view this post on Zulip 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 ~

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:00):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:01):

(and a domain)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:03):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:04):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:04):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:04):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:04):

and this implies that III\oplus I is free

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:05):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:05):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:05):

oh you are using the P + K free version

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:05):

size 2? Not 1?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:06):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:06):

II is "locally free of rank 1"

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:06):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:06):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:06):

oh I+I not I*I

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:06):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:07):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:07):

That's not obvious

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:08):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:08):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:08):

or both?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:08):

both

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:09):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:10):

and II 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:10):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:10):

I'm sure there will be an elementary argument

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:10):

wow you have high powered theorems up all your sleeves

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:12):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:14):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:15):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:17):

lol I'm pretty sure this is your fault

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:17):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:17):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:18):

in metamath vector spaces are over a division ring

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:18):

literally the whole theory goes through

view this post on Zulip 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

view this post on Zulip 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 :-)

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:18):

until you do

view this post on Zulip 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??"

view this post on Zulip 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!

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:20):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:21):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:21):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:21):

It means abstractly isomorphic as modules

view this post on Zulip 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

view this post on Zulip 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)(a) to (b)(b) you just multiply by b/ab/a

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:23):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:23):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:23):

nonzero elements of the field, I assume

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:24):

RR a Dedekind domain, KK its field of fractions

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:24):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:24):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:24):

A fractional ideal is an "ideal with denominator"

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:25):

i.e. a subset JJ of KK such that there exists some non-zero rRr\in R such that rJrJ is a regular non-zero ideal

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:25):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:25):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:26):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:27):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:27):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:27):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:27):

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

view this post on Zulip 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 RR then there are other orbits

view this post on Zulip 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.

view this post on Zulip 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 RR then there are other orbits

iff

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:29):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:30):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:30):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 14 2019 at 10:31):

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

view this post on Zulip Johan Commelin (Feb 14 2019 at 10:31):

And you have Pic(X) for any scheme X

view this post on Zulip 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×K^\times

view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:32):

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

view this post on Zulip Johan Commelin (Feb 14 2019 at 10:32):

It's certainly not defeq (-;

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:33):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:33):

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

view this post on Zulip Johan Commelin (Feb 14 2019 at 10:33):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:34):

lemme say one moer thing first

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:34):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:34):

I don't think that this is at all obvious

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:34):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:35):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:35):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:35):

any chance of a decision procedure?

view this post on Zulip Johan Commelin (Feb 14 2019 at 10:36):

Yes, there are algorithms for this.

view this post on Zulip 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

view this post on Zulip 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 Q((163)1/2)\mathbb{Q}((-163)^{1/2}) is trivial

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:37):

but that's the last one

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:37):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:37):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:37):

Right

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:37):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:37):

so the failure of unique factorization gets worse and worse

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:38):

so, worth it for mathlib?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:39):

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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:40):

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

view this post on Zulip Mario Carneiro (Feb 14 2019 at 10:41):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:42):

However the proofs all extend easily to Dedekind domains

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:42):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:45):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:45):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:46):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:46):

oh shit and some integration

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:46):

hmm

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 10:46):

maybe we'd better make them meta algorithms

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 16:26):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 16:31):

Vector bundles even!

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 16:32):

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

view this post on Zulip Reid Barton (Feb 14 2019 at 16:52):

Should we prove Swan's theorem?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Feb 14 2019 at 17:00):

I was thinking of the version for compact Hausdorff spaces

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 17:03):

Is the proof straightforward?

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 17:04):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 17:06):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 14 2019 at 17:14):

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

view this post on Zulip Kevin Buzzard (Feb 14 2019 at 17:15):

I thought topology got reorganised?

view this post on Zulip Patrick Massot (Feb 14 2019 at 17:15):

only the very first step of the reorganization

view this post on Zulip 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

view this post on Zulip 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