## Stream: condensed mathematics

### Topic: Simplicial stuff

#### Adam Topaz (Mar 16 2021 at 16:43):

Hi all, I'm working on developing some of the basic simplicial constructions necessary for the project -- especially toward hypercovers.
For now I would like to define the coskeleton functors (and prove that they're adjoint to the skeleton functors).
I made a mathlib PR with the skeleton functors earlier today: #6711

The coskeleton functors will be a bit more of a challenge :)

#### Adam Topaz (Mar 17 2021 at 21:11):

... So I'm still running into a LOT of annoying universe-related issues. To define the coskeleton functors, one takes a limit over some finite diagram indexed by a category constructed out of simplex_category. The issue is that to take a limit of a diagram indexes by J in a category C with universe parameters category.{v u} C, we must have J : Type v with J a small category.

So, I defined the following gadget
https://github.com/leanprover-community/mathlib/blob/296104b7f3295aa40c68efd17b310f33e13f318b/src/category_theory/category/ulift.lean#L73
that lets you lift a small category to another small category in another universe.

But now I find myself having to use things like ulift'.equivalence.congr_left.functor.obj all over the place and I'm ready to give up...

What's the best way forward?

#### Johan Commelin (Mar 17 2021 at 21:15):

@Scott Morrison do you have a good idea?

#### Adam Topaz (Mar 17 2021 at 21:16):

I feel like this whole enterprise would be a lot easier if we had a universe polymorphic simplex_category to begin with

#### Adam Topaz (Mar 17 2021 at 21:17):

And define simplicial_object C in the case category.{v u} C as simplex_category.{v}\op \func C.

#### Johan Commelin (Mar 17 2021 at 21:17):

hmm, because even if you say that C has objects in Type, then you are stuck when C is large.

#### Adam Topaz (Mar 17 2021 at 21:17):

Not even just for large C, but any time the morphisms of C are not in Type

#### Johan Commelin (Mar 17 2021 at 21:17):

Right, so also for laaaarge categories (-;

#### Adam Topaz (Mar 17 2021 at 21:18):

Oh yeah, you're right, if C : Type then that's the same as Cbeing large :)

#### Adam Topaz (Mar 17 2021 at 21:18):

or $\mathfrak{LARGE}$

#### Johan Commelin (Mar 17 2021 at 21:18):

But for NormedGroup.{0} and Profinite.{0} etc... we are fine.

#### Johan Commelin (Mar 17 2021 at 21:19):

So, if we just want to flesh out the theory modulo universe issues, you could assume v = 0 everywhere, for now.

#### Adam Topaz (Mar 17 2021 at 21:19):

Yeah, I think so. But it feels silly to construct these things without making it mathlib compatible

#### Johan Commelin (Mar 17 2021 at 21:20):

The downside of simplex_category := NonEmptyFinLinOrd is that now the simplex category is suddenly large.

#### Adam Topaz (Mar 17 2021 at 21:20):

Well, I already wrote a bunch of code proving all the associated categories were finite, which relies on the fact that fin a -> fin b and fin c are all finite types, and using NonEmptyFinLinOrd would make that part a lot harder...

#### Adam Topaz (Mar 17 2021 at 21:21):

This is all in branch#simplicial_cosk

#### Johan Commelin (Mar 17 2021 at 21:22):

@Mario Carneiro How evil is it to have universe constraints of the form u1 \le u2 in your type theory.

#### Peter Scholze (Mar 17 2021 at 21:22):

