Zulip Chat Archive

Stream: maths

Topic: preserve filtered colimits


view this post on Zulip Scott Morrison (Aug 25 2020 at 13:31):

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.

view this post on Zulip Scott Morrison (Aug 25 2020 at 13:32):

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

view this post on Zulip Adam Topaz (Aug 25 2020 at 13:39):

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

view this post on Zulip Reid Barton (Aug 25 2020 at 13:42):

I don't remember proving anything like this.

view this post on Zulip Reid Barton (Aug 25 2020 at 13:47):

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.

view this post on Zulip Scott Morrison (Aug 25 2020 at 13:48):

Yes.

view this post on Zulip Scott Morrison (Aug 25 2020 at 13:49):

(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.)

view this post on Zulip Reid Barton (Aug 25 2020 at 13:51):

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.

view this post on Zulip Reid Barton (Aug 25 2020 at 13:51):

Which sounds pretty dreadful

view this post on Zulip Reid Barton (Aug 25 2020 at 13:51):

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

view this post on Zulip Scott Morrison (Aug 25 2020 at 13:53):

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

view this post on Zulip Reid Barton (Aug 25 2020 at 13:53):

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

view this post on Zulip Adam Topaz (Aug 25 2020 at 13:54):

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 :-/

view this post on Zulip Adam Topaz (Aug 25 2020 at 13:55):

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

view this post on Zulip Reid Barton (Aug 25 2020 at 13:56):

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

view this post on Zulip Adam Topaz (Aug 25 2020 at 13:57):

Yeah that should be fine for sheaves on topological spaces

view this post on Zulip Scott Morrison (Aug 25 2020 at 13:58):

yes

view this post on Zulip Reid Barton (Aug 25 2020 at 13:59):

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

view this post on Zulip Reid Barton (Aug 25 2020 at 14:00):

oh but actually it might prove the result you wanted originally

view this post on Zulip Reid Barton (Aug 25 2020 at 14:01):

docs#ring.direct_limit.of.zero_exact

view this post on Zulip Reid Barton (Aug 25 2020 at 14:02):

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

view this post on Zulip Reid Barton (Aug 25 2020 at 14:03):

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) :=

view this post on Zulip Adam Topaz (Aug 25 2020 at 14:14):

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

view this post on Zulip Reid Barton (Aug 25 2020 at 14:18):

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

view this post on Zulip Scott Morrison (Aug 25 2020 at 14:19):

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

view this post on Zulip Scott Morrison (Aug 25 2020 at 14:19):

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

view this post on Zulip Reid Barton (Aug 25 2020 at 14:20):

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

view this post on Zulip Scott Morrison (Aug 25 2020 at 14:21):

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

view this post on Zulip Scott Morrison (Aug 25 2020 at 14:21):

but I don't see it.

view this post on Zulip Reid Barton (Aug 25 2020 at 14:23):

Basically you need to do what Kenny did

view this post on Zulip Reid Barton (Aug 25 2020 at 14:25):

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)

view this post on Zulip Reid Barton (Aug 25 2020 at 14:27):

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

view this post on Zulip Reid Barton (Aug 25 2020 at 14:32):

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

view this post on Zulip Adam Topaz (Aug 25 2020 at 14:47):

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)

view this post on Zulip Adam Topaz (Aug 25 2020 at 17:23):

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.

view this post on Zulip Adam Topaz (Aug 25 2020 at 18:05):

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

view this post on Zulip Scott Morrison (Aug 25 2020 at 23:49):

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

view this post on Zulip Scott Morrison (Aug 25 2020 at 23:50):

prequotient.of.inj

view this post on Zulip Adam Topaz (Aug 26 2020 at 00:21):

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

view this post on Zulip Scott Morrison (Aug 26 2020 at 01:00):

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

view this post on Zulip Adam Topaz (Aug 26 2020 at 01:06):

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

view this post on Zulip Scott Morrison (Aug 26 2020 at 01:08):

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.

view this post on Zulip Scott Morrison (Aug 26 2020 at 01:11):

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

view this post on Zulip Adam Topaz (Aug 26 2020 at 01:19):

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

view this post on Zulip Adam Topaz (Aug 26 2020 at 01:21):

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

view this post on Zulip Scott Morrison (Aug 26 2020 at 01:37):

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

view this post on Zulip Scott Morrison (Aug 26 2020 at 01:51):

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

view this post on Zulip Adam Topaz (Aug 26 2020 at 01:58):

What of we get rid of trans from relation?

view this post on Zulip Adam Topaz (Aug 26 2020 at 01:58):

And just never define a setoid?

view this post on Zulip Adam Topaz (Aug 26 2020 at 01:59):

(same with symm and refl)

view this post on Zulip Adam Topaz (Aug 26 2020 at 02:00):

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

view this post on Zulip Scott Morrison (Aug 26 2020 at 02:10):

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

view this post on Zulip Scott Morrison (Aug 26 2020 at 02:11):

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.

view this post on Zulip Scott Morrison (Aug 26 2020 at 05:03):

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

view this post on Zulip Scott Morrison (Aug 26 2020 at 07:35):

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.

view this post on Zulip Scott Morrison (Aug 26 2020 at 09:31):

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. :-(

view this post on Zulip Reid Barton (Aug 26 2020 at 11:50):

Now you should prove that, say, XX×X×XX \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.

view this post on Zulip Reid Barton (Aug 26 2020 at 11:55):

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

view this post on Zulip Reid Barton (Aug 26 2020 at 11:57):

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

view this post on Zulip Reid Barton (Aug 26 2020 at 11:58):

If we instead used the expression ab+aca * b + a * c, we'd get the same maps for all the RiR_i, of course, and a priori a different map R×R×RRR \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.

view this post on Zulip Reid Barton (Aug 26 2020 at 11:59):

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.

view this post on Zulip Adam Topaz (Aug 26 2020 at 12:02):

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

view this post on Zulip Adam Topaz (Aug 26 2020 at 12:02):

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.

view this post on Zulip Reid Barton (Aug 26 2020 at 12:03):

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

view this post on Zulip Reid Barton (Aug 26 2020 at 12:03):

and so the corresponding fact for Set is very easy

view this post on Zulip Adam Topaz (Aug 26 2020 at 12:05):

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.

view this post on Zulip Adam Topaz (Aug 26 2020 at 12:10):

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.

view this post on Zulip Adam Topaz (Aug 26 2020 at 12:10):

And yes I agree the induction would be much smoother.

view this post on Zulip Reid Barton (Aug 26 2020 at 12:12):

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.

view this post on Zulip Adam Topaz (Aug 26 2020 at 12:12):

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

view this post on Zulip Adam Topaz (Aug 26 2020 at 12:19):

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?

view this post on Zulip Adam Topaz (Aug 26 2020 at 12:59):

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

view this post on Zulip Reid Barton (Aug 26 2020 at 13:03):

right, I think that's what I proved here

view this post on Zulip Adam Topaz (Aug 26 2020 at 13:06):

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?

view this post on Zulip Adam Topaz (Aug 26 2020 at 13:11):

Oh, no, right adjoints preserve limits.

view this post on Zulip Adam Topaz (Aug 26 2020 at 13:12):

And anyway, this is only true for filtered colimits.

view this post on Zulip Adam Topaz (Aug 26 2020 at 14:19):

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


Last updated: May 09 2021 at 09:11 UTC