Stream: maths

Topic: issue with bundled subgroups

Kevin Buzzard (Mar 06 2020 at 17:51):

@Jason KY. has been bundling subgroups at Xena (for mathlib), and I've been doing preliminary experiments in @Shenyang Wu 's repository here. Here's something I ran into.

The type of monoid homomorphisms between monoids M and N is just denoted M →* N, notation for monoid_hom M N. Now say G and H are groups. Because a group is a monoid, and a group homomorphism is just a monoid homomorphism between groups, one can just use G →* H to denote group homomorphisms. This initially looks like a cool idea.

But now say I want to define map : (G →* H) → (subgroup G) → (subgroup H), pushing forward a subgroup of G by taking its image under the function G → H. monoid_hom.map is already taken, and it doesn't have this type (it maps submonoids to submonoids). Because subgroup is not a class predicate on submonoid it seems to me that I need another function. Maybe it could be called group_hom.map. Ideally I'd like to use dot notation and have f.map K for K : subgroup H. In which case maybe I should define @[reducible] def group_hom G H := monoid_hom G H. But now I lose the notation →* for group homs. I also had problems with dot notation -- e.g. (in the additive case -- but it makes no difference)

#check @add_group_hom.comap
/-
comap :
Π {G₁ : Type u_3} [_inst_3 : add_group G₁] {G₂ : Type u_4} [_inst_4 : add_group G₂],
-/

def ker' (f : add_group_hom G H) : add_subgroup G := f.comap f ⊥ -- fails:
/-
does not have explicit argument with type (add_group_hom ...)
-/
def ker (f : add_group_hom G H) : add_subgroup G := add_group_hom.comap f ⊥ -- works fine


so I seemed to have lost projection notation anyway. Is this a bug?

In writing all this down it occurs to me that another solution is to define add_monoid_hom.gmap, monoid_hom.gcomap, monoid_hom.gker and so on, and not defining group_hom at all. Or even one could argue that because groups are more popular than monoids, map could be the group one and mmap could be the monoid one.

Anyone have any thoughts about these issues?

Chris Hughes (Mar 06 2020 at 17:56):

Shouldn't this be subgroup.map not group_hom.map. Otherwise you're insisting that subgroup is the only functor on the category of groups.

Kevin Buzzard (Mar 06 2020 at 18:00):

This was something else that occurred to me, in fact we changed Shenyang's repository today from that convention to the one I was talking about in my post above (and that's why we ran into this issue). This is currently how it works for monoids though: see https://github.com/leanprover-community/mathlib/blob/36b336cb81612e0c4a37181a93262fb5d1a15fbf/src/group_theory/submonoid.lean#L725 and note line 708. Is this a bad convention?

Kevin Buzzard (Mar 06 2020 at 18:01):

If one can argue for your convention with map, let's instead talk about ker. I want f.ker to return a subgroup, and it currently returns a submonoid (actually it might not yet exist, I'm not sure, but if and when it exists it will presumably be a submonoid). Related is im and range.

Chris Hughes (Mar 06 2020 at 18:02):

Usually the name is name_of_functor.map. So it is a bad convention

Chris Hughes (Mar 06 2020 at 18:05):

I'm not sure kernels are a particularly useful thing for monoids, since the kernels being equal does not imply that the images are isomorphic. I'm not sure it should return a submonoid.

Kevin Buzzard (Mar 06 2020 at 18:08):

The reason this came up for Shenyang was that we want to prove that group cohomology is a functor, so we need that if $f:A\to B$ is a morphism of abelian additive groups and we have $A_0\subseteq A$ and $B_0\subseteq B$ subgroups with $f(A_0)\subseteq B_0$ then we get an induced map $A/A_0\to B/B_0$. When we were proving the lemmas needed to construct this I needed stuff about comaps and kernels etc. So they (by which I mean images and kernels) are certainly needed, or at least extremely useful, for subgroups.

Chris Hughes (Mar 06 2020 at 18:11):

You just have to think of different names for images in monoids and images in groups.

Reid Barton (Mar 06 2020 at 18:15):

Have you considered just using the category AddCommGroup?

Reid Barton (Mar 06 2020 at 18:16):

Probably a bug that it isn't called Ab

Kevin Buzzard (Mar 06 2020 at 18:22):

Reid Barton said:

Have you considered just using the category AddCommGroup?

My perception is that it's much harder to work with Ab because there is less infrastructure, and Shenyang has to hand in his thesis in a few months. My impression is that @Amelia Livingston will be doing an MSc project with me next year, perhaps she'll be brave enough to try?

Reid Barton (Mar 06 2020 at 18:22):

You don't actually need any infrastructure

Reid Barton (Mar 06 2020 at 18:22):

I don't really get this perception

Reid Barton (Mar 06 2020 at 18:23):

It's literally just bundling groups and bundling morphisms

Kevin Buzzard (Mar 06 2020 at 18:25):

I might just be completely wrong. Last time I worked with categories I was trying to do something much harder (gluing sheaves etc) and found it very slow going (perhaps partly because I was learning the library as well).

Reid Barton (Mar 06 2020 at 18:26):

Yes, I agree that's a lot more involved.

