Zulip Chat Archive

Stream: new members

Topic: sSet as a category


Fedor Pavutnitskiy (May 04 2022 at 12:46):

I'm trying to construct some colimits in sSet. This is a minimal code that gives me trouble:

import algebraic_topology.simplicial_set
import category_theory.limits.shapes.products

open_locale simplicial

open category_theory.limits

#check sigma.ι (λ n : , Δ[n])

Here sigma.ι is an inclusion map to the coproduct of the standard simplices. Lean says

failed to synthesize type class instance for
 category_theory.category sSet

although #print instances category_theory.category indicates sSet.large_category : category_theory.large_category sSet. Any ideas, what is happening ? I also tried to fix the universe level u and use sSet.standard_simplex.{u}.obj (simplex_category.mk n) instead of Δ[n], but the problem remains.

Kevin Buzzard (May 04 2022 at 12:52):

Your code compiles for me without errors (with mathlib from April 26th)

Reid Barton (May 04 2022 at 12:58):

From reading the documentation/source, I think Δ[n] can only be an object of sSet.{0}.

Fedor Pavutnitskiy (May 04 2022 at 13:11):

Reid Barton said:

From reading the documentation/source, I think Δ[n] can only be an object of sSet.{0}.

Thanks, sSet.{0} is fine by me and #check sigma.ι (λ n : ℕ, (sSet.standard_simplex.{0}.obj (simplex_category.mk n))) works. But this notation is tedious though. Any ideas why the original Δ[n] not working ?

Reid Barton (May 04 2022 at 13:14):

I haven't tested but Kevin says it works for him. Try adding set pp.all true and see what the error message is then.

Yaël Dillies (May 04 2022 at 13:14):

Should

localized "notation `Δ[`n`]` := sSet.standard_simplex.obj (simplex_category.mk n)" in simplicial

instead be

localized "notation `Δ[`n`]` := sSet.{0}.standard_simplex.obj (simplex_category.mk n)" in simplicial

Reid Barton (May 04 2022 at 13:17):

I think sSet.standard_simplex has no universe parameter.

Fedor Pavutnitskiy (May 04 2022 at 13:17):

Kevin Buzzard said:

Your code compiles for me without errors (with mathlib from April 26th)

Thanks Kevin, I ran leanproject upgrade-mathlib and now it works indeed. But also now the line #check sigma.ι (λ n : ℕ, (sSet.standard_simplex.{0}.obj (simplex_category.mk n))) not working :thinking:

Reid Barton (May 04 2022 at 13:19):

My latest message explains that--I guess there used to be a universe parameter in sSet.standard_simplex, but something changed.

Yaël Dillies (May 04 2022 at 13:21):

Ah I know what changed! simplex_category is not universe polymorphic anymore since Joël Riou's refactor.

Fedor Pavutnitskiy (May 04 2022 at 13:21):

Reid Barton said:

I think sSet.standard_simplex has no universe parameter.

Agreed, sSet.{0}.standard_simplexseems more reasonable, but before the update it worked with sSet.standard_simplex.{0} though. Now neither work.


Yaël Dillies (May 04 2022 at 13:22):

cf #13183

Fedor Pavutnitskiy (May 04 2022 at 13:22):

sSet.{0}.standard_simplex gives unknown identifier 'sSet.standard_simplex' :upside_down:

Yaël Dillies (May 04 2022 at 13:23):

What if you insert the universe parameter elsewhere?

Fedor Pavutnitskiy (May 04 2022 at 13:24):

sSet.standard_simplex.{0} gives incorrect number of universe levels parameters for 'sSet.standard_simplex', #0 expected, #1provided which is reasonable. Without the universe parameter it works fine.

Fedor Pavutnitskiy (May 04 2022 at 13:24):

Yaël Dillies said:

cf #13183

:+1: nice

Fedor Pavutnitskiy (May 04 2022 at 13:25):

Ok, thank you all for the help and the clarifications.


Last updated: Dec 20 2023 at 11:08 UTC