Zulip Chat Archive

Stream: maths

Topic: issue with bundled subgroups


view this post on Zulip 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₂],
    (G₁ →+ G₂) → add_subgroup G₂ → add_subgroup G₁
-/

def ker' (f : add_group_hom G H) : add_subgroup G := f.comap f  -- fails:
/-
invalid field notation, function 'add_group_hom.comap'
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?

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

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

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

view this post on Zulip Chris Hughes (Mar 06 2020 at 18:02):

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

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 18:06):

Well let's talk about images?

view this post on Zulip 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:ABf:A\to B is a morphism of abelian additive groups and we have A0AA_0\subseteq A and B0BB_0\subseteq B subgroups with f(A0)B0f(A_0)\subseteq B_0 then we get an induced map A/A0B/B0A/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.

view this post on Zulip Chris Hughes (Mar 06 2020 at 18:11):

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:15):

Have you considered just using the category AddCommGroup?

view this post on Zulip Reid Barton (Mar 06 2020 at 18:16):

Your fingers will thank you

view this post on Zulip Reid Barton (Mar 06 2020 at 18:16):

Probably a bug that it isn't called Ab

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:22):

You don't actually need any infrastructure

view this post on Zulip Reid Barton (Mar 06 2020 at 18:22):

I don't really get this perception

view this post on Zulip Reid Barton (Mar 06 2020 at 18:23):

It's literally just bundling groups and bundling morphisms

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:26):

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

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:29):

I assume the second part means: defining the differentials

view this post on Zulip 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 d2=0d^2=0

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 18:30):

and that d is an add_monoid_hom.

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 18:31):

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:31):

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

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 18:32):

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

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:33):

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 18:33):

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:34):

yep, so you can compare https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/topological_spaces/subspace.lean

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

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 18:38):

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

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

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

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 18:40):

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:40):

(thanks Johan)

view this post on Zulip Johan Commelin (Mar 06 2020 at 18:40):

I didn't do the snake lemma...

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 18:41):

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

view this post on Zulip Johan Commelin (Mar 06 2020 at 18:41):

I guess that will be on the wishlist sometime soon.

view this post on Zulip Reid Barton (Mar 06 2020 at 18:41):

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

view this post on Zulip Johan Commelin (Mar 06 2020 at 18:41):

Yeah, the good old times :rolling_on_the_floor_laughing:

view this post on Zulip Reid Barton (Mar 06 2020 at 18:43):

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 18:44):

Oh maybe im := map and range = map univ

view this post on Zulip Reid Barton (Mar 06 2020 at 18:44):

map I don't even know what it is.

view this post on Zulip Reid Barton (Mar 06 2020 at 18:45):

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

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:49):

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:49):

How else are you going to state this fact?

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:50):

I see

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 18:50):

:-)

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

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

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 18:53):

G-modules and G-module maps

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:54):

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:54):

in that sense

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:54):

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 18:55):

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:55):

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

view this post on Zulip Reid Barton (Mar 06 2020 at 18:56):

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

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

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

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

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

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

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:00):

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

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:02):

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:06):

Okay, so looking at

/-- A->B->C -/
def is_exact {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] : 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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:06):

or to +-homomorphisms now or whatever

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 19:08):

Will the range really equal the ker here?

view this post on Zulip Reid Barton (Mar 06 2020 at 19:09):

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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:09):

I mean the same range as now

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 19:09):

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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:09):

I also had that realization

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

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

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:14):

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:15):

I see

view this post on Zulip Reid Barton (Mar 06 2020 at 19:15):

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

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

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 19:17):

Is singular cohomology formalised in any theorem prover at all?

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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:18):

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

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:20):

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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:21):

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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:24):

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 19:31):

Aah but that's singular homology ;-)

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

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 19:38):

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:40):

or is the point you only consider discrete modules?

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

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 19:42):

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

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 19:43):

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

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

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 19:46):

Like a limit over the finite quotients of the group?

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 19:46):

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 19:47):

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 19:47):

and this is fine for discrete modules.

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 19:48):

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 20:33):

The second one is just normal behavior of instances

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

