colimits in an arbitrary equational theory

Stream: maths

[Chris Hughes]

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

Is it the adjoint functor theorem?

[Kevin Buzzard]

Note that this is more than one theorem

[Chris Hughes]

Maybe. What does the adjoint functor theorem say?

[Kevin Buzzard]

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]

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]

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]

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]

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]

But that's not true.

[Chris Hughes]

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

[Kevin Buzzard]

The forgetful functor from CommRing to Type probably preserves limits

[Kevin Buzzard]

so apparently it's a right adjoint

[Kevin Buzzard]

which means it has a left adjoint

[Kevin Buzzard]

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

[Chris Hughes]

I see, I'm getting confused.

[Kevin Buzzard]

I'm already confused

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Chris Hughes]

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]

But I couldn't do that with say integral domains

[Chris Hughes]

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

[Chris Hughes]

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

[Chris Hughes]

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]

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

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[orlando]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

The forgetful functor to set preserves filtered colimits I guess.

[Chris Hughes]

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]

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

[Chris Hughes]

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

[Mario Carneiro]

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

[Chris Hughes]

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

[Kevin Buzzard]

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

[Bhavik Mehta]

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]

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]

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]

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

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]

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]

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.