I think the simplex category should be a "concrete" category, i.e. have objects equal to the nonnegative integers (does that even make sense? In some sense it shouldn't...)

#### Adam Topaz (Mar 17 2021 at 21:22):

@Peter Scholze Yeah, that's how it's constructed right now

OK, great

#### Johan Commelin (Mar 17 2021 at 21:22):

But in Lean universes are not cumulative.

#### Adam Topaz (Mar 17 2021 at 21:23):

But we also have some API for skeletons of categories, which is supposed to make this easier (in theory :smile: )

#### Johan Commelin (Mar 17 2021 at 21:23):

So simplex_category : Type and hence not : Type v for larger v.

I'd guess so

#### Johan Commelin (Mar 17 2021 at 21:23):

And when you set up an API for categorical limits, you have to decide where the index categories of your limits live.

#### Johan Commelin (Mar 17 2021 at 21:24):

Ideally, they just live in any "small" universe. But you can't quantify over universes...

#### Peter Scholze (Mar 17 2021 at 21:24):

Surely they are small limits, so they probably live one universe level down from the ambient one

Aha, OK...

#### Johan Commelin (Mar 17 2021 at 21:25):

So, we currently have category.{v u} C which means C : Type u are the objects, and Hom X Y : Type v for the morphisms

#### Johan Commelin (Mar 17 2021 at 21:25):

And index categories for limits must live in Type v.

#### Johan Commelin (Mar 17 2021 at 21:26):

But when you have a limit that is naturally indexed by something in Type w for w < v, Lean just says "nope"

#### Johan Commelin (Mar 17 2021 at 21:26):

And that's annoying.

#### Peter Scholze (Mar 17 2021 at 21:26):

Oh, that's annoying indeed.

#### Peter Scholze (Mar 17 2021 at 21:26):

so there's no "universe coercion" or something like that?

#### Johan Commelin (Mar 17 2021 at 21:26):

So you can build constructions that lift things to a higher universe... yes

#### Johan Commelin (Mar 17 2021 at 21:26):

But you don't want to have those all over the place, if you can avoid it

#### Adam Topaz (Mar 17 2021 at 21:26):

We have this ulift thing

#### Adam Topaz (Mar 17 2021 at 21:26):

So I can write this, for example

def simplex_category' := ulift.{u} ℕ

instance : small_category.{u} simplex_category' :=
{ hom := λ a b, ulift (fin (a.down+1) →ₘ fin (b.down+1)),
id := λ a, ulift.up preorder_hom.id,
comp := λ _ _ _ f g, ulift.up $preorder_hom.comp g.down f.down }  #### Johan Commelin (Mar 17 2021 at 21:28): I don't know enough about foundations of maths/type theory to know what can of worms is opened by allowing to quantify over universes. #### Johan Commelin (Mar 17 2021 at 21:28): @Peter Scholze Do you know of a construction in mathematics that iterates "universe bumps"? #### Johan Commelin (Mar 17 2021 at 21:29): A universe bump, is for example the topos-theoretic approach to cohomology. If you take the abstract approach to etale cohomology, then for X : Scheme.{0} the etale cohomology will live in Type 1 #### Johan Commelin (Mar 17 2021 at 21:30): So now you can imagine that you look at Spec (some_cohomology_ring) or so... #### Johan Commelin (Mar 17 2021 at 21:31): But I don't really know of a natural example where you would want to iterate this process arbitrarily often. #### Mario Carneiro (Mar 17 2021 at 21:31): Johan Commelin said: Mario Carneiro How evil is it to have universe constraints of the form u1 \le u2 in your type theory. They already exist, you just can't write them. But they aren't usually needed, since you get an equivalent effect by replacing all instances of u2 with max u1 u2 #### Adam Topaz (Mar 17 2021 at 21:31): Or even better, if you construct say the etale \pi_1 in the categorical way it would be a group in Type 1, and then you take group cohomology of that constructed in some categorical way and you get something in Type 2, etc. #### Johan Commelin (Mar 17 2021 at 21:33): @Mario Carneiro But that doesn't allow quantifying over all u1 such that max u1 u2 = u2 #### Johan Commelin (Mar 17 2021 at 21:33): I somehow want to write def foobar {v} {v \le u} (I : Type v) ...  #### Kevin Buzzard (Mar 17 2021 at 21:34): @Adam Topaz you say etc etc but I can't see this naturally leading to a situation where we might want to universe-bump infinitely often. #### Adam Topaz (Mar 17 2021 at 21:34): Oh I see. yes of course. #### Adam Topaz (Mar 17 2021 at 21:35): Well, then you can iterate the classifying space construction of an abelian group #### Adam Topaz (Mar 17 2021 at 21:35): (which is involved in the second step of my example) #### Kevin Buzzard (Mar 17 2021 at 21:36): I did my entire course just using Prop and Type, I knew it would all fit into ZFC and I think universes are just one more thing that makes lean look intimidating #### Mario Carneiro (Mar 17 2021 at 21:39): @Johan Commelin Instead of def foobar {v} {v \le u} (I : Type v) ... Type u  you write def foobar {v} (I : Type v) ... Type (max u v)  #### Adam Topaz (Mar 17 2021 at 21:41): But what if v changes in another definition later on, while u stays the same? #### Johan Commelin (Mar 17 2021 at 21:42): @Mario Carneiro What do you suggest that this should be changed to: universes v u u' u'' w -- declare the v's first; see category_theory.category for an explanation variables {J K : Type v} [small_category J] [small_category K] variables {C : Type u} [category.{v} C] variables {F : J ⥤ C} /-- A cone t on F is a limit cone if each cone on F admits a unique cone morphism to t. See https://stacks.math.columbia.edu/tag/002E. -/ @[nolint has_inhabited_instance] structure is_limit (t : cone F) := (lift : Π (s : cone F), s.X ⟶ t.X) (fac' : ∀ (s : cone F) (j : J), lift s ≫ t.π.app j = s.π.app j . obviously) (uniq' : ∀ (s : cone F) (m : s.X ⟶ t.X) (w : ∀ j : J, m ≫ t.π.app j = s.π.app j), m = lift s . obviously)  #### Johan Commelin (Mar 17 2021 at 21:42): Currently J : Type v and [category.{v} C] #### Johan Commelin (Mar 17 2021 at 21:43): Somehow, J should be small, relative to C #### Mario Carneiro (Mar 17 2021 at 21:43): where does the inequality come up? #### Mario Carneiro (Mar 17 2021 at 21:43): [category.{v (max v u)} C] #### Johan Commelin (Mar 17 2021 at 21:43): Well, we would like to be able to consider both J : Type v and J : Type 0 #### Johan Commelin (Mar 17 2021 at 21:44): And if v happens to be 2, then J : Type 1 should also work #### Mario Carneiro (Mar 17 2021 at 21:44): or actually just variables {C : Type (max v u)} [category.{v} C] #### Mario Carneiro (Mar 17 2021 at 21:44): I mean, why does the inequality need to exist? Why can't you use a small u #### Johan Commelin (Mar 17 2021 at 21:45): I think u is unrelated to what we are doing. #### Mario Carneiro (Mar 17 2021 at 21:45): You said you need v <= u #### Mario Carneiro (Mar 17 2021 at 21:45): so apparently u needs to be large #### Johan Commelin (Mar 17 2021 at 21:45): I want J : Type v1 and [category.{v2} C] and v1 <= v2 #### Mario Carneiro (Mar 17 2021 at 21:46): what happens if the inequality fails? #### Johan Commelin (Mar 17 2021 at 21:46): And C : Type u, but that doesn't matter. #### Mario Carneiro (Mar 17 2021 at 21:46): Oh there are two v's? #### Mario Carneiro (Mar 17 2021 at 21:46): There aren't in that snippet #### Johan Commelin (Mar 17 2021 at 21:46): Currently v1 = v2 #### Johan Commelin (Mar 17 2021 at 21:47): But that causes trouble, because now we can take limits over simplex_category : Type 0 #### Adam Topaz (Mar 17 2021 at 21:47): Concretely, we want the following example to work: import category_theory.limits.limits universes v u open category_theory variables (C : Type u) [category.{v} C] [limits.has_limits C] variables (J : Type) [small_category J] (F : J ⥤ C) example : C := limits.limit F  #### Johan Commelin (Mar 17 2021 at 21:49): And we want to show that Type 2 has all products indexed by J : Type v for v = 0, v = 1 and v = 2. If that is possible, it would be great. #### Scott Morrison (Mar 17 2021 at 21:49): Without addressing the harder issue of increasing the universe polymorphicity of limits.limit, I think @Adam Topaz's suggestion above def simplex_category' := ulift.{u} ℕ instance : small_category.{u} simplex_category' := { hom := λ a b, ulift (fin (a.down+1) →ₘ fin (b.down+1)), id := λ a, ulift.up preorder_hom.id, comp := λ _ _ _ f g, ulift.up$ preorder_hom.comp g.down f.down }


is going to be pretty good.

#### Scott Morrison (Mar 17 2021 at 21:49):

After a very small amount of API for converting nat to simplex_category', it should be smooth sailing, no?

#### Johan Commelin (Mar 17 2021 at 21:50):

So that should just become the new definition of simplex_category?

Yes.

#### Adam Topaz (Mar 17 2021 at 21:50):

That sounds good to me.

#### Johan Commelin (Mar 17 2021 at 21:50):

We want some API indeed:

-- X.obj (op $(0:ℕ)) is quite a mouthful to talk about X_0 :sad: variables {C : Type*} [category C] (X : simplicial_object C) (Y : C) (f : X.obj (op$ (0:ℕ)) ⟶ Y)


#### Scott Morrison (Mar 17 2021 at 21:51):

But while we're at it, we should record somewhere Adam's other code snippet, ending at example : C := limits.limit F, perhaps as a github issue, because this is exactly what we really want.

#### Scott Morrison (Mar 17 2021 at 21:53):

local notation [n] := mk n


#### Johan Commelin (Mar 17 2021 at 21:53):

Can we have open_locale simplicial enable that?

#### Scott Morrison (Mar 17 2021 at 21:53):

where we can hide the ulift, and also put it under open_locale simplicial.

#### Scott Morrison (Mar 17 2021 at 21:53):

there's already localized notation in sSet

#### Scott Morrison (Mar 17 2021 at 21:54):

perhaps we could combine those into one locale

#### Scott Morrison (Mar 17 2021 at 21:54):

I'm not sure how much Lean time I will have today, but I can try to insert this ulift into what is already in mathlib sometime.

#### Adam Topaz (Mar 17 2021 at 21:56):

I'm starting the refactor now @Scott Morrison.

#### Adam Topaz (Mar 17 2021 at 21:56):

Probably won't finish today, but feel free to push to my branch (I'll push it to github once something is working)

