0-over-lim: Limit-preserving functors lift

Stream: toric

[Moisés Herradón Cueto]

Hi! I'm trying to learn Lean and I thought this project looked interesting.

I was trying to prove 0-over-lim: Limit-preserving functors lift to over categories, and I think it's false as stated.

It says the following: let $J$ be a category. If a functor preserves limits of shape $J$, then the induced functor in the over categories preserves limits of shape $J$ as well.

The problem is that the shape of the limits has to change once you pass to the over category. Take, for example, $J = \{A, B\}$ to be two objects and no non-trivial morphisms. Then, a functor $J \to C$ is a choice of two objects in $C$, and the limit of such a functor is the product of two objects. On the other side, a functor from $J \to C/X$ is a diagram with three objects, and the limit of such a functor is a fibered product over $X$.

There are functors which preserve products, but not finite products. For example (****wrong example, sorry), in the category of abelian groups, the functor $M\mapsto \operatorname{Hom}({\mathbb Z/2\mathbb Z}, M)$ preserves products (direct sums), but it does not preserve the fibered product $\mathbb Z \times_{\mathbb Z/2} \mathbb Z$.

This also works as an example that PreservesFiniteProducts.overPost in CategoryTheory/Limits/Preserves/Finite.lean is false.

I haven't yet figured out what this is used for. Anyway, I would love to attempt to contribute, but my knowledge of Lean is tiny.

[Aaron Liu]

What are the morphisms in the fibered product $\mathbb{Z} \times_{\mathbb{Z}/2} \mathbb{Z}$? Sorry if this is a dumb question but I can't figure it out.
EDIT: I had my diagrams the wrong way around

[Moisés Herradón Cueto]

As I'm trying to write it out I'm realizing that my example doesn't work :face_palm: Let me try to find another one...

[Moisés Herradón Cueto]

Take $\mathbf{Ab}$ to be the category of abelian groups, and $F\colon \mathbf {Ab}\to \mathbf{Ab}$ to be the functor $F(M) = M/2M$. This preserves products.

If we consider the fibered product, both of whose factors are $\mathbb Z \xrightarrow{1\mapsto 1} \mathbb Z/2\mathbb Z$, this is the kernel of the map

$$\mathbb Z \oplus \mathbb Z \xrightarrow{(a,b)\mapsto a-b\mod 2} \mathbb Z/2\mathbb Z$$

Which I think is freely generated by $\alpha = (2,0)$ and $\beta = (1,1)$, which means that

$$\mathbb Z\times_{\mathbb Z/2\mathbb Z} \mathbb Z \cong \mathbb Z\oplus \mathbb Z$$

(Even if I got the generators wrong, it's a subgroup of a free group, so it's free, and the rank is correct) So,

$$F(\mathbb Z\times_{\mathbb Z/2\mathbb Z} \mathbb Z) \cong F(\mathbb Z\oplus \mathbb Z) \cong \mathbb Z/2\mathbb Z\times \mathbb Z/2\mathbb Z$$

And also

$$F(\mathbb Z)\times_{F(\mathbb Z/2\mathbb Z)} F(\mathbb Z) \cong \mathbb Z/2\mathbb Z \times_{\mathbb Z/2\mathbb Z} \mathbb Z/2\mathbb Z \overset{(*)}\cong \mathbb Z/2\mathbb Z$$

($(*)$ In the fibered product, all maps are the identity)

[Kevin Buzzard]

I am a bit confused by what you're saying. The claim is that if some functor preserves limits of shape J then some other functor does too. What is your functor and what is J in your proposed counterexample?

[Kevin Buzzard]

Oh I think I have it now. C=D=Ab, J= discrete two-element category, F(A)=A/2A

[Moisés Herradón Cueto]

Sorry, let me clarify all the notation. The theorem says that $C$ is a category, $X$ is an object, $F\colon C\to D$ preserves limits of shape $J$. Then, $F\colon C/X\to D/F(X)$ preserves limits of shape $J$. I'm claiming that in the conclusion, the shape should be different. In my example:

• $C=D=\mathbf {Ab}$
• $X = \mathbb Z/2\Z$
• $F (M) = M/2M$

• $J$ is a category with two objects and no morphisms between them.

• A functor $c\colon J\to C$ is the same as a choice of two objects in $C$. The limit of this functor, if it exists, is the product of these objects.