Kevin Buzzard (Mar 06 2020 at 18:26):

This is bad. There are two very serious (non-Lean-related) jobs which I need to work on, and probably I should spend all weekend working on them, but all I want to do now is to see if Ab solves problems or creates them.

Kevin Buzzard (Mar 06 2020 at 18:29):

Can you help to start me off here? Shenyang has spent quite some time defining the group of n-cochains, and the subgroups of n-cocycles and n-coboundaries. When do we break intoAb?

Reid Barton (Mar 06 2020 at 18:29):

I assume the second part means: defining the differentials

Kevin Buzzard (Mar 06 2020 at 18:30):

To be a bit more precise he has cochain n G M an additive abelian group, and d : cochain n G M -> cochain (n+1) G M and he's proved $d^2=0$

Kevin Buzzard (Mar 06 2020 at 18:30):

and that d is an add_monoid_hom.

Kevin Buzzard (Mar 06 2020 at 18:31):

and it will not be hard to prove that $f:M\to N$ gives cochain n G M ->+ cochain n G N commuting with d. Can we just leave all this work alone?

Reid Barton (Mar 06 2020 at 18:31):

Yes, so all these concrete constructions make sense to do the way you have done them

Reid Barton (Mar 06 2020 at 18:31):

(assuming you don't want to build the cochains as an instance of some more general construction)

Kevin Buzzard (Mar 06 2020 at 18:32):

But now you're proposing that $H^n(G,M)$ be defined as an object of Ab?

Reid Barton (Mar 06 2020 at 18:32):

then you can tack on a AddCommGroup.of in front of your cochain n G M and turn d into a morphism (I think just definitionally)

Reid Barton (Mar 06 2020 at 18:33):

Any homological algebra like the induced map on homology from a map of chain complexes is going to be a huge mess unbundled

Reid Barton (Mar 06 2020 at 18:33):

and it will be a somewhat smaller mess if you bundle the objects

Kevin Buzzard (Mar 06 2020 at 18:33):

How do I do subgroups? Is the kernel just another object?

Kevin Buzzard (Mar 06 2020 at 18:34):

I see, I need a map from Im(d_n) to ker(d_{n+1}) and then I just define cohomology to be the cokernel. Are there cokernels in Ab? I don't even know where to look!

Reid Barton (Mar 06 2020 at 18:35):

I don't advise trying to use some general category theory notion of cokernel. Just define the object the same way you normally would, stick AddCommGroup.of in front of it and prove that it has the correct universal property

Kevin Buzzard (Mar 06 2020 at 18:38):

I'm now trying to understand what problem we're solving here.

Reid Barton (Mar 06 2020 at 18:38):

Basically, use the category theory library as though you only knew what the definition of a category is

Kevin Buzzard (Mar 06 2020 at 18:39):

I knew (or at least I thought I knew, until I ran into the issues which prompted this thread) exactly what I was doing bundling subgroups. What am I supposed to be doing with Ab?

Reid Barton (Mar 06 2020 at 18:40):

The main problem is

variables {A₁ B₁ C₁ D₁ E₁ : Type u}
variables {A₂ B₂ C₂ D₂ E₂ : Type u}

variables  [group A₁]    {f₁ : A₁ → B₁}   [group B₁]    {g₁ : B₁ → C₁}   [group C₁]    {h₁ : C₁ → D₁}   [group D₁]    {i₁ : D₁ → E₁}   [group E₁]
variables {j : A₁ → A₂}                  {k : B₁ → B₂}                  {l : C₁ → C₂}                  {m : D₁ → D₂}                  {n : E₁ → E₂}
variables  [group A₂]    {f₂ : A₂ → B₂}   [group B₂]    {g₂ : B₂ → C₂}   [group C₂]    {h₂ : C₂ → D₂}   [group D₂]    {i₂ : D₂ → E₂}   [group E₂]

variables [is_group_hom f₁] [is_group_hom g₁] [is_group_hom h₁] [is_group_hom i₁]
variables [is_group_hom f₂] [is_group_hom g₂] [is_group_hom h₂] [is_group_hom i₂]
variables [is_group_hom j] [is_group_hom k] [is_group_hom l] [is_group_hom m] [is_group_hom n]


Kevin Buzzard (Mar 06 2020 at 18:40):

Is there an analogue of map, comap, ker, im, range?

(thanks Johan)

Johan Commelin (Mar 06 2020 at 18:40):

I didn't do the snake lemma...

Kevin Buzzard (Mar 06 2020 at 18:41):

Only the 5 lemma? It was what got you started though, right?

Johan Commelin (Mar 06 2020 at 18:41):

I guess that will be on the wishlist sometime soon.

Reid Barton (Mar 06 2020 at 18:41):

I know group homs are bundled now, so you are already halfway there

Johan Commelin (Mar 06 2020 at 18:41):

Yeah, the good old times :rolling_on_the_floor_laughing:

Reid Barton (Mar 06 2020 at 18:43):

(what's the difference between im and range?)

Kevin Buzzard (Mar 06 2020 at 18:44):

Oh maybe im := map and range = map univ

Reid Barton (Mar 06 2020 at 18:44):

map I don't even know what it is.

Reid Barton (Mar 06 2020 at 18:45):

I would try to get away from subsets, and just use morphisms which are monos

Kevin Buzzard (Mar 06 2020 at 18:46):

map is supposed to be the function which pushes forward a subgroup of G to a subgroup of H under a group hom G -> H.

Reid Barton (Mar 06 2020 at 18:48):

I would just add some 1-2 line wrapper for whatever you need along these lines and then some lemmas which characterize it

Reid Barton (Mar 06 2020 at 18:49):

Often you can also get away with the lemmas because they are true by defeq

Kevin Buzzard (Mar 06 2020 at 18:49):

For example I looked at the quotient group file and thought "right, that's the API for quotient groups, let's make it in the bundled setting" and then my task was clear. Here I'm a bit less clear about what I should be doing. Maybe I should just try and prove that cohomology is a functor...should I make G-modules a category??

Reid Barton (Mar 06 2020 at 18:49):

How else are you going to state this fact?

Kevin Buzzard (Mar 06 2020 at 18:50):

Well I guess my plan was to literally just prove all the things which needed proving but not use categories at all.

I see

:-)

Kevin Buzzard (Mar 06 2020 at 18:52):

And again I can see why I naturally shy away from categories -- I know exactly how to make a G_module type (indeed Anca did this last year) but I don't really know how to make a good G_module category.

Reid Barton (Mar 06 2020 at 18:52):

so define for every type M which is an add_comm_group with an action of G, a type H^n(G, M) for each n, which has an instance of add_comm_group, and then separately for every map of G-modules, a map on cohomology, and then prove some stuff commutes

Reid Barton (Mar 06 2020 at 18:52):

We have R-modules already, so it should basically be a copy-and-paste job from that. Or you could define Ext :upside_down:

Kevin Buzzard (Mar 06 2020 at 18:53):

G-modules and G-module maps

Kevin Buzzard (Mar 06 2020 at 18:53):

Should I make a category of G-modules, or put a G-action on an object of Ab?

Reid Barton (Mar 06 2020 at 18:54):

oh yeah, maybe we already have G-modules then?

in that sense

Kevin Buzzard (Mar 06 2020 at 18:54):

That's not mathlib: I don't have the energy to show my students how to make code mathlib-acceptable so it just bitrots instead, but at least they write good projects.

Reid Barton (Mar 06 2020 at 18:54):

https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/single_obj.lean#L61

Kevin Buzzard (Mar 06 2020 at 18:55):

Where are R-modules? I don't know my way around.

Reid Barton (Mar 06 2020 at 18:55):

so you could define G-modules to be the category single_obj G ⥤ Ab

Reid Barton (Mar 06 2020 at 18:56):

https://github.com/leanprover-community/mathlib/blob/master/src/algebra/category/Module/basic.lean

Kevin Buzzard (Mar 06 2020 at 18:56):

Reid Barton said:

so you could define G-modules to be the category single_obj G ⥤ Ab

Will there be now be like 6 universes floating around?

Kevin Buzzard (Mar 06 2020 at 18:57):

What are your feelings about just sticking to Type and making things large/small categories as appropriate?

Kevin Buzzard (Mar 06 2020 at 18:58):

instead of this insane polymorphism that the CS guys are always going on about and which I still don't really see the point of?

Reid Barton (Mar 06 2020 at 18:58):

Highly recommended if you have no particular need for the generality and just want to have a working project

Reid Barton (Mar 06 2020 at 18:58):

If you want more generality, then also recommended is to fix a single Type u as much as possible. But u = 0 is also fine

Kevin Buzzard (Mar 06 2020 at 18:59):

I can live with one universe. I don't know how much pain it will cause. I know that the first time I tried categories I had some real universe hell, but my understanding is that you and Scott have somehow managed to tame it all now.

Reid Barton (Mar 06 2020 at 18:59):

Kevin Buzzard said:

Reid Barton said:

so you could define G-modules to be the category single_obj G ⥤ Ab

Will there be now be like 6 universes floating around?

To answer your question, I think you would have the same universe variables as in class G_module but I don't really understand Type*

Reid Barton (Mar 06 2020 at 19:00):

In a lot of the homotopy theory project, I define local notation Top := Top.{0}

Reid Barton (Mar 06 2020 at 19:01):

mainly because I want to use the real numbers and didn't feel like dealing with ulift

Reid Barton (Mar 06 2020 at 19:02):

If you do use single_obj G ⥤ Ab I would encourage first defining some conversions between that and G_module as a sanity check

Reid Barton (Mar 06 2020 at 19:02):

and possibly this functor definition could get annoying, I'm not sure

Kevin Buzzard (Mar 06 2020 at 19:02):

I might give this a go. I have this worry that my initial enthusiasm for having found another excuse to dip my toes into category land will soon wear off as I realise that categories are hard in Lean, but maybe each time I try them they'll be less hard. Yes I remember the ulift issues with the reals. We have punit, right? How about preal?

Reid Barton (Mar 06 2020 at 19:06):

Okay, so looking at

/-- A->B->C -/
(f : A → B) (g : B → C) [is_add_group_hom f] [is_add_group_hom g] : Prop :=
range f = ker g


the idea is to change it to something like

def is_exact {A B C : Ab} (f : A ⟶ B) (g : B ⟶ C) : Prop :=
range f = ker g


relying on the coercion from the hom types of Ab to functions

Reid Barton (Mar 06 2020 at 19:06):

or to +-homomorphisms now or whatever

Kevin Buzzard (Mar 06 2020 at 19:08):

Will the range really equal the ker here?

Reid Barton (Mar 06 2020 at 19:09):

yes, range f : set B where there is also a coercion from B to Type

Reid Barton (Mar 06 2020 at 19:09):

I mean the same range as now

Kevin Buzzard (Mar 06 2020 at 19:09):

I've just realised that I don't understand exact sequences in an abelian category properly

Kevin Buzzard (Mar 06 2020 at 19:10):

Oh OK I know how to do it, it's just that's not the way we're going to do it here.

Reid Barton (Mar 06 2020 at 19:11):

I am not trying to say you should never get your hands dirty with elements and subsets and stuff, just that you can use a language where the chunk size is closer to what you are used to.

Kevin Buzzard (Mar 06 2020 at 19:11):

there's some induced map range f -> ker g in the non-concrete setting and you want it to be an iso or whatever.

Reid Barton (Mar 06 2020 at 19:13):

Maybe for an undergraduate the {A B C : Type*} [add_comm_group A] [add_comm_group B] [add_comm_group C] (f : A → B) (g : B → C) [is_add_group_hom f] [is_add_group_hom g] does actually reflect their mental model, but probably not by the time you're doing homological algebra/group cohomology.

Reid Barton (Mar 06 2020 at 19:14):

(Is this on an old mathlib? Or are there still both bundled and unbundled group homomorphisms?)

Kevin Buzzard (Mar 06 2020 at 19:15):

Anca's group cohomology project is over a year old and I don't think she had access to bundled group homs.

I see

Reid Barton (Mar 06 2020 at 19:15):

It's similar in topology, we do not have bundled continuous maps

Kevin Buzzard (Mar 06 2020 at 19:16):

Shenyang is using bundled homs. The reason all this started was that group cohomology is probably the cohomology theory I understand best so I thought it would be an interesting topic, particularly when I realised that in theory it should be straightforward but actually it was really hard to find any examples of any cohomology theories at all in any theorem prover.

Kevin Buzzard (Mar 06 2020 at 19:16):

Anca just did H^0 and H^1, she was a BSc student and I thought that the 7 term exact sequence was plenty for a Bachelors project.

Kevin Buzzard (Mar 06 2020 at 19:17):

Is singular cohomology formalised in any theorem prover at all?

Reid Barton (Mar 06 2020 at 19:17):

At first I thought it was kind of pointless to define group cohomology, because you can express it as a special case of various other constructions. But then I realized that sometimes you just want to sit down with a 1-cocycle and calculate stuff with it, and then you also want to know that the thing you define using explicit cocyles calculates H^1. So you have to write down the cocycle-based group cohomology construction anyways.

Reid Barton (Mar 06 2020 at 19:18):

Oh wow, I didn't notice this H^1 stuff.

Reid Barton (Mar 06 2020 at 19:19):

I suppose you'll even have a small instance of this issue when you want to know that group cohomology H^n defined using n-cocyles specializes to H^1 using crossed homomorphisms when n=1

Reid Barton (Mar 06 2020 at 19:19):

Kevin Buzzard said:

Is singular cohomology formalised in any theorem prover at all?

Yes, actually it is formalized in HOL Light I think

Reid Barton (Mar 06 2020 at 19:20):

https://www.mathematics.pitt.edu/hales60/pdf/Harrison-John.pdf

Reid Barton (Mar 06 2020 at 19:21):

Hard to find when you don't know how to spell HOL Light :face_palm:

Reid Barton (Mar 06 2020 at 19:24):

Also Johan defined singular homology in a PR. But Harrison's formalization has actual theorems.

Kevin Buzzard (Mar 06 2020 at 19:31):

Aah but that's singular homology ;-)

Kevin Buzzard (Mar 06 2020 at 19:33):

Reid Barton said:

At first I thought it was kind of pointless to define group cohomology, because you can express it as a special case of various other constructions.

Sure, but I think that nonetheless these are good projects for students, and they typically teach me stuff about Lean. One could argue that it's kind of pointless to do anything in Lean 3 and we should all just sit and wait for Lean 4, but it's just too much fun.

Reid Barton (Mar 06 2020 at 19:36):

But even just thinking about what things mathlib ought to have in an ideal world, even if you define group cohomology using Ext or something, surely another of those things is "the way you can compute group cohomology using cocycles", and this is tantamount to defining group cohomology the way you're doing it now

Kevin Buzzard (Mar 06 2020 at 19:38):

I'm not sure I ever got to the bottom of this MO question

Reid Barton (Mar 06 2020 at 19:40):

(Also I don't know what the right way to really understand group cohomology of a profinite group is, unless the answer is condensed sets? Related to my recent question here)

Reid Barton (Mar 06 2020 at 19:40):

or is the point you only consider discrete modules?

Kevin Buzzard (Mar 06 2020 at 19:41):

I wonder if people understand this better now. If the module is discrete it's fine, but definitely in number theory people consider continuous cohomology with coefficients the p-adic integers, and people are dimly aware that this isn't a derived functor. I think that under mild hypotheses there's still a long exact sequence.

Reid Barton (Mar 06 2020 at 19:42):

I think I just realized that I didn't understand exactly what the issue I didn't understand was

Kevin Buzzard (Mar 06 2020 at 19:42):

I think the issue is that if you have a continuous surjection $B\to C$ then you can't necessarily find a continuous set-theoretic splitting, so the naive attempt to define the boundary map $H^0(C)\to H^1(A)$ fails.

Reid Barton (Mar 06 2020 at 19:42):

Kevin Buzzard said:

people consider continuous cohomology with coefficients the p-adic integers

is it defined as an inverse limit of cohomology with coefficients in Z/p^n?

Kevin Buzzard (Mar 06 2020 at 19:43):

(if you're defining $H^n$ as continuous cocycles over continuous coboundaries)

Kevin Buzzard (Mar 06 2020 at 19:43):

People really do use this "continuous cocycles" definition. I think it is the same as the inverse limit definition you just suggested. Problem is that inverse limits aren't exact so you don't automatically get exactness of the long (non)-exact sequence.

Reid Barton (Mar 06 2020 at 19:44):

So in the discrete coefficients case, there is still an honest abelian category right? But it's not a category of R-modules for a ring R like it would be in the finite (or discrete) group case

Kevin Buzzard (Mar 06 2020 at 19:45):

In the discrete case it's not a category of R-modules, but you can define the cohomology groups as direct limits which do preserve exactness. I am pretty sure it's an abelian category, all I know is that the parts of the formalism I need work :-)

Reid Barton (Mar 06 2020 at 19:46):

Like a limit over the finite quotients of the group?

Kevin Buzzard (Mar 06 2020 at 19:46):

$H^n(G,M):=lim_{\to}H^n(G/U,M^U)$

Kevin Buzzard (Mar 06 2020 at 19:47):

as $U$ ranges over the open (and hence finite index) normal subgroups

Kevin Buzzard (Mar 06 2020 at 19:47):

and this is fine for discrete modules.

Kevin Buzzard (Mar 06 2020 at 19:48):

and there's certainly a long exact sequence and almost surely a Hochschild-Serre spectral sequence but it's been a long time since I checked all the details of this.

Kevin Buzzard (Mar 06 2020 at 19:48):

But the moment $M$ is not discrete I know very little, beyond the fact that in some cases everything works out anyway.

Kevin Buzzard (Mar 06 2020 at 20:31):

OK so here are the exciting issues I've run into already:
1) single_obj G isn't a small category if (G : Type u) because the object of single_obj is unit not punit
2) type class inference isn't making G-modules a category:

