preserve filtered colimits

Stream: maths

[Scott Morrison]

I've been trying to show that forget CommRing preserves filtered colimits (as this is something now blocking schemes).

I'm completely stuck, however, on the following lemma:

lemma filtered_exact [is_filtered J] (F : J ⥤ CommRing.{v}) {jx jy : J} {x : F.obj jx} {y : F.obj jy}
  (w : quot.mk (relation F) (of jx x) = quot.mk _ (of jy y)) :
  ∃ (j : J) (ix : jx ⟶ j) (iy : jy ⟶ j), F.map ix x = F.map iy y :=
begin

end

at branch#preserves_filtered_colimits

Here of is building the big inductive type we use to build colimits, and relation F is the relation on it.

I want to do something like:

1. generalize one side of w
2. use quot.exact to get an eqv_gen (relation F) hypothesis
3. do induction on that, obtaining a huge case base.

I don't mind having to do a big case bash: I'd just like to get to the point I can start. All my attempts to generalize and/or induct so far quickly lose the connection with the x and y terms.

[Scott Morrison]

@Reid Barton, any suggestions? It this or similar something you did previously when you were looking at filtered colimits? I don't remember seeing this.

[Adam Topaz]

(@Scott Morrison The period at the end of the branch link breaks the link.)

[Reid Barton]

I don't remember proving anything like this.

[Reid Barton]

I think I understand your problem. It might be worth keeping in mind that the fact that comm_ring only has finitary operations is required for this to be true.

[Scott Morrison]

Yes.

[Scott Morrison]

(I should have done the Mon case instead, if I knew I was going to need to ask for help, just to keep the clutter down.)

[Reid Barton]

Maybe you would need to generalize to something like: for any two terms in the free algebra that become equal in the quotient, there's some j : J and a bunch of maps to it from all the places where the ofs live, such that if you map all those guys forward to j, the two terms are already equal there.

[Reid Barton]

Which sounds pretty dreadful

[Reid Barton]

Another approach that might be easier would be to instead put a ring structure on the Set-colimit and prove it has the right universal property

[Scott Morrison]

That does sound rather more pleasant, I guess. (Now that you say it I think I've tried that before... I guess time for another go.)

[Reid Barton]

I think there is or was a direct construction of most of this in the algebra library

[Adam Topaz]

Reid Barton said:

Another approach that might be easier would be to instead put a ring structure on the Set-colimit and prove it has the right universal property

I think the law of "conservation of work" will apply here :-/

[Adam Topaz]

I want to try out the lemma from this branch, but I'm just waiting for the oleans to be available.

[Reid Barton]

can you get away with directed instead of filtered, btw? Should be okay for now right?

[Adam Topaz]

Yeah that should be fine for sheaves on topological spaces

[Scott Morrison]

yes

[Reid Barton]

Reid Barton said:

I think there is or was a direct construction of most of this in the algebra library

oh no I'm wrong, it was always using the free ring-style construction even though it assumed directedness

[Reid Barton]

oh but actually it might prove the result you wanted originally

[Reid Barton]

docs#ring.direct_limit.of.zero_exact

[Reid Barton]

The docstring should say "some bigger ring" not "some bigger module"

[Reid Barton]

It looks like Kenny used the argument I was sketching

lemma of.zero_exact_aux {x : free_comm_ring Σ i, G i} (H : ideal.quotient.mk _ x = (0 : direct_limit G f)) :
  ∃ j s, ∃ H : (∀ k : Σ i, G i, k ∈ s → k.1 ≤ j), is_supported x s ∧
    lift (λ ix : s, f ix.1.1 j (H ix ix.2) ix.1.2) (restriction s x) = (0 : G j) :=

[Adam Topaz]

So here's a gigantic case-by-case start:

lemma filtered_exact [is_filtered J] {jx jy : J} {x : F.obj jx} {y : F.obj jy}
  (w : quot.mk (relation F) (of jx x) = quot.mk _ (of jy y)) :
  ∃ (j : J) (ix : jx ⟶ j) (iy : jy ⟶ j), F.map ix x = F.map iy y :=
begin
  replace w := quot.exact _ w,
  cases w,
  cases w_a,
  repeat {sorry}
end

[Reid Barton]

won't this generate subgoals involving stuff to which the inductive hypothesis won't apply?

[Scott Morrison]

yeah... look at the third goal, for example

[Scott Morrison]

because you're using cases, not induction, you've got nothing to work with there

[Reid Barton]

but even using induction won't work, because you'll get relations between stuff not of the form of jz z

[Scott Morrison]

yes, hence the idea to somehow generalize one side...?

[Scott Morrison]

but I don't see it.

[Reid Barton]

Basically you need to do what Kenny did

[Reid Barton]

I think the viable options are to reuse Kenny's construction, or build the ring structure on the Set-colimit (I really think this is a lot easier if you're going to build from scratch, but maybe just because I am bad at finset)

