Zulip Chat Archive

Stream: condensed mathematics

Topic: Simplicial stuff


view this post on Zulip 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 :)

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:15):

@Scott Morrison do you have a good idea?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:17):

Right, so also for laaaarge categories (-;

view this post on Zulip Adam Topaz (Mar 17 2021 at 21:18):

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

view this post on Zulip Adam Topaz (Mar 17 2021 at 21:18):

or LARGE\mathfrak{LARGE}

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:18):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:20):

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

view this post on Zulip 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...

view this post on Zulip Adam Topaz (Mar 17 2021 at 21:21):

This is all in branch#simplicial_cosk

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip Adam Topaz (Mar 17 2021 at 21:22):

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

view this post on Zulip Peter Scholze (Mar 17 2021 at 21:22):

OK, great

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:22):

But in Lean universes are not cumulative.

view this post on Zulip 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: )

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:23):

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

view this post on Zulip Peter Scholze (Mar 17 2021 at 21:23):

I'd guess so

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:24):

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

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 17 2021 at 21:24):

Aha, OK...

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:25):

And index categories for limits must live in Type v.

view this post on Zulip 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"

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:26):

And that's annoying.

view this post on Zulip Peter Scholze (Mar 17 2021 at 21:26):

Oh, that's annoying indeed.

view this post on Zulip Peter Scholze (Mar 17 2021 at 21:26):

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:26):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 17 2021 at 21:26):

We have this ulift thing

view this post on Zulip 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 }

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:28):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:30):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:33):

I somehow want to write

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 17 2021 at 21:34):

Oh I see. yes of course.

view this post on Zulip Adam Topaz (Mar 17 2021 at 21:35):

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

view this post on Zulip Adam Topaz (Mar 17 2021 at 21:35):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Mar 17 2021 at 21:41):

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

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:42):

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:43):

Somehow, J should be small, relative to C

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:43):

where does the inequality come up?

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:43):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:44):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:44):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:45):

I think u is unrelated to what we are doing.

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:45):

You said you need v <= u

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:45):

so apparently u needs to be large

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:45):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:46):

what happens if the inequality fails?

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:46):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:46):

Oh there are two v's?

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:46):

There aren't in that snippet

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:46):

Currently v1 = v2

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:47):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:50):

So that should just become the new definition of simplex_category?

view this post on Zulip Scott Morrison (Mar 17 2021 at 21:50):

Yes.

view this post on Zulip Adam Topaz (Mar 17 2021 at 21:50):

That sounds good to me.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 17 2021 at 21:53):

There's already some notation:

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:53):

Can we have open_locale simplicial enable that?

view this post on Zulip Scott Morrison (Mar 17 2021 at 21:53):

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

view this post on Zulip Scott Morrison (Mar 17 2021 at 21:53):

there's already localized notation in sSet

view this post on Zulip Scott Morrison (Mar 17 2021 at 21:54):

perhaps we could combine those into one locale

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 17 2021 at 21:56):

I'm starting the refactor now @Scott Morrison.

view this post on Zulip 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)

view this post on Zulip 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:.)

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 17 2021 at 21:58):

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

view this post on Zulip Peter Scholze (Mar 17 2021 at 21:59):

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

view this post on Zulip Peter Scholze (Mar 17 2021 at 21:59):

But I put some nasty cardinal bounds in to justify this

view this post on Zulip Peter Scholze (Mar 17 2021 at 22:00):

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 22:01):

Thanks for the example

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 17 2021 at 23:36):

I pushed a commit making simplex_category irreducible.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 18 2021 at 12:11):

Looking forward to it!

view this post on Zulip Johan Commelin (Mar 18 2021 at 12:34):

@Bhavik MehtaEager to know what you come up with!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 18 2021 at 16:15):

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

view this post on Zulip 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] :=

view this post on Zulip Adam Topaz (Mar 18 2021 at 16:16):

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

view this post on Zulip Peter Scholze (Mar 18 2021 at 16:17):

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

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 18 2021 at 16:18):

Ah!

view this post on Zulip 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

view this post on Zulip 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 (-;

view this post on Zulip Peter Scholze (Mar 18 2021 at 16:19):

In what range do they live, typically?

view this post on Zulip Johan Commelin (Mar 18 2021 at 16:19):

0 -- 1024

view this post on Zulip Adam Topaz (Mar 18 2021 at 16:19):

not sure exactly, but 1000 is high

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 18 2021 at 16:21):

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

view this post on Zulip Adam Topaz (Mar 18 2021 at 16:21):

(so 50 is meant to be very low)

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 16:32):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 16:35):

but

infixr `⋆`:1000000 := has_mul.mul

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

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Mar 18 2021 at 16:38):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 18 2021 at 22:02):

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?

