# Zulip Chat Archive

## Stream: maths

### Topic: colimits in an arbitrary equational theory

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

#### Kevin Buzzard (Mar 19 2020 at 19:13):

Is it the adjoint functor theorem?

#### Kevin Buzzard (Mar 19 2020 at 19:14):

Note that this is more than one theorem

#### Chris Hughes (Mar 19 2020 at 19:14):

Maybe. What does the adjoint functor theorem say?

#### 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

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

#### 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

#### 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

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

#### Chris Hughes (Mar 19 2020 at 19:31):

But that's not true.

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

#### Kevin Buzzard (Mar 19 2020 at 19:36):

The forgetful functor from CommRing to Type probably preserves limits

#### Kevin Buzzard (Mar 19 2020 at 19:36):

so apparently it's a right adjoint

#### Kevin Buzzard (Mar 19 2020 at 19:36):

which means it has a left adjoint

#### 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

#### Chris Hughes (Mar 19 2020 at 19:37):

I see, I'm getting confused.

#### Kevin Buzzard (Mar 19 2020 at 19:37):

I'm already confused

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

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

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

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

#### 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`

#### Chris Hughes (Mar 19 2020 at 19:41):

But I couldn't do that with say integral domains

#### 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`

#### Chris Hughes (Mar 19 2020 at 19:43):

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

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

#### orlando (Mar 19 2020 at 19:48):

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

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

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

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

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

#### 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 $g$ and $g^{-1}$ and define multiplication by "multiply and then cancel" then associativity is going to be painful.

#### orlando (Mar 19 2020 at 20:26):

Kevin : Yes it's ok ... the same is true for the forgetful forget $A-\text{Alg} \to \text{Set}$ ... with the polynomial $A$-algebra $A[X_S]$ ! I thinck the property of $F$ preserve limit tell us (for example) that $\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]$

#### Johan Commelin (Mar 19 2020 at 20:41):

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

#### orlando (Mar 19 2020 at 20:49):

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

#### 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)

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

#### Kevin Buzzard (Mar 19 2020 at 20:51):

The forgetful functor to set preserves filtered colimits I guess.

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

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

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

#### 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)

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

#### 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

#### 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

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

#### 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

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

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

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

#### 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