import category_theory.single_obj
import algebra.category.Group
import category_theory.functor_category

open category_theory

def group_module (G : Type) [group G] := single_obj G ⥤ AddCommGroup

variables (G : Type) [group G]

instance : category (group_module G) :=
--   by apply_instance -- fails
functor.category _ _


Reid Barton (Mar 06 2020 at 20:33):

The second one is just normal behavior of instances

Johan Commelin (Mar 06 2020 at 20:35):

You can @[derive category] the instance when you define it, or prove it by delta group_module; apply_instance.

Reid Barton (Mar 06 2020 at 20:36):

For the first, does it matter whether single_obj G is a small category?

Reid Barton (Mar 06 2020 at 20:38):

I would perhaps do this

universe u

def group_module (G : Type u) [group G] := single_obj G ⥤ AddCommGroup.{u}

instance (G : Type u) [group G] : large_category (group_module G) :=
by delta group_module; apply_instance


Kevin Buzzard (Mar 06 2020 at 20:48):

Well my plan was to stick to one universe Type u and then just to make all the categories have the size they'd have in ZFC -- so the single object one small, the abelian groups large, and G-module large. But single_obj seems to have decided that u=0. I don't know if it matters. I was just imagining that making everything the right size instead of polymorphic world instantly remove all universe issues. Of course you're both right about the second issue -- thanks