view this post on Zulip Adam Topaz (Mar 18 2021 at 22:05):

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

view this post on Zulip Adam Topaz (Mar 18 2021 at 22:33):

#6761

view this post on Zulip 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.

view this post on Zulip 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.

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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 19 2021 at 20:22):

I'm trying but I'm not getting anywhere

view this post on Zulip Adam Topaz (Mar 19 2021 at 20:22):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 19 2021 at 20:24):

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

view this post on Zulip Adam Topaz (Mar 19 2021 at 20:24):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 19 2021 at 20:27):

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

view this post on Zulip Adam Topaz (Mar 19 2021 at 20:29):

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

view this post on Zulip Kevin Buzzard (Mar 19 2021 at 21:01):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 20 2021 at 05:02):

Yeah this is probably some sort of Kan extension.

view this post on Zulip Adam Topaz (Mar 20 2021 at 05:02):

And yeah good point about the cosimplicial objects.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Bhavik Mehta (Mar 20 2021 at 14:24):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:05):

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

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:05):

Or does the Kan machine solve your troubles?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:08):

The latter. But it's already done.

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:08):

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

view this post on Zulip Adam Topaz (Mar 20 2021 at 18:10):

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

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:13):

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

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:13):

This is the "end goal" of the simplicial stuff

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 20 2021 at 18:14):

Sounds good.

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:15):

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

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:15):

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

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:15):

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

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:16):

actually, let me just do it right now

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 20 2021 at 18:47):

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

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:49):

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

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:49):

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

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:49):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 22 2021 at 16:39):

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

view this post on Zulip Bhavik Mehta (Mar 22 2021 at 16:39):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Mar 22 2021 at 17:00):

Nope and there absolutely should be

view this post on Zulip Adam Topaz (Mar 22 2021 at 17:00):

It's similar to your thingy2 :)

view this post on Zulip Bhavik Mehta (Mar 22 2021 at 17:00):

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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Mar 23 2021 at 00:40):

Yeah codensity monads would be cool to have

view this post on Zulip 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 S0SS_0\to S, i.e. S1=S0×SS0S_1=S_0\times_S S_0, S2=S0×SS0×SS0S_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.

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:24):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 25 2021 at 09:26):

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

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Mar 25 2021 at 09:27):

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

view this post on Zulip Adam Topaz (Mar 25 2021 at 13:51):

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

view this post on Zulip 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..."?

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 25 2021 at 13:58):

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

view this post on Zulip Adam Topaz (Mar 25 2021 at 13:58):

Ah ok

view this post on Zulip Adam Topaz (Mar 25 2021 at 13:59):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 25 2021 at 17:02):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 25 2021 at 17:45):

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

view this post on Zulip Adam Topaz (Mar 25 2021 at 17:49):

Hmm ok

view this post on Zulip Adam Topaz (Mar 25 2021 at 17:49):

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

view this post on Zulip Adam Topaz (Mar 25 2021 at 17:50):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 17:51):

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

view this post on Zulip Johan Commelin (Mar 25 2021 at 17:57):

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

view this post on Zulip Adam Topaz (Mar 25 2021 at 17:59):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 25 2021 at 18:00):

Yeah, I guess that can work

view this post on Zulip 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 :)

view this post on Zulip Adam Topaz (Mar 25 2021 at 18:00):

I'll sketch up some code now.

view this post on Zulip 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

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?

view this post on Zulip Johan Commelin (Mar 26 2021 at 05:14):

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

view this post on Zulip Johan Commelin (Mar 26 2021 at 05:14):

I'm just guessing...

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:00):

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

view this post on Zulip 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, ...

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:07):

seems to fix it.... What?

view this post on Zulip Kevin Buzzard (Mar 26 2021 at 13:13):

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

view this post on Zulip Kevin Buzzard (Mar 26 2021 at 13:14):

It doesn't seem to be a universe issue shrug

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:14):

Yeah, I fixed all the universes last night.

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:14):

I think it could be an actual bug

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:25):

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

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:25):

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

view this post on Zulip Kevin Buzzard (Mar 26 2021 at 13:27):

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

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:27):

AAH!

view this post on Zulip Kevin Buzzard (Mar 26 2021 at 13:28):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 26 2021 at 13:28):

Snarky bug!

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:43):

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

view this post on Zulip Johan Commelin (Mar 26 2021 at 13:44):

@Adam Topaz Nope, I don't think so

view this post on Zulip 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 XBX_\bullet \to B to X0BX_0 \to B.

view this post on Zulip Johan Commelin (Mar 26 2021 at 13:46):

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

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Mar 26 2021 at 13:46):

