kernels of quotient maps

Stream: maths

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Kenny says I should bundle linear maps

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

@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]

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

[Kevin Buzzard]

I thought I'd do the module case

[Kenny Lau]

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

[Kenny Lau]

try submodule.mkq or something

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

does submodule.mkq work?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

"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]

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

[Johan Commelin]

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

[Kevin Buzzard]

Oh yes! You're right.

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

It's not a theorem about arbitrary linear maps

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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

[Johan Commelin]

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]

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

[Kevin Buzzard]

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]

You can find it under the "A".

[Kevin Buzzard]

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]

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