#### Scott Morrison (Mar 17 2021 at 21:57):

(I wish we could rename the emojis. You have to type :working on it: to get that one, but we all seem to use it as the much better :you are working on it and that is awesome:.)

#### Peter Scholze (Mar 17 2021 at 21:57):

Well, in this proetale business one wants to often construct things that admit no further etale covers, for which one takes a product of "all" etale maps, and sometimes needs to iterate this process countably many times. If one is not careful, one would enlarge the universe infinitely often

#### Scott Morrison (Mar 17 2021 at 21:58):

That is something we can not do around here. :-)

#### Peter Scholze (Mar 17 2021 at 21:59):

Well, I'm not doing it either, I stay in one universe throughout

#### Peter Scholze (Mar 17 2021 at 21:59):

But I put some nasty cardinal bounds in to justify this

#### Peter Scholze (Mar 17 2021 at 22:00):

Anyways, I'm off for tonight! I'm really excited about the progress!

#### Johan Commelin (Mar 17 2021 at 22:01):

Thanks for the example

#### Adam Topaz (Mar 17 2021 at 22:50):

@Scott Morrison @Johan Commelin I pushed a sketchy refactor to this branch: branch#simplex_refactor

It still needs a bit of cleaning up, but at least there are no errors.

Also the has_(co)limit instances are now MUCH easier :)

#### Adam Topaz (Mar 17 2021 at 22:51):

In any case, I'm done for today, but please feel free to push to this branch as you see fit

#### Scott Morrison (Mar 17 2021 at 23:36):

I pushed a commit making simplex_category irreducible.

#### Scott Morrison (Mar 17 2021 at 23:48):

I was aspiring to make mk irreducible as well, but that one has me stumped at the moment.

#### Bhavik Mehta (Mar 18 2021 at 11:56):

I started a refactor to mathlib generalising the universe variables for limits a few weeks ago, basically allowing us to talk about non-small limits as well - it mostly went pretty smoothly and I'm hoping to PR it soon

#### Scott Morrison (Mar 18 2021 at 12:11):

Looking forward to it!

#### Johan Commelin (Mar 18 2021 at 12:34):

@Bhavik MehtaEager to know what you come up with!

#### Adam Topaz (Mar 18 2021 at 15:08):

I refactors a bit more around simplex_category in the following branch, building on Scott's latest commits:
https://github.com/leanprover-community/mathlib/compare/simplex_refactor_hom_irred

#### Adam Topaz (Mar 18 2021 at 15:09):

The main thing is that I introduced an (irreduccible) simplex_category.hom with a little API with mk and to_preorder_hom.

#### Adam Topaz (Mar 18 2021 at 15:09):

Adding some careful simp lemmas actually simplifies the file quite a bit with a lot of simp lemmas being redundant.

#### Adam Topaz (Mar 18 2021 at 15:10):

The only strange thing is that I now have to use simpa [fin.pred_above] in a few places whereas previously it was just simpa. I don't really know why, but it works.

#### Adam Topaz (Mar 18 2021 at 15:11):

The skeletal functor for simplex_category is now completely universe polymorphic -- simplex_category and NonemptyFinLinOrd can be in completely unrelated universes.

#### Adam Topaz (Mar 18 2021 at 16:14):

I would also like to introduce the following (localized) notation. What's a sensible value for 1000 in the following code?

-- TODO: find a sensible value for 1000.
localized
"notation X _[:1000 n ] := (X : simplicial_object _).obj (op (simplex_category.mk n))"
in simplicial


#### Adam Topaz (Mar 18 2021 at 16:15):

This way the face maps look nice:

def δ {n} (i : fin (n+2)) : X _[n+1] ⟶ X _[n] :=


#### Adam Topaz (Mar 18 2021 at 16:16):

Of course, if someone has another suggestion for a better approximation of $X_{n+1} \to X_n$, please let me know :)

#### Peter Scholze (Mar 18 2021 at 16:17):

I have no idea what's happening here. What is the 1000 supposed to be doing?

#### Adam Topaz (Mar 18 2021 at 16:17):

Oh, it's a silly lean thing... it just tells lean how much priority to give to this notation

Ah!

#### Adam Topaz (Mar 18 2021 at 16:18):

Without the 1000, I would have to write X _[n+1] ⟶ (X _[n]) or else lean would get confused

#### Johan Commelin (Mar 18 2021 at 16:19):

Peter, these numbers govern whether a + b * c is (a + b) * c or a + (b * c). Luckily, they work out to mean the latter (-;

#### Peter Scholze (Mar 18 2021 at 16:19):

In what range do they live, typically?

#### Johan Commelin (Mar 18 2021 at 16:19):

0 -- 1024

#### Adam Topaz (Mar 18 2021 at 16:19):

not sure exactly, but 1000 is high

#### Johan Commelin (Mar 18 2021 at 16:20):

Ooh, I guess 0 or 1024 doesn't belong to the range... but I'm not sure

#### Adam Topaz (Mar 18 2021 at 16:21):

= is _ =:50 _:50 := eq #1 #0

#### Adam Topaz (Mar 18 2021 at 16:21):

(so 50 is meant to be very low)

#### Kevin Buzzard (Mar 18 2021 at 16:32):

$ mentions zero: _ $:1 _:0 := #1 #0

#### Yakov Pechersky (Mar 18 2021 at 16:33):

There's also :max and one more than that, :std.prec.max_plus, that "turns it up to 11", which means bind in the strongest way possible, currently only used for

src/data/opposite.lean:notation α ᵒᵖ:std.prec.max_plus := opposite α
src/field_theory/adjoin.lean:notation K⟮:std.prec.max_plus l:(foldr ,  (h t, insert.insert t h) ∅) ⟯ := adjoin K l


#### Kevin Buzzard (Mar 18 2021 at 16:35):

but

infixr ⋆:1000000 := has_mul.mul

#print notation ⋆ -- _ ⋆:1000000 _:999999 := has_mul.mul #1 #0


#### Adam Topaz (Mar 18 2021 at 16:36):

@Yakov Pechersky I don't really understand the notation syntax. Does the above X _[n] notation look reasonable to you?

#### Adam Topaz (Mar 18 2021 at 16:38):

Should the X and/or the ] have some number next to them as well?

#### Yakov Pechersky (Mar 18 2021 at 16:41):

I think it will work. Here's my test:

open_locale big_operators

notation  _[:1000 n ] := fin n

#print notation _[

#check λ (f : (fin _ × fin _ → ℕ)), ∑ i : _[ 2 + 2 ] × _[ 3 * 3 ], f i


#### Yakov Pechersky (Mar 18 2021 at 16:41):

Without a number, ] will be :0 which I don't think will make a difference whether it is 0 or 999

#### Scott Morrison (Mar 18 2021 at 22:02):

I refactored a bit more around simplex_category in the following branch, building on Scott's latest commits:
https://github.com/leanprover-community/mathlib/compare/simplex_refactor_hom_irred

#### Adam Topaz (Mar 18 2021 at 22:05):

I think so... let me go through it quickly an open a PR.

#6761

