sSet as a category

Stream: new members

[Fedor Pavutnitskiy]

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]

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

[Reid Barton]

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

[Fedor Pavutnitskiy]

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]

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]

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]

I think sSet.standard_simplex has no universe parameter.

[Fedor Pavutnitskiy]

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]

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

[Yaël Dillies]

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

[Fedor Pavutnitskiy]

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]

cf #13183

[Fedor Pavutnitskiy]

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

[Yaël Dillies]

What if you insert the universe parameter elsewhere?

[Fedor Pavutnitskiy]

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]

Yaël Dillies said:

cf #13183

:+1: nice

[Fedor Pavutnitskiy]

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