## Stream: maths

### Topic: kernels of quotient maps

#### 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)

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

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

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

Kenny says I should bundle linear maps

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

import ring_theory.ideal_operations

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


How am I doing so far?

#### 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

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

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

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

#### Kenny Lau (Feb 13 2019 at 09:16):

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

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

I thought I'd do the module case

#### Kenny Lau (Feb 13 2019 at 09:17):

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

#### Kenny Lau (Feb 13 2019 at 09:17):

try submodule.mkq or something

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

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

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

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

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

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

#### Kenny Lau (Feb 13 2019 at 09:18):

does submodule.mkq work?

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

Yes.

import ring_theory.ideal_operations

def module.kernel {R : Type*} [comm_ring R]
[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


#### 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

#### 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

#### Mario Carneiro (Feb 13 2019 at 17:20):

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


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

#### 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

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

#### Kevin Buzzard (Feb 13 2019 at 19:26):

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

#### Johan Commelin (Feb 13 2019 at 19:34):

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

#### Kevin Buzzard (Feb 13 2019 at 19:34):

Oh yes! You're right.

#### Johan Commelin (Feb 13 2019 at 19:34):

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

#### Johan Commelin (Feb 13 2019 at 19:35):

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

#### Kevin Buzzard (Feb 13 2019 at 19:35):

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

#### Johan Commelin (Feb 13 2019 at 19:35):

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

#### Johan Commelin (Feb 13 2019 at 19:35):

It's not a theorem about arbitrary linear maps

#### Kevin Buzzard (Feb 13 2019 at 19:36):

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

#### 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"...

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

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

#### Chris Hughes (Feb 13 2019 at 20:34):

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

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

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

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

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

You can find it under the "A".

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

#### 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