#### Adam Topaz (Mar 18 2021 at 22:37):

@Scott Morrison One thing to note: this PR deletes a handful of the simp lemmas that were in the file from before, in favor of some simp lemmas for this new (irreducible) simplex_category.hom. If there's a lemma that seems to be missing, I'd be happy to add it back.

#### Adam Topaz (Mar 19 2021 at 19:19):

aaah. I'm running into even more categorical headaches. This time I think it's because opposite is irreducible.

It feels really silly that tidy cant close this proof all by itself. I don't even want to think about the map_comp' field if map_id' is hard!
I think the issue boils down to the definition here:
https://github.com/leanprover-community/mathlib/blob/ec1b65487b40942baa21bf2dc3dd0a337e4f8f83/src/algebraic_topology/simplex_category.lean#L461

along with the fact that tidy can't see past the definition of unop.

Anyone have any thoughts on how to simplify this situation?

#### Johan Commelin (Mar 19 2021 at 20:17):

Sorry, I'm completely spent. I hope someone else can take a look. Otherwise, I'll see if I can help once I'm re-energized.

#### Kevin Buzzard (Mar 19 2021 at 20:22):

I'm trying but I'm not getting anywhere

#### Adam Topaz (Mar 19 2021 at 20:22):

Crazy idea: can we define simplex_category so that we NEVER use opposites?

#### Adam Topaz (Mar 19 2021 at 20:23):

I even tried going through this making opposite and friends semireducible, and it's not much better.

#### Kevin Buzzard (Mar 19 2021 at 20:24):

I tried making opposite reducible and the code just broke :-)

#### Adam Topaz (Mar 19 2021 at 20:24):

semireducible is better because you can still write things like foo.unop

#### Adam Topaz (Mar 19 2021 at 20:27):

with things being semireducible I got down to

C : Type u,
_inst_1 : category C,
n : ℕ,
_inst_2 : has_finite_limits C,
X : simplex_categoryᵒᵖ,
T : truncated C n,
j_val : over (unop X),
j_property : simplex_category.len j_val.left ≤ n
⊢ (over.map (simplex_category.hom.mk preorder_hom.id)).obj ↑(unop ⟨j_val, j_property⟩) = j_val


#### Adam Topaz (Mar 19 2021 at 20:27):

but simp still gets stuck, i guess because of the various unops

#### Adam Topaz (Mar 19 2021 at 20:29):

is there a tactic that makes something reducible in the middle of a tactic block?

#### Kevin Buzzard (Mar 19 2021 at 21:01):

Right, this is as far as I can get too.

#### Kevin Buzzard (Mar 19 2021 at 21:02):

You can also do this:

      have h : simplex_category.hom.mk preorder_hom.id = simplex_category.hom.id (unop X),
ext,
refl,


but if you rw h it doesn't seem to help and then simp just unrewrites it again.

#### Johan Commelin (Mar 20 2021 at 04:17):

@Adam Topaz We are also using some cosimplicial objects in LTE... so defining simplex_category to usual_simplex_category^op will just shift the problems around, I fear.

#### Bhavik Mehta (Mar 20 2021 at 04:44):

Is this just a Kan extension? Taking a limit in this form looks familiar to me, I've come across a bunch of goals which look like this and I think they can all be unified nicely

#### Adam Topaz (Mar 20 2021 at 05:02):

Yeah this is probably some sort of Kan extension.

#### Adam Topaz (Mar 20 2021 at 05:02):

And yeah good point about the cosimplicial objects.

#### Adam Topaz (Mar 20 2021 at 05:20):

I guess this is exactly the right(?) Kan extension along the inclusion of (truncated n)\op into simplex_category\op.

#### Adam Topaz (Mar 20 2021 at 13:49):

@Bhavik Mehta I guess it could be useful to have Kan extensions in mathlib (everything is a Kan extension, after all...). The question is what assumptions should we add to ensure they exist? We could ask that the category has all limits, but this is too strong. In the coskeleton case, you only need finite limits because the categories in question all happen to be finite, but of course this won't be true for a general Kan extension.

#### Adam Topaz (Mar 20 2021 at 14:05):

I also realize now that this trunc gadget I defined is just some comma category associated to the inclusion of truncated n into simplex_category.

#### Bhavik Mehta (Mar 20 2021 at 14:24):

Bhavik Mehta I guess it could be useful to have Kan extensions in mathlib (everything is a Kan extension, after all...). The question is what assumptions should we add to ensure they exist? We could ask that the category has all limits, but this is too strong. In the coskeleton case, you only need finite limits because the categories in question all happen to be finite, but of course this won't be true for a general Kan extension.

I think the right thing to do is copy the is/has limit pattern, and have a class saying that certain Kan extensions do exist, but not all, so that we can talk about both local and global Kan extensions - and for the existence of global Kan extensions we should just be able to assume that the appropriate (co)limits over comma categories exist; so in your case you can show this by using equivalence to your finite index categories

#### Bhavik Mehta (Mar 20 2021 at 14:26):