view this post on Zulip Reid Barton (Mar 06 2020 at 20:36):

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

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

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

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 20:49):

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

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

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

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

view this post on Zulip Johan Commelin (Mar 06 2020 at 21:49):

Scott Morrison said:

-- TODO no images yet...

This.

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 21:50):

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

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

view this post on Zulip Reid Barton (Mar 06 2020 at 22:03):

What does kernel f end up being in this case?

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

view this post on Zulip Scott Morrison (Mar 06 2020 at 22:28):

Use the API. :-)

view this post on Zulip Scott Morrison (Mar 06 2020 at 22:28):

And don't look under the hood.

view this post on Zulip Scott Morrison (Mar 06 2020 at 22:29):

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

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

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

view this post on Zulip Scott Morrison (Mar 07 2020 at 00:09):

Yes, that sounds reasonable.

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

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

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 14:36):

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

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

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 14:58):

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

view this post on Zulip 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,
  map_add' := int.cast_add, }
-- 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.

view this post on Zulip Kevin Buzzard (Mar 07 2020 at 17:53):

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

view this post on Zulip Scott Morrison (Mar 07 2020 at 17:53):

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

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

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

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

view this post on Zulip 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,
    exact add_monoid_hom.map_add _ _ _
  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_add' := G_module.linear g
  },
  map_id' := λ _, begin
    apply add_monoid_hom.ext,
    intro m,
    exact G_module.id G m,
  end,
  map_comp' := λ _ _ _ g h, begin
    apply add_monoid_hom.ext,
    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,
    map_add' := (f.app ()).map_add,
    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.

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

view this post on Zulip Scott Morrison (Mar 08 2020 at 18:42):

G_module is some private thing you have?

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

view this post on Zulip Scott Morrison (Mar 08 2020 at 18:48):

Do we have group rings in mathlib?

view this post on Zulip Johan Commelin (Mar 08 2020 at 18:53):

They are finsupp

view this post on Zulip Scott Morrison (Mar 08 2020 at 18:53):

Where is the multiplication defined?

view this post on Zulip Scott Morrison (Mar 08 2020 at 18:54):

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

view this post on Zulip Scott Morrison (Mar 08 2020 at 18:54):

Surely!?

view this post on Zulip Scott Morrison (Mar 08 2020 at 18:55):

Oh dear. :-)

view this post on Zulip Scott Morrison (Mar 08 2020 at 18:55):

Now I remember Yury proposing that we change this.

view this post on Zulip Scott Morrison (Mar 08 2020 at 18:56):

This is #1864.

view this post on Zulip Scott Morrison (Mar 08 2020 at 18:56):

What a mess.

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

view this post on Zulip Scott Morrison (Mar 08 2020 at 19:09):

Do we know what notations we would want for monoid_algebra?

view this post on Zulip Scott Morrison (Mar 08 2020 at 19:09):

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

view this post on Zulip 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 {tn}\{t^n\}?

view this post on Zulip Scott Morrison (Mar 08 2020 at 19:11):

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

view this post on Zulip Reid Barton (Mar 08 2020 at 19:39):

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

view this post on Zulip Reid Barton (Mar 08 2020 at 19:40):

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

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

view this post on Zulip Reid Barton (Mar 08 2020 at 19:43):

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

view this post on Zulip Scott Morrison (Mar 08 2020 at 20:07):

So --- your suggestion is to ignore pointwise multiplication

view this post on Zulip Scott Morrison (Mar 08 2020 at 20:07):

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

view this post on Zulip Scott Morrison (Mar 08 2020 at 20:07):

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

view this post on Zulip Scott Morrison (Mar 08 2020 at 20:08):

and then we can naturally define group rings?

view this post on Zulip Reid Barton (Mar 08 2020 at 20:09):

I think so

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

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 23:21):

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

view this post on Zulip 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₁}) :=
(V : AddCommGroup.{u₁})
(ρ : G  Group.of (Aut V))

and the obvious definitions following from that.

Mostly for discussion and comparison for now.

view this post on Zulip Mario Carneiro (Mar 10 2020 at 06:06):

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

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