[Reid Barton]

For the latter it might be a good idea to prove first that $X \mapsto X \times X$ (and $X \mapsto *$) preserves filtered colimits

[Reid Barton]

Then I feel like the rest is just a series of diagram chases

[Adam Topaz]

Would it perhaps make sense to replace relation.map by this:

| map : Π (jx jy j : J) (x : F.obj jx) (y : F.obj jy) (ix : jx ⟶ j) (iy : jy ⟶ j),
    relation (of _ (F.map ix x)) (of _ (F.map iy y)) → relation (of jx x) (of jy y)

[Adam Topaz]

Okay, I think I have something working... what's the easiest way to obtain a common j with maps jx \hom j and jy \hom j given jx jy : J and is_filtered J ? found it: is_filtered_or_empty.cocone_objs.

[Adam Topaz]

Oh no! I ran into a point where I have to prove that prequotient.ofis injective. That's unprovable right?

[Scott Morrison]

No, rather there should be an automatically generated lemma for it.

[Scott Morrison]

prequotient.of.inj

[Adam Topaz]

@Scott Morrison I tried doing something like this:

lemma filtered_exact [is_filtered J] (a b : prequotient F) (w : relation F a b) :
  Π (jx jy : J) (x : F.obj jx) (y : F.obj jy),
  a = of jx x → b = of jy y →
  (∃ (j : J) (ix : jx ⟶ j) (iy : jy ⟶ j), F.map ix x = F.map iy y) :=
begin
  induction w,
  sorry
end

At least the induction gets started this way.

[Scott Morrison]

That lemma does seem provable. But can we actually deduce the lemma I was after from it?

[Adam Topaz]

I haven't tried. I didn't have much time for lean today.

[Scott Morrison]

I think it may be. There's actually something pretty stupid going on in the construction of colimits here --- we go to all the effort of making relation F an equivalence relation, and then use quot instead of quotient.

[Scott Morrison]

oh, this isn't a problem in the construction, just in the lemmas I'm trying to prove now. maybe not a big deal

[Adam Topaz]

It's possible to just get rid of refl, symm and trans in the definition of relation

[Adam Topaz]

It is strange that quot.mk is used sometimes as opposed to quotient.mk, given that there is a setoid around

[Scott Morrison]

Renaming your filtered_exact to filtered_exact', the original filtered_exact is indeed provable from it:

lemma filtered_exact [is_filtered J] (F : J ⥤ CommRing.{v}) {jx jy : J} {x : F.obj jx} {y : F.obj jy}
  (w : quotient.mk (of jx x) = quotient.mk (of jy y)) :
  ∃ (j : J) (ix : jx ⟶ j) (iy : jy ⟶ j), F.map ix x = F.map iy y :=