Kevin Buzzard (Mar 06 2020 at 20:49):

Oh apparently it doesn't matter, the G-modules are u-large anyway

Reid Barton (Mar 06 2020 at 20:51):

I think it would in fact be better to make single_obj G be a small category, but in this situation I don't think it will make a difference (unless you try to define M^G as the limit of this diagram)

Scott Morrison (Mar 06 2020 at 21:47):

I just PR'd limits and colimits in AddCommGroup, in case that is useful for Kevin's current investigations. I added a small tutorial file, which for now just contains:

import algebra.category.Group
import category_theory.limits.shapes.kernels

open category_theory
open category_theory.limits

/-!
Some small examples of using limits and colimits in Ab, the category of additive commutative groups.
-/

example (G H : Ab) (f : G ⟶ H) : Ab := kernel f
example (G H : Ab) (f : G ⟶ H) [epi f] : kernel (cokernel.π f) ≅ H := as_iso (kernel.ι (cokernel.π f))

-- TODO no images yet...


Kevin Buzzard (Mar 06 2020 at 21:49):

Thanks! I'm currently working on this. I don't think I want Shenyang to go down the category theory route really but I'm interested in experimenting myself.

Johan Commelin (Mar 06 2020 at 21:49):

Scott Morrison said:

-- TODO no images yet...


