Zulip Chat Archive

Stream: maths

Topic: kernels of quotient maps


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

I was surprised that I couldn't find that the kernel of R -> R / I was I (R a ring, I an ideal)

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

Then I was more surprised that I couldn't find kernels at all.

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

Kenny says I should bundle linear maps

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

import ring_theory.ideal_operations

def module.kernel {R : Type*} [comm_ring R]
{M N : Type*} [add_comm_group M] [add_comm_group N]
[module R M] [module R N] (f : linear_map R M N) :
submodule R M := submodule.comap f 

How am I doing so far?

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

What confuses me now is that submodule.quotient.mk is not a linear_map R M M/P for P a submodule

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

it's just a map M -> M / P

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

@Kenny Lau is what I need already in mathlib? Some analogue of submodule.quotient.mk which produces the structure you want me to use?

view this post on Zulip Kenny Lau (Feb 13 2019 at 09:16):

well it's a ring hom R -> R/I

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

I thought I'd do the module case

view this post on Zulip Kenny Lau (Feb 13 2019 at 09:17):

wait submodule.quotient.mk isn't linear...?

view this post on Zulip Kenny Lau (Feb 13 2019 at 09:17):

try submodule.mkq or something

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

submodule.quotient.mk is just the map M -> M / N

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

No doubt there's a theorem that it's linear

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

but my understanding is that you don't want me to use that map in public

view this post on Zulip Kenny Lau (Feb 13 2019 at 09:18):

does submodule.mkq work?

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

Yes.

import ring_theory.ideal_operations

def module.kernel {R : Type*} [comm_ring R]
{M N : Type*} [add_comm_group M] [add_comm_group N]
[module R M] [module R N] (f : linear_map R M N) :
submodule R M := submodule.comap f 

lemma module.ker_quotient
  {R : Type*} [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M]
  [N : submodule R M] :
module.kernel (submodule.mkq N) = N := sorry

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

I don't know the API for this bundled version but in principle it feels like tehe right thing to do

view this post on Zulip Mario Carneiro (Feb 13 2019 at 17:18):

the kernel of a linear map should definitely be there, I think it is linear_map.ker

view this post on Zulip Mario Carneiro (Feb 13 2019 at 17:20):

theorem submodule.ker_mkq (p : submodule α β) : p.mkq.ker = p

view this post on Zulip Kevin Buzzard (Feb 13 2019 at 18:31):

Excellent! Thanks. I'm learning my way around the bundled module set-up. I've been reading linear_algebra/basic.lean but I was only up to line 600 when I saw your message :-) Why does this theorem live in the submodule namespace, whereas linear_map.ker lives in the linear_map namespace?

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

The quotient is indexed by the submodule, so one can write p.mkq ..., and ker is indexed by the linear map, so one can write f.ker

view this post on Zulip Kevin Buzzard (Feb 13 2019 at 19:25):

"is indexed by..." := "the first input of the function is..."? So this goes back to the dot notation which I was learning about last week.

view this post on Zulip Kevin Buzzard (Feb 13 2019 at 19:26):

I see, so this dot notation trick informs naming conventions.

view this post on Zulip Johan Commelin (Feb 13 2019 at 19:34):

Yes, but it doesn't explain why the theorem is in a particular namespace, right?

view this post on Zulip Kevin Buzzard (Feb 13 2019 at 19:34):

Oh yes! You're right.

view this post on Zulip Johan Commelin (Feb 13 2019 at 19:34):

Well, actually it does... because it is a theorem about submodules...

view this post on Zulip Johan Commelin (Feb 13 2019 at 19:35):

I guess N : submodule is the first argument of the thm

view this post on Zulip Kevin Buzzard (Feb 13 2019 at 19:35):

It's a theorem about the kernel of M -> M / N.

view this post on Zulip Johan Commelin (Feb 13 2019 at 19:35):

But you first need an N, before you can talk about that map

view this post on Zulip Johan Commelin (Feb 13 2019 at 19:35):

It's not a theorem about arbitrary linear maps

view this post on Zulip Kevin Buzzard (Feb 13 2019 at 19:36):

I see, perhaps N is the only input because everything else can be inferred.

view this post on Zulip Kevin Buzzard (Feb 13 2019 at 19:41):

Which somehow makes N the thing which is controlling everything. I guess you know as well as I do Johan that mathematicians never put too much thought into names. I still don't really see what they've got against "Theorem 3.1"...

view this post on Zulip Chris Hughes (Feb 13 2019 at 20:28):

I hate reading notes and seeing "by theorem 7.8". I can never remember what 7.8 is. Mathematicians could definitely learn the habit of better names.

view this post on Zulip Johan Commelin (Feb 13 2019 at 20:30):

But you can infer from the context what the statement of the theorem is! The reference number is there, only if you want to look up the proof.

view this post on Zulip Chris Hughes (Feb 13 2019 at 20:34):

I never attempt to infer. I'll try that in future.

view this post on Zulip Johan Commelin (Feb 13 2019 at 20:37):

Just look at your internal tactic state before and just after the theorem application. The difference is the statement of theorem 7.8.

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

Ok, so this gives us kernels of linear maps between modules. But can I build a linear map from a ring hom?

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

If I said in a lecture "now we're done by theorem abs_pow_mul" or whatever then where is the algorithm which takes this name and finds the theorem earlier in your notes? The advantage of our numbering system is that in the absence of hyperlinks, which is what we had to work with until the 1990s, the "theorem 7.8" notation was a solid way of making referencing previous results easy. The issue is that we now do have hyperlinks but mathematicians haven't adapted.

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

You can find it under the "A".

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

Ok, so this gives us kernels of linear maps between modules. But can I build a linear map from a ring hom?

linear_algebra/basic.lean is quite an easy read :-) but I don't remember seeing it in there. I think it's a recent addition to mathlib that if A -> B is a ring map then B is an A-module.

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

But I don't know where that addition is. Shouldn't be hard to find though, try to make the instance using type class inference and then see what it's called


Last updated: May 18 2021 at 07:19 UTC