begin
  cases quotient.exact w with _ _ _ h _ tz _ h₁ h₂,
  { apply filtered_exact' F (relation.refl _) _ _ rfl rfl, },
  { let h := relation.symm _ _ h,
    apply filtered_exact' F h _ _ rfl rfl, },
  { let h := relation.trans _ _ _ h₁ h₂,
    apply filtered_exact' F h _ _ rfl rfl, },
  { exact filtered_exact' F _x ((F.map f) y) y rfl rfl, },
end

[Scott Morrison]

Ah, no, but the trans case of your lemma is simply not provable. I don't think this is going to work.

[Adam Topaz]

What of we get rid of trans from relation?

[Adam Topaz]

And just never define a setoid?

[Adam Topaz]

(same with symm and refl)

[Adam Topaz]

This would be a hack anyway... There must be a better way!

[Scott Morrison]

I don't think that the setoid business is an issue.

[Scott Morrison]

You have a choice whether you deal with transitivity as a case of the relation, or as a case of eqv_gen if you decide not to use a setoid.

[Scott Morrison]

@Reid Barton or @Bhavik Mehta, I can prove the diagonal functor preserves filtered colimits. But could you sketch out for me a bit more detail how you thought that would be useful defining a ring structure on the type level colimit?

[Scott Morrison]

Oh, I see, multiplication gives a natural transformation F ⋙ Δ ⟶ F, and we can take the induced map on colimits, and since Δ preserves filtered colimits, we can turn that into a morphism Δ (colimit F) ⟶ colimit F, which is what we wanted.

[Scott Morrison]

I can use this to construct one and mul quite slickly on the type level colimit, but so far my efforts to check the axioms just result in big messes. :-(

[Reid Barton]

Now you should prove that, say, $X \mapsto X \times X \times X$ also preserves filtered colimits and therefore any axiom involving 3 variables follows from the fact that, by construction, the maps to the colimit preserve the addition and multiplication you just defined.

[Reid Barton]

That is, if we switch to a more comfortable notation denoting a typical input ring as $R_i$ and their colimit in Set as $R$, you've constructed addition on $R$ as the map $R \times R \to R$ such that the squares formed together with $R_i \times R_i \to R_i$ commute, and similarly for multiplication. In other words, each map $R_i \to R$ now preserves $+$ and $*$.

[Reid Barton]

Now, suppose we want to prove that say $a * (b + c) = a * b + a * c$ is satisfied in $R$. Look at the diagram formed by the maps $(a, b, c) \mapsto a * (b + c) : R_i \times R_i \times R_i \to R_i$. Because the maps $R_i \to R$ preserve addition and multiplication, we can extend this diagram to include the corresponding map $R \times R \times R \to R$.

[Reid Barton]

If we instead used the expression $a * b + a * c$, we'd get the same maps for all the $R_i$, of course, and a priori a different map $R \times R \times R \to R$, but we can conclude that they're actually equal because there's only one map that fits there by the universal property of the colimit.

[Reid Barton]

The same kind of argument will appear later when you want to verify the universal property, whicih amounts to showing that the map you get from the universal property in Set is also a ring homomorphism.

[Adam Topaz]

I'm a bit confused as to how this solves the original issue of proving the filtered_exact lemma from before. It seems that one would just have to prove a similar lemma for colimits in the category Type* (which is certainly a sensible thing to do), and it seems to me that this would have similar issues with getting the induction right. That is unless mathlib already has an analogue of filtered_exact for colimits in Type*?

[Adam Topaz]

Also, with this formulation it feels like we should just define sheaves of rings to be internal ring objects in the category of sheaves of sets.

[Reid Barton]

The point is that in Set, any element of a colimit (even one that isn't filtered) is actually of the form of _

[Reid Barton]

and so the corresponding fact for Set is very easy

[Adam Topaz]

Well, we already know this for colimits (in the filtered case) in CRing from of_surjective which is a lemma in the file that Scott was working with.

[Adam Topaz]

Ok, I think I see why it is easier in the Type*. The point is that we would define the relation whose quotient is the colimit directly on the disjoint union of the components, as opposed to working with an auxiliary prequotient type.

[Adam Topaz]

And yes I agree the induction would be much smoother.

[Reid Barton]

Hmm, it's possible you could use the surjectivity somehow, but it's not clear to me. The relations are also more complicated, involving multiple variables.

[Adam Topaz]

I might be misunderstanding the root of the issue, but it seems to be coming from using this auxiliary prequotient thing.

[Adam Topaz]

Ha, I guess there is not induction at all in the case of Type*:

import category_theory.limits.limits
import category_theory.limits.types

universes u v

open category_theory
open category_theory.limits

variables {J : Type v} [small_category J] (F : J ⥤ Type u)

namespace colimit
def relation : (Σ (j : J), F.obj j) → (Σ (j : J), F.obj j) → Prop :=
  λ ⟨j₁,x₁⟩ ⟨j₂,x₂⟩, ∃ (i : j₁ ⟶ j₂), F.map i x₁ = x₂
end colimit

def colimit := quot (colimit.relation F)

I think that's the right construction?

[Adam Topaz]

Okay, it works for colimits of types :)

import category_theory.limits.limits
import category_theory.limits.types

universes u v

open category_theory
open category_theory.limits

variables {J : Type v} [small_category J] (F : J ⥤ Type u)

namespace colimit
@[reducible]
def relation : (Σ (j : J), F.obj j) → (Σ (j : J), F.obj j) → Prop :=
  λ x y, ∃ (i : x.1 ⟶ y.1), F.map i x.2 = y.2
end colimit

def colimit := quot (colimit.relation F)

lemma filtered_exact [is_filtered J] (x y : Σ (j : J), F.obj j)
  (h : quot.mk (colimit.relation F) x = quot.mk (colimit.relation F) y) :
  (∃ (j : J) (i1 : x.1 ⟶ j) (i2 : y.1 ⟶ j), F.map i1 x.2 = F.map i2 y.2) :=
begin
  cases x with j1 x,
  cases y with j2 y,
  replace h := quot.exact _ h,
  induction h,
  { cases h_a,
    refine ⟨h_y.1,h_a_w,𝟙 _,_⟩,
    simpa },
  { refine ⟨h.1,𝟙 _, 𝟙 _, _⟩,
    simp },
  { rcases h_ih with ⟨j,i1,i2,h⟩,
    refine ⟨j,i2,i1,_⟩,
    symmetry, assumption },
  { rcases h_ih_a with ⟨j1,i11,i12,h1⟩,
    rcases h_ih_a_1 with ⟨j2,i21,i22,h2⟩,
    rcases is_filtered_or_empty.cocone_objs j1 j2 with ⟨j,i1,i2,_⟩,
    rcases is_filtered_or_empty.cocone_maps (i12 ≫ i1) (i21 ≫ i2) with ⟨jj,i,hh⟩,
    use jj,
    use i11 ≫ i1 ≫ i,
    use i22 ≫ i2 ≫ i,
    simp only [functor_to_types.map_comp_apply],
    rw [h1,←h2],
    simp_rw ←functor_to_types.map_comp_apply,
    rw hh }
end

[Reid Barton]

right, I think that's what I proved here

[Adam Topaz]

By the way, isn't there some general category theory voodoo which tells us that the underlying type of the colimits in CRing are the same as the colimits of the underlying type, using the fact that the forgetful functor from CRing to Set is a right adjoint?

[Adam Topaz]

Oh, no, right adjoints preserve limits.

[Adam Topaz]

And anyway, this is only true for filtered colimits.

[Adam Topaz]

I guess there is some general-nonsense type theorem that this fits into (something about algebras for Lawvere theories, etc.) but the proof seems to boil down to the fact that filtered colimits commute with finite limits in Set, so one would have to do the work that Reid is suggesting anyway :)

[Justus Springer]

As I've written here, I am taking on the project to prove that forgetful functors preserve filtered colimits. I just PR'd a working draft for Mon: #9101. Before I apply my approach to other algebraic categories like CommRing, I thought I'd ask for feedback on the general design (or just a go-head signal if you think it looks good). @Scott Morrison

[Reid Barton]

Have you seen the discussion starting here on this same topic from last year? It seems that your PR does a lot of work to check what basically amounts to the fact that the functor $X \mapsto X \times X$ on Set preserves filtered colimits. Specifically, if I have a filtered diagram $(M_i)_{i \in I}$ of monoids and I denote by $M$ the colimit in Set (for now) of the underlying sets, then $(M_i \times M_i)_{i \in I} \to M \times M$ is also a colimit diagram in Set.
Once you know this fact, there is a proof where you just fill in the multiplication map $M \times M \to M$ on the colimit of underlying sets to be the unique thing that fits in the diagram. On paper, this should be a lot slicker because the hard work occurs in the proof that $X \mapsto X \times X$ preserves filtered colimits, which I believe Scott proved in mathlib at some point in the past year. I don't know whether the slickness would necessarily preserve formalization though.

[Reid Barton]

More explicitly,

• (if this doesn't already exist) Define functors square and cube and punit which are given on objects by square.obj X = X × X and cube.obj X = X × X × X and punit.obj X = punit. Using the concrete built-in products (rather than fin 2 -> X or something) will make the later parts of the argument easier, and has a cost that only gets paid once. Prove that these functors preserve filtered counits, possibly using bowtie and tulip if there isn't already something more convenient.
  Then to construct the colimit of a filtered diagram F in Mon,

• Define the carrier M of the colimit as the colimit of (F ⋙ forget Mon), and define mk j : F.obj j -> M using the structure maps ι of the colimit.

• Define the multiplication mu : M × M -> M by using the universal property of M × M as a colimit (because square preserves filtered colimits). That makes sense because the maps in the diagram F preserve multiplication. Then define * on M by a * b = mu (a, b).
• mk j x * mk j y = mk j (x * y) by the construction of mu.
• To prove that * is associative, consider the two maps assoc1, assoc2 : M × M × M -> M defined by assoc1 x y z = (x * y) * z, assoc2 x y z = x * (y * z). Because M × M × M is a colimit, in order to check assoc1 = assoc2, it suffices to check that they agree back in each F.obj j × F.obj j × F.obj j. That holds because we can move mk past * and because F.obj j is associative.
• Repeat these last two steps for eta : punit -> M which is going to be the map picking out the unit, and the unit laws. Then we can make M into a monoid.
• To check an instance of the universal property of M in Mon: we know there's a unique map on underlying sets which makes everything commute. To see that it's a monoid homomorphism again amounts to checking that two maps out of M × M are equal and two maps out of punit are equal, and we can check these using uniqueness of maps out of a colimit again.

[Scott Morrison]

I think the last thing I PR'd was src#category_theory.limits.colimit_limit_to_limit_colimit_is_iso, which says:

# Filtered colimits commute with finite limits.

We show that for a functor `F : J × K ⥤ Type v`, when `J` is finite and `K` is filtered,
the universal morphism `colimit_limit_to_limit_colimit F` comparing the
colimit (over `K`) of the limits (over `J`) with the limit of the colimits is an isomorphism.

(In fact, to prove that it is injective only requires that `J` has finitely many objects.)

[Scott Morrison]

but I suspect there is a branch with more of Reid's proposal implemented.

[Scott Morrison]

Ah, I found the branch that I was working in a long time back... It is a mess and broken in places, but branch#preserves_filtered_colimits may have some useful stuff.

[Justus Springer]

Thanks so much for the detailed explanation @Reid Barton !
I saw the discussion you mentioned. I have to admit, I didn't look into it that much. The last thing I saw is there was some universe issue arising when proving that some functor category has limits. Instead of trying to understand this in detail, I figured I'd just start from scratch and discover any issues by my own. My approach goes as follows:

• Let $(M_i)_{i\in I}$ be a filtered diagram of monoids. Goal: Install a monoid structure on the colimit $M=\bigsqcup_i M_i/\sim$. Denote its element as equivalence classes of dependent pairs $[i,x]$ where $x\in M_i$.
• Define $1_M$ as $[j_0,1]$, where $j_0$ is an arbitrarily chosen object. Show this to be independent of the choice of $j_0$.
• Define multiplication $[i,x]\cdot[j,y]$ by passing to a common successor level $i\to k \leftarrow j$ and then multiply in $M_k$. Show this to be well-defined in both slots (that's where you need a tulip diagram) and also independent of $k$ (that's where you need a bowtie).
• Monoid laws are easily verified, as we can unfold the definition of $1_M$ and $\cdot_M$ at any custom index $j\in I$. For example, we have $1_M\cdot[j,x]=[j,1]\cdot[j,x]=[j,1\cdot x]=[j,x]$. Similarly for associativity.

For now, I'd argue that this approach is more straightforward than the one you mentioned. Although the approach via the functor X↦X×X looks slicker on paper, I have the feeling we'd have to be currying and uncurrying the multiplication mu : M × M → M all the time. Similarly, translating from eta : punit → M to 1 : M and back. That said, I didn't seriously give this approach a try. I'm definitely going to do some experiments, now that I understand it better. The question now is, whether it's worth switching to the other approach now.

[Justus Springer]

Scott Morrison said:

Ah, I found the branch that I was working in a long time back... It is a mess and broken in places, but branch#preserves_filtered_colimits may have some useful stuff.

I saw this branch, that's where I stole your bowtie from :wink: (#9099)

[Scott Morrison]

Sorry, yes, I've started to read your PRs since writing this and realised you must have found it!

[Reid Barton]

The main point is really that the same statement and proof also work for commutative monoids and groups and abelian groups and rings and commutative rings and modules and probably we want most of these facts as well. So, it would be best to minimize the work that is specific to the case of monoids. In that context, it seems wrong to be invoking stuff like tulip directly in a context where we are specifically talking about monoids. However, the monoids part of your PR is certainly not that long already and experimentation is definitely needed to know whether the alternative strategy I outlined would actually come out shorter.

[Reid Barton]

(It's also the case that the alternative strategy gives more generally preservation of sifted colimits, basically filtered colimits plus reflexive coequalizers, though I've personally never cared about reflexive coequalizers as much as I think I'm supposed to.)

[Reid Barton]

Justus Springer said:

I have the feeling we'd have to be currying and uncurrying the multiplication mu : M × M → M all the time. Similarly, translating from eta : punit → M to 1 : M and back.

I think it won't be so bad; this is the sort of thing Lean is very good at. I have an old branch https://github.com/leanprover-community/mathlib/commit/d4477fa7f79beea1058f72fc3741c88a1832d9a1#diff-1877ef03abd5d5a24980277d502e71d2418728fcf33ec4a8d26cacb0526245eeR565 with a similar sort of argument for Ore localization (not using the category theory library, but similarly obtaining the monoid structure from a universal property). In your situation it will be even simpler, because the universal property just involves maps in Set.

[Reid Barton]

But this is why I think it's important to literally use M × M and not, say, fin 2 -> M or some abstractly-given product functor on Set.

[Reid Barton]

By the way, there could be other ways to reduce duplication between the proofs for monoids, rings, etc. (In the limit, one invents universal algebra but it's probably too much to bite off for now.)

[Justus Springer]

Reid Barton said:

By the way, there could be other ways to reduce duplication between the proofs for monoids, rings, etc. (In the limit, one invents universal algebra but it's probably too much to bite off for now.)

I was planning to build things up incrementally. E.g. if I already have the additive monoid structure on M, I can build upon it for the ring structure etc. Hopefully @[to_additive] helps as well. Either way, there will of course be duplication. The question is how bad it gets...

[Justus Springer]

To be honest, I only care about the case of commutative rings anyway, so I'm not motivated enough to go down the universal algebra path... But of course I care about getting things right and stating it at the "correct" level of abstraction.

[Justus Springer]

So thanks again for the input! That's exactly why I'm PRing it now, before spending a lot more time duplicating this design to other algebraic categories.

[Justus Springer]

I've transported my approach to other algebraic categories and removed the WIP label from #9101 and #9099. It should be ready for review now.

[Justus Springer]

@Reid Barton I did some experiments, but then decided against changing original my approach. Most of the repetition is not because I need to define binary operations M×M→ M all the time. In fact, I define multiplication only once for monoids and then build upon it for other algebraic structures. Still, there is a lot of boilerplate code, as the basic pattern is the same for all the categories, and we need to verify all the axioms for every algebraic structure. But I think that would be the same with both approaches.

[Johan Commelin]

I've kicked the bowtie-and-tulip PR on the queue.

[Kevin Buzzard]

how appropriate that a Dutchman did it

[Johan Commelin]

I don't think I've ever touched a bowtie in my life

[Kevin Buzzard]

Maybe a Brit could have kicked that part of the PR.

[Patrick Massot]

Even when that picture was taken?

[Patrick Massot]

I think I see a bowtie on https://leanprover.zulipchat.com/avatar/112680/medium?v=2

[Johan Commelin]

ooh lol, I might have been wearing a bowtie during my PhD defense :rofl: I happily forgot that part of the ceremony

[Justus Springer]

It was a tough and well considered decision how to call the second diagram: Tulip, crown or trident.

[Johan Commelin]

@Justus Springer The Dutch are very proud of you now (-;

[Johan Commelin]

Next time you are looking for a name: we are also very fond of windmills, wooden shoes, and cheese.

[Filippo A. E. Nuccio]

Oh funny: I thought beer was also your cup of tea.