This.

Kevin Buzzard (Mar 06 2020 at 21:50):

Ha ha, since when was it called Ab for real? :-)

Scott Morrison (Mar 06 2020 at 21:52):

Just added this in the PR. It is just an abbreviation for AddCommGroup, and the library itself still says AddCommGroup throughout.

Reid Barton (Mar 06 2020 at 22:03):

What does kernel f end up being in this case?

Scott Morrison (Mar 06 2020 at 22:28):

In this case it will be a horrible thing, because I've just pulled things out of general limits. So in particular it will the subset of functions from the walking_parallel_pair type (which has two elements, called left and right) which assign to left an element of G and to right an element of H, such that the element in G gets sent to the element in H, and gets sent to zero. :-)

Use the API. :-)

Scott Morrison (Mar 06 2020 at 22:28):

And don't look under the hood.

Scott Morrison (Mar 06 2020 at 22:29):

We can add the definitionally nice shortcut instances as well if we want to.

Reid Barton (Mar 07 2020 at 00:07):

My concern is that, particularly for the cokernel, the best way to use the API may sometimes be: define the cokernel in the obvious way, prove that it satisfies the universal property, then use the uniqueness up to isomorphism of the cokernel to transfer (at your own expense) the statement that you can check for the obvious cokernel to whatever one you get from the instance.

