## Stream: maths

### Topic: preserve filtered colimits

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


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

#### Adam Topaz (Aug 25 2020 at 13:39):

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

#### Reid Barton (Aug 25 2020 at 13:42):

I don't remember proving anything like this.

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

Yes.

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

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

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

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

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

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

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

#### Reid Barton (Aug 25 2020 at 13:56):

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

#### Adam Topaz (Aug 25 2020 at 13:57):

Yeah that should be fine for sheaves on topological spaces

yes

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

#### Reid Barton (Aug 25 2020 at 14:00):

oh but actually it might prove the result you wanted originally

#### Reid Barton (Aug 25 2020 at 14:01):

docs#ring.direct_limit.of.zero_exact

#### Reid Barton (Aug 25 2020 at 14:02):

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

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


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


#### Reid Barton (Aug 25 2020 at 14:18):

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

#### Scott Morrison (Aug 25 2020 at 14:19):

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

#### Scott Morrison (Aug 25 2020 at 14:19):

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

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

#### Scott Morrison (Aug 25 2020 at 14:21):

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

#### Scott Morrison (Aug 25 2020 at 14:21):

but I don't see it.

#### Reid Barton (Aug 25 2020 at 14:23):

Basically you need to do what Kenny did

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

#### Reid Barton (Aug 25 2020 at 14:27):

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 (Aug 25 2020 at 14:32):

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

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


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

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

#### Scott Morrison (Aug 25 2020 at 23:49):

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

#### Scott Morrison (Aug 25 2020 at 23:50):

prequotient.of.inj

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

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

#### Adam Topaz (Aug 26 2020 at 01:06):

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

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

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

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

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

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


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

#### Adam Topaz (Aug 26 2020 at 01:58):

What of we get rid of trans from relation?

#### Adam Topaz (Aug 26 2020 at 01:58):

And just never define a setoid?

#### Adam Topaz (Aug 26 2020 at 01:59):

(same with symm and refl)

#### Adam Topaz (Aug 26 2020 at 02:00):

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

#### Scott Morrison (Aug 26 2020 at 02:10):

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

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

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

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

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

#### Reid Barton (Aug 26 2020 at 11:50):

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 (Aug 26 2020 at 11:55):

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 (Aug 26 2020 at 11:57):

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 (Aug 26 2020 at 11:58):

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

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

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

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

#### Reid Barton (Aug 26 2020 at 12:03):

and so the corresponding fact for Set is very easy

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

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

#### Adam Topaz (Aug 26 2020 at 12:10):

And yes I agree the induction would be much smoother.

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

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

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

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


#### Reid Barton (Aug 26 2020 at 13:03):

right, I think that's what I proved here

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

#### Adam Topaz (Aug 26 2020 at 13:11):

Oh, no, right adjoints preserve limits.

#### Adam Topaz (Aug 26 2020 at 13:12):

And anyway, this is only true for filtered colimits.

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