(In #5152 I constructed the global left Kan extension given small colimits, but I certainly agree it's better to have additional restrictions)

#### Adam Topaz (Mar 20 2021 at 15:39):

@Johan Commelin another reason to have Kan extensions is to "define" the big Witt vectors :rofl:
https://ncatlab.org/nlab/show/Lambda-ring

#### Johan Commelin (Mar 20 2021 at 16:09):

We already have examples of Lambda rings in mathlib! Just not the a definition of Lambda ring, so the examples aren't registered as such. But certain Dickson polynomials give an example.

#### Johan Commelin (Mar 20 2021 at 18:00):

By the way, (@Scott Morrison) the alternating face map cochain complex attached to a cosimplicial object is now done. Just pointing this out, in case others had it on a todo list somewhere.

#### Johan Commelin (Mar 20 2021 at 18:05):

@Adam Topaz Is there still something that you want me to look at?

#### Johan Commelin (Mar 20 2021 at 18:05):

Or does the Kan machine solve your troubles?

#### Adam Topaz (Mar 20 2021 at 18:06):

I think building right Kan extensions is the way to go here. I'll try it out on Monday

#### Adam Topaz (Mar 20 2021 at 18:08):

Are we going full Dold-Kan? Or do we just need the construction of a complex from a cosimplicial object?

#### Johan Commelin (Mar 20 2021 at 18:08):

The latter. But it's already done.

#### Johan Commelin (Mar 20 2021 at 18:08):

Of course full Dold-Kan would be nice to have, independent from LTE.

#### Adam Topaz (Mar 20 2021 at 18:10):

And what sort of API do we need from hypercovers by profinite sets?

#### Johan Commelin (Mar 20 2021 at 18:13):

https://leanprover-community.github.io/liquid/sect0005.html#prop:normedcompletion

#### Johan Commelin (Mar 20 2021 at 18:13):

This is the "end goal" of the simplicial stuff

#### Johan Commelin (Mar 20 2021 at 18:14):

Patrick is working on the dependency https://leanprover-community.github.io/liquid/sect0005.html#prop:completeexact that is used in the proof.

Sounds good.

#### Johan Commelin (Mar 20 2021 at 18:15):

@Adam Topaz From that "end goal" we only need the second half

#### Johan Commelin (Mar 20 2021 at 18:15):

So this will use the Vhat.lean that you are already familiar with, I think

#### Johan Commelin (Mar 20 2021 at 18:15):

I'll make a mental todo, to split that lemma into two pieces in the blueprint

#### Johan Commelin (Mar 20 2021 at 18:16):

actually, let me just do it right now

#### Johan Commelin (Mar 20 2021 at 18:37):

@Adam Topaz due to the split, the "end goal" is now https://leanprover-community.github.io/liquid/sect0005.html#hypercover-exact

#### Adam Topaz (Mar 20 2021 at 18:41):

Ok so the key point is to write a hypercovers of profinite sets as a cofiltered limit of finite sets. I think the key point for that is the equivalence between Pro(Fintype) and Profinite. What's the status of that @Bhavik Mehta @Calle Sönne ?

#### Bhavik Mehta (Mar 20 2021 at 18:42):

Do you need the full equivalence of categories or is the expression of a profinite set as a cofiltered limit of finite sets enough?

#### Adam Topaz (Mar 20 2021 at 18:44):

I think you need a categorical equivalence (maybe a bit less, but still something close to that), since we're looking at simplicial profinite sets, meaning we certainly need some compatibility with morphisms

#### Adam Topaz (Mar 20 2021 at 18:47):

Oh, and I guess we will also need alt_face_map_complex to be functorial

#### Johan Commelin (Mar 20 2021 at 18:49):

hah! good point. Currently it isn't set up that way.

#### Johan Commelin (Mar 20 2021 at 18:49):

Well... there's nothing for simplicial objects anyway.

#### Johan Commelin (Mar 20 2021 at 18:49):

I grabbed stuff from branch#sset, and dualized it to make it work for cosimplicial stuff

#### Adam Topaz (Mar 22 2021 at 16:39):

Yep! this is good enough. I'm trying to add the last few bits from your code @Bhavik Mehta regarding the adjunctions being (co)reflective when $\iota$ is fully faithful

#### Adam Topaz (Mar 22 2021 at 16:39):

I think it would be ready to PR once that's done.

#### Bhavik Mehta (Mar 22 2021 at 16:39):

Cool! Let me know if there's anything I can do :)

#### Bhavik Mehta (Mar 22 2021 at 16:40):

To be honest I think it's ready to PR without that extra stuff, and those bits can be another PR

#### Adam Topaz (Mar 22 2021 at 16:40):

I'll try for a few mins, and if I get bogged down (which I probably will), I'll leave those for later.

#### Adam Topaz (Mar 22 2021 at 16:59):

@Bhavik Mehta is there a lemma of the following form in mathlib?

lemma is_iso_π_initial {J : Type v} [small_category J] {C : Type u₁} [category.{v} C] {j : J}
(term : is_initial j) [has_limits_of_shape J C] (F : J ⥤ C) : is_iso (limit.π F j) := sorry


#### Bhavik Mehta (Mar 22 2021 at 17:00):

Nope and there absolutely should be

#### Adam Topaz (Mar 22 2021 at 17:00):

It's similar to your thingy2 :)

#### Bhavik Mehta (Mar 22 2021 at 17:00):

There's some related things in limits/shapes/initial

#### Adam Topaz (Mar 22 2021 at 17:28):

#6820
I compromised by only providing the initial/terminal defs, leaving the actual proof of (co)reflectivity to when we have lemmas such as is_iso_π_initial as above (and a similar one for colimits)

#### Adam Topaz (Mar 22 2021 at 17:52):

An idea for a nice project: Prove that the ultrafilter monad is isomorphic to the right Kan extension of the inclusion Fintype -> Type (over itself)

#### Adam Topaz (Mar 22 2021 at 20:17):

Once #6820 goes through, here's the coskeleton functor (and the adjunction with the skeleton functor)
https://github.com/leanprover-community/mathlib/blob/6b69979cc2f4b136212e4f3196138e17bb735b1f/src/algebraic_topology/simplicial_object.lean#L153

#### Bhavik Mehta (Mar 23 2021 at 00:40):

Yeah codensity monads would be cool to have

#### Peter Scholze (Mar 25 2021 at 09:22):

By the way, for the proof of 9.5, one only needs the version of 8.19 for Cech nerves of covers $S_0\to S$, i.e. $S_1=S_0\times_S S_0$, $S_2=S_0\times_S S_0\times_S S_0$ etc. Hypercovers would be great to have anyways, but they are not strictly necessary for the proof.

#### Johan Commelin (Mar 25 2021 at 09:24):

I haven't thought hard about how much this would simplify 8.19.

#### Johan Commelin (Mar 25 2021 at 09:24):

One reason I didn't think this through, is that I'm worried we'll end up with a hypercover that is canonically isomorphic to the Cech nerve

#### Peter Scholze (Mar 25 2021 at 09:24):

I think quite a bit: The statement is easier, and the reduction to finite sets is a lot easier

#### Johan Commelin (Mar 25 2021 at 09:25):

Ok, so it might be easier to transport stuff to the actual Cech nerve, instead of proving that our almost-Cech nerve is a hypercover

#### Peter Scholze (Mar 25 2021 at 09:26):

Well, as usual one can probably formalize "is a Cech cover"

#### Peter Scholze (Mar 25 2021 at 09:26):

and state 8.19 in that form (so the $=$'s above are just statements that natural maps are isomorphisms)

#### Johan Commelin (Mar 25 2021 at 09:27):

Yep, I think "is a Cech cover" is a good suggestion

#### Adam Topaz (Mar 25 2021 at 13:51):

Oh, if we only need Cech nerves that indeed simplifies a lot!

#### Adam Topaz (Mar 25 2021 at 13:56):

Do we actually need this "is Cech nerve" prop for 8.19, or can we just state 8.19 as "for any cover, the complex built out of its Cech nerve is exact..."?

#### Peter Scholze (Mar 25 2021 at 13:57):

Johan knows better, but my sense is that the "is Cech nerve" version would be much easier to use

#### Peter Scholze (Mar 25 2021 at 13:58):

Basically, the simplicial diagram one writes down is not tautologically a Cech nerve

Ah ok

#### Adam Topaz (Mar 25 2021 at 13:59):

Then yes I agree with the "is Cech nerve" approach

#### Adam Topaz (Mar 25 2021 at 17:01):

Okay, I added a little gadget that will help with constructing the Cech nerve. It's the construction that freely adds a terminal object to a category.
See the with_term branch of lean-liquid.

The idea is that we can now take fin nas a discrete category, add a terminal object freely, then take a limit over with_term (discrete (fin n)) to get the iterated fibered product needed for the construction.
The universal property of with_term (which is also in this file) shows that this with_term cconstruction is functorial in the category, so it should be straaightforward to obtain the simplicial structure we need by mapping w.r.t. morphisms in simplex_category.

#### Adam Topaz (Mar 25 2021 at 17:02):

https://github.com/leanprover-community/lean-liquid/blob/with_term/src/for_mathlib/with_term.lean

#### Johan Commelin (Mar 25 2021 at 17:41):

@Adam Topaz thanks! So far, I've been modeling the augmented cosimplicial complex as a functor from the simplex category + a separate augmentation map

#### Adam Topaz (Mar 25 2021 at 17:42):

Right, so I'm envisioning constructing the Cech nerve of an arbitrary morphism in a category with finite limits

#### Johan Commelin (Mar 25 2021 at 17:44):

For the cosimplicial lattice, I constructed it by hand, because I don't think that PolyhedralLattice has finite colimits.

#### Johan Commelin (Mar 25 2021 at 17:45):

It's just that for special morphisms you can make it work

Hmm ok

#### Adam Topaz (Mar 25 2021 at 17:49):

I can make it more explicit by saying only the diagrams involved have limits

#### Adam Topaz (Mar 25 2021 at 17:50):

Thats similar to what I did with Ran (as suggested by @Bhavik Mehta )

#### Johan Commelin (Mar 25 2021 at 17:51):

But still, there are morphisms in PolyhedralLattice for which you can't form the Cech conerve

#### Johan Commelin (Mar 25 2021 at 17:57):

Hmm, actually maybe cokernels do exist... but something like multiplication by n>0 on $\Z$ will have trivial cokernel, because all the objects are free.

#### Adam Topaz (Mar 25 2021 at 17:59):

I can still make it work, by saying specific diagrams have (co)limits

#### Johan Commelin (Mar 25 2021 at 18:00):

ooh, I misunderstood. For a moment I thought that you meant specific "shapes", but you mean only the diagrams involved in the one specific Cech nerve?

#### Johan Commelin (Mar 25 2021 at 18:00):

Yeah, I guess that can work

#### Adam Topaz (Mar 25 2021 at 18:00):

I was thinking of shapes, but we can still talk about specific diagrams if shapes dont work :)

#### Adam Topaz (Mar 25 2021 at 18:00):

I'll sketch up some code now.

#### Adam Topaz (Mar 26 2021 at 03:25):

I tried starting on the Cech nerve construction in the cech branch of lean-liquid.
I'm running into the following error

22:5: kernel failed to type check declaration 'Cech.map_cone' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
Π [_inst_1 : category C] {X B : C} (f : X ⟶ B) {C_1 : Type u} {a b : simplex_categoryᵒᵖ},
(a ⟶ b) → limits.cone (Cech_diagram f (opposite.unop a)) → limits.cone (Cech_diagram f (opposite.unop b))
elaborated value:
λ [_inst_1 : category C] {X B : C} (f : X ⟶ B) {C_1 : Type u} {a b : simplex_categoryᵒᵖ} (h : a ⟶ b)
(C_1 : limits.cone (Cech_diagram f (opposite.unop a))), sorry
nested exception message:
failed to add declaration to environment, it contains local constants


I've tried diagnosing this issue with no luck.
If I try to start building the definition of this cone anyway, I get errors like:

22:5: unknown local constant: _ffresh.0


I did a lot of pattern matching in the file for_mathlib/fan.lean in this branch. Could it be some side effect of this?

#### Johan Commelin (Mar 26 2021 at 05:14):

Is there some data higher up in the file that is sorryd?

#### Johan Commelin (Mar 26 2021 at 05:14):

I'm just guessing...

#### Adam Topaz (Mar 26 2021 at 13:00):

@Johan Commelin Nope, no sorry'd data, as far as I can tell.

#### Adam Topaz (Mar 26 2021 at 13:07):

Well, changing the type to

def Cech.map_cone {a b : simplex_category.{v}ᵒᵖ} : Π (h : a ⟶ b)
(C : limits.cone (Cech_diagram f a.unop)), limits.cone (Cech_diagram f b.unop) := λ h C, ...


#### Adam Topaz (Mar 26 2021 at 13:07):

seems to fix it.... What?

#### Kevin Buzzard (Mar 26 2021 at 13:13):

I was just looking at this. I totally agree it's bizarre :-)

#### Kevin Buzzard (Mar 26 2021 at 13:14):

It doesn't seem to be a universe issue shrug

#### Adam Topaz (Mar 26 2021 at 13:14):

Yeah, I fixed all the universes last night.

#### Adam Topaz (Mar 26 2021 at 13:14):

I think it could be an actual bug

#### Kevin Buzzard (Mar 26 2021 at 13:17):

-- bad
def Cech.map_cone {a b : simplex_category.{v}ᵒᵖ} (h : a ⟶ b)
(C : limits.cone (Cech_diagram f a.unop)) : limits.cone (Cech_diagram f b.unop) := sorry

-- good
def Cech.map_cone {a b : simplex_category.{v}ᵒᵖ} (h : a ⟶ b) :
(limits.cone (Cech_diagram f a.unop)) → limits.cone (Cech_diagram f b.unop) := sorry


#### Adam Topaz (Mar 26 2021 at 13:25):

Still more to do: functoriality in f, relax the has_limits condition, etc.

#### Kevin Buzzard (Mar 26 2021 at 13:27):

Oh! I think it's just the repetition of the variable C!

AAH!

#### Kevin Buzzard (Mar 26 2021 at 13:28):

I've never seen variable name repetition result in that error though!

#### Adam Topaz (Mar 26 2021 at 13:28):

Fixed:

abbreviation Cech.map_cone {a b : simplex_category.{v}ᵒᵖ} (h : a ⟶ b)
(CC : limits.cone (Cech.diagram f a.unop)) : limits.cone (Cech.diagram f b.unop) :=
fan.map_cone (ufin.map h.unop.to_preorder_hom) _ _ CC


Snarky bug!

#### Adam Topaz (Mar 26 2021 at 13:43):

Do we have the type category of augmented simplicial objects somewhere?

#### Johan Commelin (Mar 26 2021 at 13:44):

@Adam Topaz Nope, I don't think so

#### Adam Topaz (Mar 26 2021 at 13:45):

I would like to state the fact that the Cech nerve, considered as an augmented simplicial object, is right adjoint to the functor sending an augmented simplicial object $X_\bullet \to B$ to $X_0 \to B$.

#### Johan Commelin (Mar 26 2021 at 13:46):

So the other category will be an arrow category, right?

#### Adam Topaz (Mar 26 2021 at 13:46):

Okay, I'll just define it then. Everyone cool with the following defn?

structure augmented_simplicial_object :=
(X : simplicial_object C)
(B : C)
(f : X _[0] ⟶ B)


#### Johan Commelin (Mar 26 2021 at 13:46):

Are you using comma for that?

#### Adam Topaz (Mar 26 2021 at 13:46):

I'm using over B

#### Adam Topaz (Mar 26 2021 at 13:47):

Oh, but I guess I should use arrow or something

#### Johan Commelin (Mar 26 2021 at 13:47):

So I guess you could also use comma to define augemented_bla

Yeah true.

#### Johan Commelin (Mar 26 2021 at 13:47):

If you have the functor that sends X : simplicial_object to X_[0]

#### Adam Topaz (Mar 26 2021 at 13:47):

Once #6830 goes through, we could use structured arrows :)

#### Adam Topaz (Mar 26 2021 at 13:48):

I think this is reasonable:

structure simplicial_object.over (B : C) :=
(X : simplicial_object C)
(f : X _[0] ⟶ B)


#### Adam Topaz (Mar 26 2021 at 13:48):

But yes I should use a comma category for this.

#### Adam Topaz (Mar 26 2021 at 13:49):

Although I don't recall whether we have that $X \mapsto X_0$ is a functor...

#### Peter Scholze (Mar 26 2021 at 13:49):

Shouldn't there be a condition that all induced maps $X_i\to X_0\to B$ agree?

#### Adam Topaz (Mar 26 2021 at 13:50):

Oh yeah that's right

#### Adam Topaz (Mar 26 2021 at 13:50):

It's really a morphism from X to the constant simplicial object

Right

#### Peter Scholze (Mar 26 2021 at 13:52):

There are many variants of this simplex category; for example, allowing possibly empty finite totally ordered sets, one gets augmented simplicial objects. There's a further variant relevant for split augmented simplicial objects

#### Peter Scholze (Mar 26 2021 at 13:52):

How much extra work would it be to set up such variants?

#### Adam Topaz (Mar 26 2021 at 13:52):

Even easier:

@[derive category]
def simplicial_object.over (B : C) :=
over ((category_theory.functor.const simplex_category.{v}ᵒᵖ).obj B)


#### Adam Topaz (Mar 26 2021 at 13:55):

Yeah, I'm used to thinking of these as $B = X_{-1}$

#### Adam Topaz (Mar 26 2021 at 13:56):

I guess if we could apply this with_term construction to simplex_category\op and look at functors from that as well.

#### Johan Commelin (Mar 26 2021 at 13:56):

Peter Scholze said:

How much extra work would it be to set up such variants?

It depends on whether there is a common abstraction

#### Peter Scholze (Mar 26 2021 at 13:57):

It's all diagram categories for certain simple combinatorial test categories

#### Johan Commelin (Mar 26 2021 at 13:57):

If there isn't then it's usually just "copy-paste the file, make some adjustments, define a compatibility functor"

#### Adam Topaz (Mar 26 2021 at 13:57):

For the with_termgadget, I just came up with it yesterday so it's not battle tested.

#### Johan Commelin (Mar 26 2021 at 13:57):

@Peter Scholze I've heard of test categories a long time ago. But we certainly don't have them in mathlib

#### Adam Topaz (Mar 26 2021 at 13:58):

What is a test category?

#### Peter Scholze (Mar 26 2021 at 13:58):

Test category is just a name

#### Peter Scholze (Mar 26 2021 at 13:58):

Maybe I should have said index category

Ah ok.

#### Peter Scholze (Mar 26 2021 at 13:58):

e.g., the simplex category, the "semisimplex category", the augmented simplex category, etc.

#### Johan Commelin (Mar 26 2021 at 13:59):

https://ncatlab.org/nlab/show/test+category

#### Johan Commelin (Mar 26 2021 at 13:59):

I thought you meant actual test categories

#### Johan Commelin (Mar 26 2021 at 13:59):

they seem relevant

#### Adam Topaz (Mar 26 2021 at 13:59):

We're now discussing some stuff related to 2-categories and pseudofunctors. I guess working with such test categories would be easier if we could discuss pseudofunctors with values in CAT

#### Johan Commelin (Mar 26 2021 at 13:59):

generalizing simiplicial and cubical, etc...

#### Peter Scholze (Mar 26 2021 at 13:59):

yeah sorry I didn't mean it in that technical sense

#### Peter Scholze (Mar 26 2021 at 14:00):

There's nothing 2-categorical going on here, I think; we just have a couple of interesting combinatorial categories, and are interested in the functor categories from there

#### Johan Commelin (Mar 26 2021 at 14:00):

ok, it still seems related/relevant

#### Peter Scholze (Mar 26 2021 at 14:01):

like simplicial objects, semisimplicial objects, etc.

#### Peter Scholze (Mar 26 2021 at 14:01):

it is related, but points in a direction that's really relevant right now

#### Adam Topaz (Mar 26 2021 at 14:01):

Oh, what I mean is, for example, the construction a \mapsto (over a) is really a pseudofunctor

#### Peter Scholze (Mar 26 2021 at 14:02):

So I just wondered whether one can set up the basics on say simplicial objects in such a way that setting up semisimplicial objects, augmented simplicial objects, split augmented simplicial objects, etc., can be done without copy-pasting everything

#### Peter Scholze (Mar 26 2021 at 14:02):

hmm OK, but I think that construction is not relevant for what I am trying to say

#### Peter Scholze (Mar 26 2021 at 14:02):

(I would formalize augmented simplicial objects differently)

#### Adam Topaz (Mar 26 2021 at 14:03):

How? Don't you want to add an initial object to simplex_category?

#### Johan Commelin (Mar 26 2021 at 14:04):

Peter Scholze said:

So I just wondered whether one can set up the basics on say simplicial objects in such a way that setting up semisimplicial objects, augmented simplicial objects, split augmented simplicial objects, etc., can be done without copy-pasting everything

I think that avoiding copy-pasting would certainly be useful. But how do you characterize the index categories?

#### Adam Topaz (Mar 26 2021 at 14:04):

I guess I'm envisioning taking simplex_category, and considering something like with_initial simplex_category

#### Peter Scholze (Mar 26 2021 at 14:05):

I don't know! In principle one could just allow all index categories for some basic stuff?

#### Peter Scholze (Mar 26 2021 at 14:05):

augmented simplicial objects are indexed by the category of possibly empty finite totally ordered sets

#### Adam Topaz (Mar 26 2021 at 14:06):

Right, so we could take e.g. the category of fin n with n possibly 0 and nonincreasing maps, but then we end up with more n-1+1 = n issues when we want to relate this to the usual simplex category :sad:

#### Peter Scholze (Mar 26 2021 at 14:06):

I guess this is formally adding an initial object, yes; but I'd prefer a direct description over the one given by its relation to the simplex category (which I'd rather have as a proposition)