Reid Barton (Mar 07 2020 at 00:07):

For example, try proving if f : G -> H is a mono and G and H are finite, then |cokernel f| = |H| / |G|.

Scott Morrison (Mar 07 2020 at 00:09):

Yes, that sounds reasonable.

Scott Morrison (Mar 07 2020 at 05:29):

Okay, I've updated that tutorial file, as of #2101. Now we have images, and defining exactness is one line away:

import algebra.category.Group
import category_theory.limits.shapes.kernels

open category_theory
open category_theory.limits

local notation Ab := Ab.{0}

/-!
Some small examples of using limits and colimits in Ab, the category of additive commutative groups.
-/

example (G H : Ab) (f : G ⟶ H) : Ab := kernel f

example (G H : Ab) (f : G ⟶ H) [epi f] : kernel (cokernel.π f) ≅ H := as_iso (kernel.ι (cokernel.π f))

-- Since Ab has equalizers, we automatically get the fact that
-- in the factorization of f as G --(factor_thru_image f)--> image f --(image.ι f)--> H,
-- the morphism factor_thru_image is epic.
example (G H : Ab) (f : G ⟶ H) : epi (factor_thru_image f) := by apply_instance

-- Using this, we can build the map which is an isomorphism iff G --f--> H --g--> K is exact:
noncomputable example {G H K : Ab} (f : G ⟶ H) (g : H ⟶ K) (w : f ≫ g = 0) : image f ⟶ kernel g :=
kernel.lift g (image.ι f)
begin
apply (cancel_epi (factor_thru_image f)).1,
simp [w],
end


Kevin Buzzard (Mar 07 2020 at 14:35):

@Scott Morrison your category theory tutorials are just way too advanced for me. The kind of questions I have are of the following nature: "I have an object in Ab and as far as I can see it's a type. I have a morphism in Ab from this type to itself. How do I actually get hold of the map from the type to itself?" I need some sort of "category theory for dummies" tutorial. Every line I write takes forever when I'm using category theory.

Kevin Buzzard (Mar 07 2020 at 14:36):

Ooh I've got it :-) The morphism was a heavily-disguised add_monoid_hom.

Kevin Buzzard (Mar 07 2020 at 14:39):

My problem is that to use category theory I instantly have to know all this exotic notation with << and <<< and so on, and somehow you have to know it all at once before you can even start. I seem to have to keep category.lean and functor.lean and natural_transformation.lean open at all times just so I can have access to all the notation.

Kevin Buzzard (Mar 07 2020 at 14:58):

Maybe I should just write some basic thing and PR it.

Scott Morrison (Mar 07 2020 at 17:53):

@Kevin Buzzard, I added a basic section to the tutorial on Ab:

/-!
# Basic setup of the category of abelian groups

We demonstrate using the objects of Ab, which are bundled add_comm_group,
and the morphisms, which are add_monoid_hom (aka →+).
-/

-- We decide to work in Type 0,
-- so we can work with concrete examples like ℤ, without using ulift.
local notation Ab := Ab.{0}

-- An object of Ab is a bundled add_comm_group.
-- If an appropriate instance is available, we can use AddCommGroup.of to lift
-- a type to a bundled object.
def Z : Ab := AddCommGroup.of ℤ
def Q : Ab := AddCommGroup.of ℚ

-- There's a coercion back from Ab to Type,
-- so we can just use objects in Ab as if they were the underlying type.
example : Q := (1/3 : ℚ)
-- (Note in the next line we're using the usual function arrow,
-- not the category theory morphism arrow ⟶)
example : Z → Q := λ i, (int.cast i : ℚ)

