issue with bundled subgroups

Stream: maths

[Kevin Buzzard]

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

[Chris Hughes]

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]

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]

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]

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

[Chris Hughes]

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]

Well let's talk about images?

[Kevin Buzzard]

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]

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

[Reid Barton]

Have you considered just using the category AddCommGroup?

[Reid Barton]

Your fingers will thank you

[Reid Barton]

Probably a bug that it isn't called Ab

[Kevin Buzzard]

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]

You don't actually need any infrastructure

[Reid Barton]

I don't really get this perception

[Reid Barton]

It's literally just bundling groups and bundling morphisms

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

I assume the second part means: defining the differentials

[Kevin Buzzard]

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]

and that d is an add_monoid_hom.

[Kevin Buzzard]

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]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Reid Barton]

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]

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]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

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

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

(thanks Johan)

[Johan Commelin]

I didn't do the snake lemma...

[Kevin Buzzard]

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

[Johan Commelin]

I guess that will be on the wishlist sometime soon.

[Reid Barton]

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

[Johan Commelin]

Yeah, the good old times :rolling_on_the_floor_laughing:

[Reid Barton]

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

[Kevin Buzzard]

Oh maybe im := map and range = map univ

[Reid Barton]

map I don't even know what it is.

[Reid Barton]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

How else are you going to state this fact?

[Kevin Buzzard]

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

[Reid Barton]

I see

[Kevin Buzzard]

:-)

[Kevin Buzzard]

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]

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]

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]

G-modules and G-module maps

[Kevin Buzzard]

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

[Reid Barton]

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

[Reid Barton]

in that sense

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

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]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

or to +-homomorphisms now or whatever

[Kevin Buzzard]

Will the range really equal the ker here?

[Reid Barton]

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

[Reid Barton]

I mean the same range as now

[Kevin Buzzard]

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

[Reid Barton]

I also had that realization

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Reid Barton]

I see

[Reid Barton]

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

[Kevin Buzzard]

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]

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]

Is singular cohomology formalised in any theorem prover at all?

[Reid Barton]

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]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

Aah but that's singular homology ;-)

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

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

or is the point you only consider discrete modules?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

Like a limit over the finite quotients of the group?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and this is fine for discrete modules.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

The second one is just normal behavior of instances

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

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]

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]

Scott Morrison said:

-- TODO no images yet...

This.

[Kevin Buzzard]

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

[Scott Morrison]

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

[Reid Barton]

What does kernel f end up being in this case?

[Scott Morrison]

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. :-)

[Scott Morrison]

Use the API. :-)

[Scott Morrison]

And don't look under the hood.

[Scott Morrison]

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

[Reid Barton]

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]

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

[Scott Morrison]

Yes, that sounds reasonable.

[Scott Morrison]

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]

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

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

[Kevin Buzzard]

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]

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

[Scott Morrison]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Kevin Buzzard]

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]

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]

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]

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.

[Kevin Buzzard]

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]

G_module is some private thing you have?

[Scott Morrison]

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]

Do we have group rings in mathlib?

[Johan Commelin]

They are finsupp

[Scott Morrison]

Where is the multiplication defined?

[Scott Morrison]

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

[Scott Morrison]

Surely!?

[Scott Morrison]

Oh dear. :-)

[Scott Morrison]

Now I remember Yury proposing that we change this.

[Scott Morrison]

This is #1864.

[Scott Morrison]

What a mess.

[Scott Morrison]

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]

Do we know what notations we would want for monoid_algebra?

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Scott Morrison]

So --- your suggestion is to ignore pointwise multiplication

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

and then we can naturally define group rings?

[Reid Barton]

I think so

[Kevin Buzzard]

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]

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]

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]

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]

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

[Scott Morrison]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

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