terminology for co/skeleton functors

Stream: Infinity-Cosmos

[Emily Riehl]

@Mario Carneiro and I have an open PR #16781 under review. One suggestion made by @Joël Riou is to introduce terminology for the co/skeleton functors. It's not clear to me which functors those should be and so I wanted to consult with creators/users like @Kim Morrison @Adam Topaz @Johan Commelin.

[Emily Riehl]

I'm aware of two conventions in the literature, where
(i) skeleton := lan (Truncated.inclusion (n := n)).op and where
(ii) skeleton := truncation.{u} n >>> lan (Truncated.inclusion).op.

In the current draft version of the SimplicialSets file, (i) would be more useful because we prove lan (Truncated.inclusion (n := n)).op is a fully faithful left adjoint, during which it might be useful to have a name for that functor.

But I suspect definition (ii) would be more useful to folks interacting with simplicial sets in Mathlib.

What do others think? (Whatever we choose, "coskeleton" should be defined dually.)

[Adam Topaz]

@Jack McKoen should probably weigh in here as well, since he has been working on skeleton functors.

[Emily Riehl]

Note the current version of mathlib actually uses sk to refer to the functor I've called "truncation" above. I think this should be called "truncation" and so far no one has objected ;)

[Adam Topaz]

You're right, it should indeed be called truncation. As I understand it, Jack has been working on defining the skeleton in terms of subsets of the types of n-simplices of a given simplicial set.

[Adam Topaz]

But I think his result is again a full blown simplicial set, not a truncated one.

[Jack McKoen]

Adam Topaz said:

As I understand it, Jack has been working on defining the skeleton in terms of subsets of the types of n-simplices of a given simplicial set.

That's right, so I have no overlap with #16781 just yet.

[Adam Topaz]

Using lan/ran is indeed convenient as that gives you the adjunctions for free.

[Emily Riehl]

Do you have a terminological preference, though? Should sk n be an endofunctor of SSet or a functor from SSet.truncation n to SSet?

[Adam Topaz]

Oh good question, I think it should be from SSet to itself.

[Emily Riehl]

This was my thinking too. Then e.g. @Jack McKoen could prove that under certain conditions X is n-skeletal meaning the counit map sk n X -> X is an iso.

[Adam Topaz]

But I think that giving some name to the functors from the truncated categories is also worthwhile? I guess "inductive" and "coinductive" are off the table ? :)

[Emily Riehl]

We also have the adjunction sk n -| cosk n as endofunctors of SSet. This can be useful independently of the adjucntions above.

[Emily Riehl]

In the literature both functors are called sk n with context to disambiguate ;)

[Adam Topaz]

I guess the same can be done here... one in the SSet namespace and one in the SSet.Truncated namespace.

[Adam Topaz]

The latter should probably be protected.

[Emily Riehl]

That's a good idea.

[Emily Riehl]

Though could you explain exactly what "protected" means?

[Mario Carneiro]

the protected keyword on a declaration means it can't be used un-namespaced, open ignores it

[Mario Carneiro]

this can prevent name clashes if you open lots of things

[Emily Riehl]

Adam Topaz said:

I guess the same can be done here... one in the SSet namespace and one in the SSet.Truncated namespace.

I've just pushed a revision to #16781 implementing this suggestion in case anyone wants to check it out (in the SimplicialSet file).

[Joël Riou]

If it is applicable, I would suggest definitions of (co)skeleton should be done for simplicial objects in a general category (under the suitable typeclass assumptions under which lan/ran are defined) rather than for SSet only.
(Also, in the case of simplicial sets, the notion of split simplicial objects https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicTopology/SplitSimplicialObject.html may be helpful in a detailed analysis of the skeleton, using the notion of nondegenerate simplices.)

[Emily Riehl]

Interesting. @Jack McKoen is this the sort of thing you've been working on/with?

I'm used to the term "split simplicial object" referring to (augmented) simplicial objects that extend along canonical maps  Δ → Δ^+ → Δ^⊥ or Δ → Δ^+ → Δ^⊤. Sometimes these maps are called "extra degeneracies". See eg Kerodon.

[Joël Riou]

I have also formalized extradegeneracies https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicTopology/ExtraDegeneracy.html (this is used in the formalization of group cohomology), but I was using "split" in the sense of https://stacks.math.columbia.edu/tag/017O
All simplicial sets are split in that sense, and it seems to me that the skeletal filtration of a split simplicial object can be described easily in terms of a splitting.

[Jack McKoen]

@Emily Riehl this is closer to what I've been working on. I've been formalising most of https://kerodon.net/tag/0010 (on the skeletal filtration). In particular I need this construction