Simplicial stuff

Stream: condensed mathematics

[Adam Topaz]

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]

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

@Scott Morrison do you have a good idea?

[Adam Topaz]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Johan Commelin]

Right, so also for laaaarge categories (-;

[Adam Topaz]

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

[Adam Topaz]

or $\mathfrak{LARGE}$

[Johan Commelin]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Adam Topaz]

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]

This is all in branch#simplicial_cosk

[Johan Commelin]

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

[Peter Scholze]

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]

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

[Peter Scholze]

OK, great

[Johan Commelin]

But in Lean universes are not cumulative.

[Adam Topaz]

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

[Johan Commelin]

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

[Peter Scholze]

I'd guess so

[Johan Commelin]

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

[Johan Commelin]

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

[Peter Scholze]

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

[Peter Scholze]

Aha, OK...

[Johan Commelin]

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]

And index categories for limits must live in Type v.

[Johan Commelin]

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

[Johan Commelin]

And that's annoying.

[Peter Scholze]

Oh, that's annoying indeed.

[Peter Scholze]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Adam Topaz]

We have this ulift thing

[Adam Topaz]

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]

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]

@Peter Scholze Do you know of a construction in mathematics that iterates "universe bumps"?

[Johan Commelin]

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]

So now you can imagine that you look at Spec (some_cohomology_ring) or so...

[Johan Commelin]

But I don't really know of a natural example where you would want to iterate this process arbitrarily often.

[Mario Carneiro]

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]

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]

@Mario Carneiro But that doesn't allow quantifying over all u1 such that max u1 u2 = u2

[Johan Commelin]

I somehow want to write

def foobar {v} {v \le u} (I : Type v) ...

[Kevin Buzzard]

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

Oh I see. yes of course.

[Adam Topaz]

Well, then you can iterate the classifying space construction of an abelian group

[Adam Topaz]

(which is involved in the second step of my example)

[Kevin Buzzard]

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]

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

But what if v changes in another definition later on, while u stays the same?

[Johan Commelin]

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

Currently J : Type v and [category.{v} C]

[Johan Commelin]

Somehow, J should be small, relative to C

[Mario Carneiro]

where does the inequality come up?

[Mario Carneiro]

[category.{v (max v u)} C]

[Johan Commelin]

Well, we would like to be able to consider both J : Type v and J : Type 0

[Johan Commelin]

And if v happens to be 2, then J : Type 1 should also work

[Mario Carneiro]

or actually just variables {C : Type (max v u)} [category.{v} C]

[Mario Carneiro]

I mean, why does the inequality need to exist? Why can't you use a small u

[Johan Commelin]

I think u is unrelated to what we are doing.

[Mario Carneiro]

You said you need v <= u

[Mario Carneiro]

so apparently u needs to be large

[Johan Commelin]

I want J : Type v1 and [category.{v2} C] and v1 <= v2

[Mario Carneiro]

what happens if the inequality fails?

[Johan Commelin]

And C : Type u, but that doesn't matter.

[Mario Carneiro]

Oh there are two v's?

[Mario Carneiro]

There aren't in that snippet

[Johan Commelin]

Currently v1 = v2

[Johan Commelin]

But that causes trouble, because now we can take limits over simplex_category : Type 0

[Adam Topaz]

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]

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]

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]

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

[Johan Commelin]

So that should just become the new definition of simplex_category?

[Scott Morrison]

Yes.

[Adam Topaz]

That sounds good to me.

[Johan Commelin]

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]

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]

There's already some notation:

local notation `[`n`]` := mk n

[Johan Commelin]

Can we have open_locale simplicial enable that?

[Scott Morrison]

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

[Scott Morrison]

there's already localized notation in sSet

[Scott Morrison]

perhaps we could combine those into one locale

[Scott Morrison]

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]

I'm starting the refactor now @Scott Morrison.

[Adam Topaz]

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]

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

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]

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

[Peter Scholze]

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

[Peter Scholze]

But I put some nasty cardinal bounds in to justify this