#### Johan Commelin (Mar 26 2021 at 14:06):

@Adam Topaz I agree that with_initial might not scale.

#### Johan Commelin (Mar 26 2021 at 14:07):

Just like we switched to group_with_zero instead of with_zero G for the target of valuations

#### Johan Commelin (Mar 26 2021 at 14:08):

If we can actually characterize useful properties of these index categories, then simplex_category can be swapped out for semisimplex_category or NonemptyFinLinOrd or FinLinOrd or whatever.

#### Adam Topaz (Mar 26 2021 at 14:08):

But (with_term J) \func Cis the category of augmented J \func C for arbitrary J

#### Johan Commelin (Mar 26 2021 at 14:08):

Maybe you want F : J \functor J' and (hF : adds_term F)

#### Adam Topaz (Mar 26 2021 at 14:09):

Ah ok, maybe that's the way to go

#### Johan Commelin (Mar 26 2021 at 14:09):

Because certainly 3 months from now someone will come along with a functor from FinLinOrd and be very disappointed that it isn't an augmented simplicial set.

#### Peter Scholze (Mar 26 2021 at 14:09):

Hmm, true. Somehow "augmented simplicial objects" are for me slightly more primitive than "augmented" "simplicial sets", but it's a borderline case.

#### Adam Topaz (Mar 26 2021 at 14:10):

