Zulip Chat Archive

Stream: maths

Topic: colimits in an arbitrary equational theory


view this post on Zulip Chris Hughes (Mar 19 2020 at 19:12):

@Reid Barton was talking about potentially proving existence and properties of colimits in arbitrary "equational theories", which means that this stuff wouldn't have to be proved for each category individually. An important theorem is the theorem that the forgetful functor to Set preserves directed colimits.

What is the general theorem that would give me the existence of things like colimits, but also free groups, rings etc. in these categories. Is it possible to have automation that would just prove the existence of something random like the free ring over an abelian group?

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

Is it the adjoint functor theorem?

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

Note that this is more than one theorem

view this post on Zulip Chris Hughes (Mar 19 2020 at 19:14):

Maybe. What does the adjoint functor theorem say?

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

It says that under certain conditions, a functor has an adjoint, and when you apply it to the forgetful functor from Group to Set, the adjoint is the functor which sends a set to the free group on that set

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

although IIRC not every version of the adjoint functor theorem applies to that functor, because Group doesn't have a small generating set or something.

view this post on Zulip Chris Hughes (Mar 19 2020 at 19:17):

I have just read nlab very briefly. The condition is for being an adjoint, not for having an adjoint right? Or are these the same. Given a functor, I want to construct the adjoint, not just show the a functor I already have is the adjoint

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

Yeah I think these are the same. "the adjoint" of a functor actually means that you have two functors F and G, and F is a left adjoint of G and G is a right adjoint of F

view this post on Zulip Chris Hughes (Mar 19 2020 at 19:31):

So I guess there is a theorem there to prove that all the forgetful functors between algebraic structures preserve colimits, and some other conditions that I don't properly understand. And then you can apply the adjoint functor theorem.

view this post on Zulip Chris Hughes (Mar 19 2020 at 19:31):

But that's not true.

view this post on Zulip Chris Hughes (Mar 19 2020 at 19:34):

For it to apply doesn't the forgetful functor from say CommRing to Type need to preserve colimits? Which it doesn't.

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

The forgetful functor from CommRing to Type probably preserves limits

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

so apparently it's a right adjoint

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

which means it has a left adjoint

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

and this gives us a functor F from Type to CommRing which has some property which I'll have to look up

view this post on Zulip Chris Hughes (Mar 19 2020 at 19:37):

I see, I'm getting confused.

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

I'm already confused

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

So this might mean Hom_{ring}(F(S),R)=Hom_{set}(S,R)

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

where R is a ring which is regarded as a set on the RHS

view this post on Zulip Chris Hughes (Mar 19 2020 at 19:41):

For me, it's "obvious" that a free group exists, because if I look at the axioms for a group, I can make them into an inductive relation in the way colimits are constructed in algebra/category/Group/colimits

view this post on Zulip Chris Hughes (Mar 19 2020 at 19:41):

But I couldn't do that with say integral domains

view this post on Zulip Chris Hughes (Mar 19 2020 at 19:42):

Because I can't make a constructor for zero_ne_one, or eq_zero_or_eq_zero_of_mul_eq_zero

view this post on Zulip Chris Hughes (Mar 19 2020 at 19:43):

Does this have something to do with limits not being preserved or something?

view this post on Zulip Chris Hughes (Mar 19 2020 at 19:46):

What's the correct generality for the theorem that says the forgetful functor from Group or CommRing or Module to Set preserves directed colimits?

view this post on Zulip orlando (Mar 19 2020 at 19:48):

@Kevin Buzzard your fonctor FF, it is not le polynomial Ring in variable (xs)sS(x_s)_{s \in S}. If i take S={1,2}S = \{1, 2\}, HomRing(Z[x1,x2],R)=HomSet(S,R)\text{Hom}_{\text{Ring}}(\Z[x_1,x_2],R) = \text{Hom}_{\text{Set}}(S,R), the universal property of ...

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

I don't know how to use the adjoint functor theorem. I can believe that I've used it the wrong way.

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 20:00):

Oh but this looks OK doesn't it? my F(S) seems to be the free Z-algebra on S?

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

Chris Hughes said:

For me, it's "obvious" that a free group exists, because if I look at the axioms for a group, I can make them into an inductive relation in the way colimits are constructed in algebra/category/Group/colimits

This might be the proof of the adjoint functor theorem in some sense. Maybe @Scott Morrison or @Reid Barton know what's going on?

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

I think we have to hope for @Reid Barton. My limited understanding of adjoint functor theorems does not look like this.

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 20:22):

Yeah this is a very cool piece of Lean code isn't it. I am pretty sure that it's fairly universally believed amongst mathematicians that the existence of free groups has some content because if you just look at strings of gg and g1g^{-1} and define multiplication by "multiply and then cancel" then associativity is going to be painful.

view this post on Zulip orlando (Mar 19 2020 at 20:26):

Kevin : Yes it's ok ... the same is true for the forgetful forget AAlgSetA-\text{Alg} \to \text{Set} ... with the polynomial AA-algebra A[XS]A[X_S] ! I thinck the property of FF preserve limit tell us (for example) that Z[x1,x2,x3,x4]Z[x1,x2]Z[x1,x2,x5,x6]=Z[x1,x2,x3,x4,x5,x6]\mathbb{Z}[x_1,x_2,x_3,x_4] \otimes_{\mathbb{Z}[x_1,x_2]} \mathbb{Z}[x_1,x_2,x_5,x_6] = \mathbb{\Z}[x_1,x_2,x_3,x_4,x_5,x_6]