[Peter Scholze]

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

[Johan Commelin]

Thanks for the example

[Adam Topaz]

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

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

[Scott Morrison]

I pushed a commit making simplex_category irreducible.

[Scott Morrison]

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

[Bhavik Mehta]

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]

Looking forward to it!

[Johan Commelin]

@Bhavik MehtaEager to know what you come up with!

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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]

(see https://github.com/leanprover-community/mathlib/blob/d2e2236a441cc95572885406a06ee482e1a8c632/src/algebraic_topology/simplicial_object.lean#L35 )

[Adam Topaz]

This way the face maps look nice:

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

[Adam Topaz]

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

[Peter Scholze]

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

[Adam Topaz]

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

[Peter Scholze]

Ah!

[Adam Topaz]

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

[Johan Commelin]

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]

In what range do they live, typically?

[Johan Commelin]

0 -- 1024

[Adam Topaz]

not sure exactly, but 1000 is high

[Johan Commelin]

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

[Adam Topaz]

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

[Adam Topaz]

(so 50 is meant to be very low)

[Kevin Buzzard]

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

[Yakov Pechersky]

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]

but

infixr `⋆`:1000000 := has_mul.mul

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

[Adam Topaz]

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

[Adam Topaz]

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

[Yakov Pechersky]

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]

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

[Scott Morrison]

Adam Topaz said:

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

Is this ready to PR?

[Adam Topaz]

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

[Adam Topaz]

#6761

[Adam Topaz]

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

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

Take a look at the following goal:
https://github.com/leanprover-community/mathlib/blob/ec1b65487b40942baa21bf2dc3dd0a337e4f8f83/src/algebraic_topology/simplicial_object.lean#L170

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]

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]

I'm trying but I'm not getting anywhere

[Adam Topaz]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

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]

Yeah this is probably some sort of Kan extension.

[Adam Topaz]

And yeah good point about the cosimplicial objects.

[Adam Topaz]

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

[Adam Topaz]

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

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]

Adam Topaz said:

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]

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

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

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]

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]

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

[Johan Commelin]

Or does the Kan machine solve your troubles?

[Adam Topaz]

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

[Adam Topaz]

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

[Johan Commelin]

The latter. But it's already done.

[Johan Commelin]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Johan Commelin]

This is the "end goal" of the simplicial stuff

[Johan Commelin]

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

[Adam Topaz]

Sounds good.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

actually, let me just do it right now

[Johan Commelin]

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

[Adam Topaz]

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]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Adam Topaz]

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]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Adam Topaz]

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]

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

Nope and there absolutely should be

[Adam Topaz]

It's similar to your thingy2 :)

[Bhavik Mehta]

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

[Adam Topaz]

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

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]

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]

Yeah codensity monads would be cool to have

[Peter Scholze]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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

[Peter Scholze]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Peter Scholze]

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

[Adam Topaz]

Ah ok

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Johan Commelin]

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

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

[Johan Commelin]

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

[Johan Commelin]

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

[Adam Topaz]

Hmm ok

[Adam Topaz]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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]

Yeah, I guess that can work

[Adam Topaz]

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

[Adam Topaz]

I'll sketch up some code now.

[Adam Topaz]

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

on the following line:
https://github.com/leanprover-community/lean-liquid/blob/0590ca0c74e0cb60530da104ee75784c941d4fd4/src/for_mathlib/cech.lean#L22

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]

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

[Johan Commelin]

I'm just guessing...

[Adam Topaz]

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

[Adam Topaz]

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]

seems to fix it.... What?

[Kevin Buzzard]

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

[Kevin Buzzard]

It doesn't seem to be a universe issue shrug

[Adam Topaz]

Yeah, I fixed all the universes last night.

[Adam Topaz]

I think it could be an actual bug

[Kevin Buzzard]

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

Well, here's the Cech nerve:
https://github.com/leanprover-community/lean-liquid/blob/44ab8925dc1d44c584204941e681dd8741267743/src/for_mathlib/cech.lean#L35