-- Morphisms are Ab are just bundled morphisms, i.e. add_monoid_hom:
example : (Z →+ Q) = (Z ⟶ Q) := rfl
example : (Z ⟶ Q) :=
{ to_fun := λ i, (int.cast i : ℚ),
map_zero' := rfl,
-- This means we can use lemmas about add_monoid_hom when we need to:
example (f : Z ⟶ Q) (z₁ z₂ : Z) : f (z₁ + z₂) = f z₁ + f z₂ := by rw add_monoid_hom.map_add


Advice (or PRs) for further content very welcome.

Kevin Buzzard (Mar 07 2020 at 17:53):

I'm writing basic category theory docs right now, just to let you know.

Scott Morrison (Mar 07 2020 at 17:53):

Excellent! I look forward to reviewing them. :-) Thank you.

Kevin Buzzard (Mar 07 2020 at 17:54):

I haven't worked with bundled categories before -- example : (Z →+ Q) = (Z ⟶ Q) := rfl came as a pleasant surprise to me earlier today, as you probably spotted.

Scott Morrison (Mar 07 2020 at 17:58):

Curiously, I couldn't write example : (Z ⟶ Q) = (Z →+ Q) := rfl (i.e. reversing the equality), which made me sad. Somehow the elaborator made bad guesses about expected types, and failed to find the category instance for Z and Q... :-(

Kevin Buzzard (Mar 07 2020 at 18:01):

Many thanks for this. Whilst I have got on top of the basics of categories, functors and natural transformations before, I have never used bundledconcrete categories and from what Reid was saying this stuff is going to be critical (i.e. I really want to say "im f = ker g" with equality taking place in set B or subgroup B or whatever.

Kevin Buzzard (Mar 08 2020 at 18:25):

Reid Barton said:

We have R-modules already, so it should basically be a copy-and-paste job from that. Or you could define Ext :upside_down:

import category_theory.single_obj
import algebra.category.Group
import category_theory.concrete_category
import algebra.punit_instances
import G_module.basic
universe u

open category_theory

@[derive large_category]
def Group_module (G : Type u) [group G] := single_obj G ⥤ AddCommGroup.{u}

variables (G : Type u) [group G]

instance : has_coe_to_sort (Group_module G) :=
{ S := Type u, coe := λ M, M.obj unit.star }

instance Group_module.to_G_module (M : Group_module G) : G_module G M :=
{ smul := λ g m, (M.map g).to_fun m,
id := begin
intro m,
show (M.map (𝟙 _)).to_fun m = m,
rw category_theory.functor.map_id,
refl,
end,
smul_smul := λ g h m, begin
show _ = (M.map (h ≫ g)).to_fun m,
rw M.map_comp,
refl,
end,
linear := λ g m n, begin
unfold has_scalar.smul,
end }

variables (M N : Type) [add_comm_group M] [add_comm_group N] [G_module G M]
[G_module G N] (f : G_module_hom G M N)

instance : concrete_category (Group_module G) :=
{ to_category :=
{ hom   := λ M N, G_module_hom G M N,
id    := λ M, 1,
comp  := λ A B C f g, g.comp f,
},
forget := {
obj := λ M, M,
map := λ M N f, f.to_fun },
forget_faithful := { }
}

def of (M : Type u) [add_comm_group M] [G_module G M] : Group_module G :=
{ obj := λ _, AddCommGroup.of M,
map := λ _ _ g, {
to_fun := λ m, @has_scalar.smul G M _ (g : G) (m : M),
map_zero' := G_module.g_zero g,
},
map_id' := λ _, begin
intro m,
exact G_module.id G m,
end,
map_comp' := λ _ _ _ g h, begin
intro m,
exact (G_module.smul_smul h g m).symm
end
}

-- TODO: Once #1445 has merged, replace this with has_zero_object (Module R)
instance : has_zero (Group_module G) := ⟨of G punit⟩

variables (MM NN UU : Group_module G)

instance to_G_module_hom : has_coe (MM ⟶ NN) (G_module_hom G MM NN) :=
{ coe := λ f,
{ to_fun := (f.app ()).to_fun,
map_zero' := (f.app ()).map_zero,
Gmul' := λ g m, begin
dsimp,
unfold has_scalar.smul,
have h := (f.naturality g),
swap, exact (), swap, exact (),
show (MM.map g ≫ f.app ()).to_fun m = _,
rw h,
refl,
end
}
}

@[simp] lemma id_apply (m : MM) : ((𝟙 MM) : MM → MM) m = m := rfl

@[simp] lemma coe_comp (f : MM ⟶ NN) (g : NN ⟶ UU) :
((f ≫ g) : MM → UU) = g ∘ f := rfl

def hom_is_module_hom {M₁ M₂ : Group_module G} (f : M₁ ⟶ M₂) :
G_module_hom G M₁ M₂ := f


I can concrete categories! That took me a long time, and it wasn't quite as simple as it might have been because M ⟶ N is defeq to R-module homs in the R-module case, whereas the G-modules are defined as this functor category so we have to make the coercion to G-module homs explicitly (it took me a while to spot this subtlety).

The only other thing I didn't really understand was how in mathlib they get away with this. I don't understand that line. The analogous definition in the code above takes me 15 lines and I need an @ at some point.

Kevin Buzzard (Mar 08 2020 at 18:26):

OK so now I can get started with the super-important things I needed to do this weekend, at 6:25pm on Sunday evening :-/ I guess I shouldn't be doing work at weekends anyway :-)

Scott Morrison (Mar 08 2020 at 18:42):

G_module is some private thing you have?

Scott Morrison (Mar 08 2020 at 18:44):

You've done something a little strange: defined G-modules as functors from G to Ab, but then defined morphisms as some hand-rolled thing, rather than just natural transformations.

Scott Morrison (Mar 08 2020 at 18:48):

Do we have group rings in mathlib?

Johan Commelin (Mar 08 2020 at 18:53):

They are finsupp

Scott Morrison (Mar 08 2020 at 18:53):

Where is the multiplication defined?

Scott Morrison (Mar 08 2020 at 18:54):

It can't possibly be finsupp, because the only sensible multiplication there is pointwise.

Surely!?

Oh dear. :-)