Are you using comma for that?

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:46):

I'm using over B

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:47):

Oh, but I guess I should use arrow or something

view this post on Zulip Johan Commelin (Mar 26 2021 at 13:47):

So I guess you could also use comma to define augemented_bla

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:47):

Yeah true.

view this post on Zulip Johan Commelin (Mar 26 2021 at 13:47):

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

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:47):

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

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:48):

But yes I should use a comma category for this.

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:49):

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

view this post on Zulip Peter Scholze (Mar 26 2021 at 13:49):

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

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:50):

Oh yeah that's right

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:50):

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

view this post on Zulip Peter Scholze (Mar 26 2021 at 13:50):

Right

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 26 2021 at 13:52):

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

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:55):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 26 2021 at 13:57):

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

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:58):

What is a test category?

view this post on Zulip Peter Scholze (Mar 26 2021 at 13:58):

Test category is just a name

view this post on Zulip Peter Scholze (Mar 26 2021 at 13:58):

Maybe I should have said index category

view this post on Zulip Adam Topaz (Mar 26 2021 at 13:58):

Ah ok.

view this post on Zulip Peter Scholze (Mar 26 2021 at 13:58):

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

view this post on Zulip Johan Commelin (Mar 26 2021 at 13:59):

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

view this post on Zulip Johan Commelin (Mar 26 2021 at 13:59):

I thought you meant actual test categories

view this post on Zulip Johan Commelin (Mar 26 2021 at 13:59):

they seem relevant

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 26 2021 at 13:59):

generalizing simiplicial and cubical, etc...

view this post on Zulip Peter Scholze (Mar 26 2021 at 13:59):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 26 2021 at 14:00):

ok, it still seems related/relevant

view this post on Zulip Peter Scholze (Mar 26 2021 at 14:01):

like simplicial objects, semisimplicial objects, etc.

view this post on Zulip Peter Scholze (Mar 26 2021 at 14:01):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 26 2021 at 14:02):

(I would formalize augmented simplicial objects differently)

view this post on Zulip Adam Topaz (Mar 26 2021 at 14:03):

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

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Mar 26 2021 at 14:04):

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

view this post on Zulip 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?

view this post on Zulip Peter Scholze (Mar 26 2021 at 14:05):

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

view this post on Zulip 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:

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Mar 26 2021 at 14:06):

@Adam Topaz I agree that with_initial might not scale.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 26 2021 at 14:08):

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

view this post on Zulip Johan Commelin (Mar 26 2021 at 14:08):

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

view this post on Zulip Adam Topaz (Mar 26 2021 at 14:09):

Ah ok, maybe that's the way to go

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 26 2021 at 14:10):

What would adds_term even look like?

view this post on Zulip Adam Topaz (Mar 26 2021 at 14:10):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 26 2021 at 14:11):

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

view this post on Zulip Johan Commelin (Mar 26 2021 at 14:12):

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

view this post on Zulip Johan Commelin (Mar 26 2021 at 14:12):

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

view this post on Zulip Adam Topaz (Mar 26 2021 at 14:17):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Adam Topaz (Mar 26 2021 at 16:50):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 26 2021 at 17:22):

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

view this post on Zulip Adam Topaz (Mar 26 2021 at 17:23):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 26 2021 at 17:25):

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

view this post on Zulip Adam Topaz (Mar 26 2021 at 17:27):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 26 2021 at 17:28):

Oh yeah that should be okay.

view this post on Zulip Johan Commelin (Mar 26 2021 at 17:28):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 26 2021 at 17:29):

So you can always do cases n

view this post on Zulip Johan Commelin (Mar 26 2021 at 17:29):

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

view this post on Zulip Johan Commelin (Mar 26 2021 at 17:30):

But I might be naive again :see_no_evil:

view this post on Zulip Adam Topaz (Mar 26 2021 at 17:30):

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

view this post on Zulip Adam Topaz (Mar 26 2021 at 17:30):

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

view this post on Zulip Adam Topaz (Mar 26 2021 at 17:31):

And how would we forget the augmentation?

view this post on Zulip 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}{1,0,1,}\{-1,0\} \to \{-1,0,1,\ldots\}, we get the Cech nerve "for free"

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 26 2021 at 17:33):

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

view this post on Zulip Johan Commelin (Mar 26 2021 at 17:34):

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

view this post on Zulip Adam Topaz (Mar 26 2021 at 17:34):

Yeah :-/

view this post on Zulip Adam Topaz (Mar 26 2021 at 17:36):

(and it's all definitions...)

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 26 2021 at 17:39):

(sorry, replace with_trunc with with_term above :) )

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 27 2021 at 05:10):

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


Last updated: May 09 2021 at 21:10 UTC