[Adam Topaz]

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

[Kevin Buzzard]

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

[Adam Topaz]

AAH!

[Kevin Buzzard]

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

[Adam Topaz]

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

[Johan Commelin]

Snarky bug!

[Adam Topaz]

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

[Johan Commelin]

@Adam Topaz Nope, I don't think so

[Adam Topaz]

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]

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

[Adam Topaz]

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]

Are you using comma for that?

[Adam Topaz]

I'm using over B

[Adam Topaz]

Oh, but I guess I should use arrow or something

[Johan Commelin]

So I guess you could also use comma to define augemented_bla

[Adam Topaz]

Yeah true.

[Johan Commelin]

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

[Adam Topaz]

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

[Adam Topaz]

I think this is reasonable:

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

[Adam Topaz]

But yes I should use a comma category for this.

[Adam Topaz]

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

[Peter Scholze]

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

[Adam Topaz]

Oh yeah that's right

[Adam Topaz]

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

[Peter Scholze]

Right

[Peter Scholze]

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]

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

[Adam Topaz]

Even easier:

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

[Adam Topaz]

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

[Adam Topaz]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Adam Topaz]

What is a test category?

[Peter Scholze]

Test category is just a name

[Peter Scholze]

Maybe I should have said index category

[Adam Topaz]

Ah ok.

[Peter Scholze]

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

[Johan Commelin]

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

[Johan Commelin]

I thought you meant actual test categories

[Johan Commelin]

they seem relevant

[Adam Topaz]

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]

generalizing simiplicial and cubical, etc...

[Peter Scholze]

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

[Peter Scholze]

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]

ok, it still seems related/relevant

[Peter Scholze]

like simplicial objects, semisimplicial objects, etc.

[Peter Scholze]

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

[Adam Topaz]

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

[Peter Scholze]

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]

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

[Peter Scholze]

(I would formalize augmented simplicial objects differently)

[Adam Topaz]

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

[Johan Commelin]

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]

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

[Peter Scholze]

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

[Peter Scholze]

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

[Adam Topaz]

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]

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]

@Adam Topaz I agree that with_initial might not scale.

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Adam Topaz]

Ah ok, maybe that's the way to go

[Johan Commelin]

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]

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

[Adam Topaz]

What would adds_term even look like?

[Adam Topaz]

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

[Adam Topaz]

(@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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Adam Topaz]

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]

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]

TBH, I'm not happy about this construction :-/ it feels clunky

[Adam Topaz]

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]

I mean, this works:

long

import algebraic_topology.simplex_category

namespace simplex_category

local attribute [semireducible] simplex_category simplex_category.hom

open category_theory

def augmented := ulift ℕ

namespace augmented

instance : small_category augmented :=
{ hom := λ a b, ulift (fin a.down →ₘ fin b.down),
  id := λ a, ulift.up preorder_hom.id,
  comp := λ a b c f g, ulift.up (g.down.comp f.down) }

def incl : simplex_category ⥤ augmented :=
{ obj := λ x,
    match x with
    | ulift.up a := ulift.up (a + 1)
    end,
  map := λ a b f,
    match a, b, f with
    | ulift.up a, ulift.up b, ulift.up f := ulift.up f
    end }

end augmented

end simplex_category

But I'm not a fan of the line

local attribute [semireducible] simplex_category simplex_category.hom

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Adam Topaz]

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]

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]

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

[Adam Topaz]

Oh yeah that should be okay.

[Johan Commelin]

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

[Johan Commelin]

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]

So you can always do cases n

[Johan Commelin]

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

[Johan Commelin]

But I might be naive again :see_no_evil:

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

And how would we forget the augmentation?

[Adam Topaz]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Adam Topaz]

Yeah :-/

[Adam Topaz]

(and it's all definitions...)

[Adam Topaz]

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]

(sorry, replace with_trunc with with_term above :) )

[Adam Topaz]

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]

Adam Topaz said:

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

#6908