What would adds_term even look like?

#### Adam Topaz (Mar 26 2021 at 14:10):

Of course you could ask for an equivalence of categories with with_term J...

#### Adam Topaz (Mar 26 2021 at 14:11):

(@Johan Commelin going back to the issue of augemented simplicial objects: Is this correct?
https://github.com/leanprover-community/lean-liquid/blob/6f0f94d46027dac3e916180d483f893550af6096/src/simplicial/alternating_face_map.lean#L18

#### Adam Topaz (Mar 26 2021 at 14:11):

That's what I was trying to model with the above structure

#### Johan Commelin (Mar 26 2021 at 14:12):

Well, that was a very lame attempt at assuming an augmented cosimplicial gadget

#### Johan Commelin (Mar 26 2021 at 14:12):

But there shouldn't be a maths problem? Right?

#### Adam Topaz (Mar 26 2021 at 14:17):

Oh I see you have these hf conditions on lemmas everywhere.

#### Adam Topaz (Mar 26 2021 at 14:25):

Well, the over approach seems to be somewhat reasonable for now:

open_locale simplicial

@[derive category, simp]
protected def over (B : C) :=
over ((category_theory.functor.const simplex_category.{v}ᵒᵖ).obj B)

namespace over

@[simps]
def forget : simplicial_object.over B ⥤ simplicial_object C := over.forget _

def to_hom : simplicial_object.over B ⥤ category_theory.over B :=
{ obj := λ X, over.mk (X.hom.app (opposite.op [0])),
map := λ X Y f, over.hom_mk (f.left.app _) }

end over


#### Adam Topaz (Mar 26 2021 at 16:23):

Okay, I added a lot more stuff to the cech file, but it still requires a LOT of cleanup and it still has a few sorries. Anyone who is interested should please feel free to push to this branch!

#### Adam Topaz (Mar 26 2021 at 16:51):

I would like to try what Peter suggested and just defining the augmented simplex category (as the category structure on nat, where n now corresponds to (fin n)), but I'm again running into issues with simplex_category being irreducible, etc.

#### Adam Topaz (Mar 26 2021 at 16:59):

I mean, this works:

long

But I'm not a fan of the line

local attribute [semireducible] simplex_category simplex_category.hom


#### Adam Topaz (Mar 26 2021 at 17:21):

There are other annoyances as well :-/
E.g. if we want to write X _[-1] for the target of the augmentation, we would need to deal with int (or maybe the subtype of integers which are at least -1), and its relationship with nat.

#### Johan Commelin (Mar 26 2021 at 17:22):

I guess the other option is to write X _[0] for the target of the automation.

#### Adam Topaz (Mar 26 2021 at 17:23):

We would still need to deal with things like $n \mapsto n+1 \mapsto (n+1)-1$

#### Johan Commelin (Mar 26 2021 at 17:23):

And so there will be an n -> n+1 shift, when moving between augmented and non-augmented

#### Johan Commelin (Mar 26 2021 at 17:24):

Where will the n-1 show up? Maybe we will just always do cases n, to split into 0 and n+1.

#### Adam Topaz (Mar 26 2021 at 17:25):

Yeah, here's what I had in mind: say that $X$ is augmented, and $Y$ is the nonaugmented thing constructed by forgetting the augmentation. We would have: Y _[n] = X _[n+1]. I guess this is ok.

#### Adam Topaz (Mar 26 2021 at 17:27):

But what if we have a simplicial object $X$, an object $B$, and a morphism froom $X$ to the constant simplicial object $B$. If we want to turn that into an augmented simplicial object $A$, we would have A _[n-1] = X _[n] for positive $n$.

#### Johan Commelin (Mar 26 2021 at 17:27):

Vice versa, if you have Y _[0] -> Z, then you can make an augmented thing using the equation compiler.

#### Adam Topaz (Mar 26 2021 at 17:28):

Oh yeah that should be okay.

#### Johan Commelin (Mar 26 2021 at 17:28):

So you define A _[0] := B and A _[n+1] := X _[n]

#### Johan Commelin (Mar 26 2021 at 17:29):

And, by the nature of the situation, whenever you want to move between the two, you will always need to know whether n = 0 or n = _ + 1

#### Johan Commelin (Mar 26 2021 at 17:29):

So you can always do cases n

#### Johan Commelin (Mar 26 2021 at 17:29):

I'm optimistic that we can get away with it here

#### Johan Commelin (Mar 26 2021 at 17:30):

But I might be naive again :see_no_evil:

#### Adam Topaz (Mar 26 2021 at 17:30):

Now another issue: We have truncated n in the nonaugmented case as the subtype $\{ i | i \le n\}$

#### Adam Topaz (Mar 26 2021 at 17:30):

Now we would want to define an augmented truncated n as $\{i | i \le n+1\}$.

#### Adam Topaz (Mar 26 2021 at 17:31):

And how would we forget the augmentation?

#### Adam Topaz (Mar 26 2021 at 17:31):

I guess what I'm going for is this: If we take Ran with respect to the opposite of the inclusion $\{-1,0\} \to \{-1,0,1,\ldots\}$, we get the Cech nerve "for free"

#### Adam Topaz (Mar 26 2021 at 17:32):

So I want to, in some sense, identify 0-truncated augmented simplicial objects with the arrow category

#### Johan Commelin (Mar 26 2021 at 17:33):

Can you do a characteristic predicate for the "arrow category = 0-truncated = whatever"?

#### Johan Commelin (Mar 26 2021 at 17:34):

I'm sorry, this sounds like a lot of new stuff :surprise:

Yeah :-/

#### Adam Topaz (Mar 26 2021 at 17:36):

(and it's all definitions...)

#### Adam Topaz (Mar 26 2021 at 17:38):

On the other hand, if we use with_trunc (simplex_category.truncated n)\op, and map with respect to (simplex_category.truncated n)\op \func (simplex_category)\op, we get with_trunc (simplex_category.truncated n)\op \func with_trunc (simplex_category)\op.

#### Adam Topaz (Mar 26 2021 at 17:39):

(sorry, replace with_trunc with with_term above :) )

#### Adam Topaz (Mar 26 2021 at 17:46):

E.g.

import .with_term
import algebraic_topology.simplicial_object

namespace simplicial_object

open category_theory

universes v u

variables (C : Type u) [category.{v} C]

@[derive category]
def augmented := (with_term simplex_categoryᵒᵖ) ⥤ C

@[derive category]
def augmented.truncated (n : ℕ) := (with_term (simplex_category.truncated n)ᵒᵖ) ⥤ C

noncomputable
def augmented.truncated.trunc {n : ℕ} : augmented C ⥤ augmented.truncated C n :=
(whiskering_left _ _ _).obj (with_term.map simplex_category.truncated.inclusion.op)

end simplicial_object


#### Scott Morrison (Mar 27 2021 at 05:10):

lemma is_iso_π_initial {J : Type v} [small_category J] {C : Type u₁} [category.{v} C] {j : J}