Scott Morrison (Mar 08 2020 at 18:55):

Now I remember Yury proposing that we change this.

This is #1864.

What a mess.

Scott Morrison (Mar 08 2020 at 18:59):

Ugh... the convolution product which is the current notion of multiplication on finsupp assumes the domain is an additive monoid.
Are we going to have two different versions, monoid_algebra and add_monoid_algebra? I guess yes. Then we'll build polynomials on top of add_monoid_algebra, and group rings on top of monoid_algebra.

Scott Morrison (Mar 08 2020 at 19:09):

Do we know what notations we would want for monoid_algebra?

Scott Morrison (Mar 08 2020 at 19:09):

I'd love to be able to write k[G].

Scott Morrison (Mar 08 2020 at 19:11):

Actually, maybe add_monoid_algebra is an unnecessary distraction. How awkward would it be to say that polynomials over R are the group ring for the multiplicative monoid $\{t^n\}$?

Scott Morrison (Mar 08 2020 at 19:11):

It is quite unnatural to say that the monoid indexing monomials is an additive monoid.

Reid Barton (Mar 08 2020 at 19:39):

Pointwise multiplication is actually not that sensible because it is generally not unital

Reid Barton (Mar 08 2020 at 19:40):

I think finsupp (multiplicative nat) sounds fine for polynomials.

Reid Barton (Mar 08 2020 at 19:41):

I agree though that Kevin did something odd. Actually, there are two category instances in this code. One from large_category and one from concrete_category.

Reid Barton (Mar 08 2020 at 19:43):

Since you already have G_module, you could just not bother with the functor stuff.

Scott Morrison (Mar 08 2020 at 20:07):

So --- your suggestion is to ignore pointwise multiplication

Scott Morrison (Mar 08 2020 at 20:07):

but to switch the convolution product to assuming a monoid, rather than an add_monoid

Scott Morrison (Mar 08 2020 at 20:07):

and replacing nat with multiplicative nat for polynomials? (and corresponding changes for mv_polynomials)

Scott Morrison (Mar 08 2020 at 20:08):

and then we can naturally define group rings?

I think so

Kevin Buzzard (Mar 08 2020 at 20:10):

The G-module structure is from a student project. Do I not need the concrete category instance? I was just playing around without thinking

Reid Barton (Mar 08 2020 at 20:14):

I'm not sure why you would ever need it actually. Does the rest of your code work if you delete the whole instance?

Kevin Buzzard (Mar 08 2020 at 20:19):

Sorry it's not runnable by anyone else though. It's currently a fork of a student project and I'm reluctant to make it public because I want the student to do the work, not me!

Kevin Buzzard (Mar 08 2020 at 20:52):

So I guess what I was hoping to get from the concrete category construction was some way of coercing from hom sets to functions. But I think that right from the offset the definition of G-module means that the hom sets can not be defeq to functions -- but on the other hand one can use coercions. I now understand coercions sufficiently well not to be scared about this.

Scott Morrison (Mar 08 2020 at 22:22):

multiplicative nat is just a disaster. The definitional equality leaks through everywhere, and it's a mess.

Scott Morrison (Mar 08 2020 at 22:23):

At this point I think it may just be easier to define monoid_algebra and add_monoid_algebra separately. :-(

Reid Barton (Mar 08 2020 at 22:32):

Kevin, maybe by now you've worked this out but the coercion setup is not related to the concrete_category instance

Kevin Buzzard (Mar 08 2020 at 23:21):

Right -- I've remind the concrete category instance and my coercions are still working fine.

Scott Morrison (Mar 10 2020 at 06:05):

@Kevin Buzzard, I just made a draft PR showing how I'd define GroupModule as

structure GroupModule (G : Group.{u₁}) :=
(ρ : G ⟶ Group.of (Aut V))


and the obvious definitions following from that.

Mostly for discussion and comparison for now.

Mario Carneiro (Mar 10 2020 at 06:06):

oh, this is my first time hearing about draft PRs, perhaps they can replace [WIP] PRs?

Mario Carneiro (Mar 10 2020 at 06:13):

eh, on second thought, it looks to not support some basic features, and https://github.com/wip/app is a simpler alternative

Last updated: May 18 2021 at 07:19 UTC