• A functor $c\colon J\to C/X$ is the same as a choice of two objects with morphisms $A\to X$ and $B\to X$. The limit is the fibered product $A\times_X B$.

[Aaron Liu]

Is $M / 2M$ the cokernel of the doubling map?

[Moisés Herradón Cueto]

Yes, or $M\otimes_{\mathbb Z} {\mathbb Z/2\mathbb Z}$, if you prefer.

[Yaël Dillies]

All we want in the end is that if F preserves finite limits then so does Over.post F. Feel free to change the statement of 0-over-lim so long as you can still prove that from it!

[Moisés Herradón Cueto]

Ohh, that's great news!

[Notification Bot]

Moisés Herradón Cueto has marked this topic as resolved.

[Yaël Dillies]

Should I assign you to the task?

[Moisés Herradón Cueto]

I'm not very confident, to be honest... And I suspect that if I do prove it, it might be really poor quality. But if it's all the same to everyone else, I'll give it a shot.

[Yaël Dillies]

It is yours :smile:

[Kevin Buzzard]

I would imagine that a limit of shape J in $C/X$ is the same as a limit of shape some (finite) modification of J in $C$, so this should hopefully be fine.

[Edward van de Meent]

i'm not sure how you would get a map from the limit in $C$ into $X$ though... i imagine the ability to do this is very dependent on the choice of $C$ and $X$...

[Edward van de Meent]

for example, imagine the poset $C := \mathbb{N} + \{\infty_1,\infty_2, \infty_3\}$ such that $\infty_1 \leq \infty_3$, all $\infty_i$ are larger than elements of $\mathbb{N}$, and $\infty_2$ is not comparable with the other infinities. then the limit of $\mathbb{N}$ in $C/\infty_3$ is $\infty_1$, but it is not clear how to recover this from a limit in $C$ (to me)

[Edward van de Meent]

since in particular, $\infty_2$ has a cone over $\mathbb{N}$ but does not factor through $\infty_1$ (EDIT: i'm confusing limits with colimits)

[Edward van de Meent]

thinking about this again, indeed if we choose shape $J + \{*\}$ and add (unique) arrows $f_j : j \rightarrow *$ for every $j \in J + \{*\}$, i imagine we get the right limit?

[Moisés Herradón Cueto]

That's my hope for sure

[Andrew Yang]

I am doubtful that we actually need this because the functor we care about is a right adjoint and this follows from the "adunction in over category" thing. But this would be a great addition into mathlib anyways.

[Andrew Yang]

The thing we want in mathlib might be:

1. If J is connected and F preserves it, then so does Over.post F.
2. If F preserves products indexed by I, then Over.post F preserves pullbacks indexed by I.

[Andrew Yang]

It would also be nice to have the colimit version. Here I think the (analogous to original) claim is true.

[Edward van de Meent]

to make the first thing concrete, does the following look good?

import Mathlib
open CategoryTheory
open Limits

example {C D J : Type*} [Category C] [Category D]
    [Category J] [IsConnected J] (F : C ⥤ D) {X : C} (K : J ⥤ Over X)
    (hF : PreservesLimit (K ⋙ Over.forget X) F) :
    PreservesLimit K (Over.post F) := by
  sorry

I could be putting the Over.forget in the wrong place

[Edward van de Meent]

alternatively, the "forall" case:

example {C D J : Type*} [Category C] [Category D] [Category J]
    [IsConnected J] (F : C ⥤ D) (X : C) (hF : PreservesLimitsOfShape J F) :
    PreservesLimitsOfShape J (Over.post (X := X) F) :=
  sorry

[Edward van de Meent]

as for the second thing:

example {C D J : Type*} [Category C] [Category D]
    (F : C ⥤ D) (X : C) (hF : PreservesLimitsOfShape (Discrete J) F) :
    PreservesLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) (Over.post (X := X) F) :=
  sorry

[Notification Bot]

Moisés Herradón Cueto has marked this topic as unresolved.

[Moisés Herradón Cueto]

I made a pull request. Like I said, I'm just learning Lean, so any and all feedback would be greatly appreciated!

[Yaël Dillies]

You were quick! Having a look :smile:

[Yaël Dillies]

I just stumbled upon docs#CategoryTheory.Over.ConstructProducts.over_product_of_widePullback, which is what you proved, but less general. We'll have to remember to remove it when we upstream your work!