view this post on Zulip Johan Commelin (Mar 19 2020 at 20:41):

@orlando That's right. (But I think you mean "preserve colimit".)

view this post on Zulip orlando (Mar 19 2020 at 20:49):

Ok ... i flip limit and co-limit !!!! Thx !

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 20:50):

Right -- the forgetful functor preserves limits (because to make a categorical product of rings you put a ring structure on the product of the underlying sets, and...probably something about subsets) and the free functor preserves colimits (a special case of which is precisely Orlando's statement)

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 20:51):

So integral domains and fields etc aren't equational theories I guess, and neither are topological spaces I suppose.

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 20:51):

The forgetful functor to set preserves filtered colimits I guess.

view this post on Zulip Chris Hughes (Mar 20 2020 at 01:43):

Kevin Buzzard said:

Chris Hughes said:

For me, it's "obvious" that a free group exists, because if I look at the axioms for a group, I can make them into an inductive relation in the way colimits are constructed in algebra/category/Group/colimits

This might be the proof of the adjoint functor theorem in some sense. Maybe Scott Morrison or Reid Barton know what's going on?

I think the thing about inductive relations is essentially the statement that the forgetful functor from Group to [has_one] [has_mul] [has_inv] is a right adjoint.

view this post on Zulip Chris Hughes (Mar 20 2020 at 01:52):

So maybe the general theorem is that in equational theories, forgetting axioms is always a right adjoint functor.

view this post on Zulip Chris Hughes (Mar 20 2020 at 01:57):

And then maybe you can combine it with theorems about adjoints and products of categories, to get things like monoid algebras.

view this post on Zulip Mario Carneiro (Mar 20 2020 at 01:59):

I think this generalizes to universal algebras or varieties (anything with operations and equations but not disequalities like in a field)

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

Which is what you'd expect because there's no such thing as the free field over a ring or something.

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 07:03):

The integers has a map to all fields and there's no initial object in the category of fields

view this post on Zulip Bhavik Mehta (Mar 21 2020 at 14:34):

To me this feels reminiscent of classifying toposes of algebraic (or other sorts) of theory (eg see this nlab article), I will think more about this

view this post on Zulip Thomas Read (Mar 21 2020 at 16:15):

For existence of free things, I think you generally want to show that the category of say groups is (equivalent to) the category of algebras for a monad. In particular this holds for any algebraic theory that comes from a Lawvere theory / equational theory / operad / basically any universal algebra thing.

In this case we call the forgetful functor monadic.

Now there's a theorem that a monadic functor U : A -> C creates any limits that C has, and any colimits that C has and the monad and its square preserve (see http://www.math.jhu.edu/~eriehl/context.pdf p.180). In particular if the monad is finitary (preserves filtered colimits) then U will also preserve filtered colimits - and it turns out that the monad you get from a Lawvere theory / equational theory / any appropriately finite universal algebra thing is finitary. The same thing probably holds for directed colimits, though I'm a bit confused about when you can substitute filtered and directed.

This should deal with most of what you want to know about the forgetful functor to Set. I don't know as much about forgetful functors between other categories. In the case of the free ring over an abelian group you can use the fact that rings are monoids in the category of abelian groups, and so the forgetful functor Ring -> AbGrp is monadic. This stuff is related to the theory of distributive laws. I don't know if you can always get something like that by dropping axioms from an equational theory though.

view this post on Zulip Bhavik Mehta (Mar 21 2020 at 16:25):

We have that monadic functors creates limits, and we almost have that they create any colimits that the monad preserves in mathlib already

view this post on Zulip Scott Morrison (Mar 21 2020 at 19:51):

@Bhavik Mehta, do you think you could put together a TODO list of the facts we need? What new design do we need? We still don't have anthing about filtered colimits, or finitary monads. I guess we would need to decide which of "Lawvere theory / equational theory / any appropriately finite universal algebra thing" is appropriate.

view this post on Zulip Bhavik Mehta (Mar 21 2020 at 20:06):

I think so but I'm not entirely sure I'm the best person for this - can people suggest what exactly the end goal here would be? The forgetful functor of algebraic theories preserves directed/filtered colimits and has a left adjoint?

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

The end goal is producing actual has_colimit instances on categories that algebraists want to use, with a minimum of effort per category, and a maximum of "it's definitionally what you would expect". :-)

view this post on Zulip Thomas Read (Mar 21 2020 at 22:04):

One slightly different path that's worth considering is that if U : A -> C is monadic and C is cocomplete (e.g. Set) then to show A is cocomplete you just need to show that A has coequalizers. This will get you coproducts that are definitionally fairly sensible.

The finitary monad approach (at least by the proof I know) will get you coequalizers which are definitionally absolutely horrendous, so it's only likely to be worthwhile if explicitly constructing coequalizers is pretty hard for the category in question.


Last updated: May 11 2021 at 17:39 UTC