standardSimplex → stdSimplex

Stream: Infinity-Cosmos

[Nick Ward]

A small heads up: #20974 renames SSet.standardSimplex to SSet.stdSimplex. Relatedly, #20954 makes possible the notation stdSimplex.δ 0 in place of stdSimplex.map (SimplexCategory.δ 0).

[Joël Riou]

As these files are going to expand significantly in a near future, in #21025, I am splitting SimplicialSet.Basic, creating three new files StdSimplex, Boundary and Horn.

[Emily Riehl]

Great, I like this.

[Joël Riou]

In #21090, I refactor the definitions of the boundary of the standard simplex and the horns. ∂Δ[n] and Λ[n, i] shall be a subcomplexes of Δ[n]. This refactor only adds the necessary Subpresheaf API in order to make mathlib compile, but there will be more later.

[Nick Ward]

#PR reviews > #21741 -> #21748: presentation of `SimplexCategory` might be interesting to people here.

[Emily Riehl]

Congrats @Robin Carlier! FYI to @Amelia Livingston.

[Emily Riehl]

@Joël Riou a question about using some of the changes in #21090, which we just merged into the InfinityCosmos repository. In a file written by @Jack McKoen, he uses SSet.boundaryInclusion which I see is now depreciated in favor of SSet.boundary. See here

/-- an inductive type defining boundary inclusions as a class of morphisms. Used to take advantage
  of the `MorphismProperty` API. -/
inductive BoundaryInclusion : {X Y : SSet} → (X ⟶ Y) → Prop
  | mk n : BoundaryInclusion (boundaryInclusion n)

/-- The class of all boundary inclusions. -/
def BoundaryInclusions : MorphismProperty SSet := fun _ _ p ↦ BoundaryInclusion p

On the other hand, mathlib seems to still provide SSet.boundaryInclusion for the inclusion induced by the subcomplex, which is what we're trying to use here. What's the right way to refer to this map?

[Joël Riou]

You can use ∂Δ[n].ι or (boundary.{u} n).ι. ("boundary" is a subcomplex of the standard simplex, and ι is the inclusion of a subcomplex.) Note also that in #21118, I shall introduce generating cofibrations/trivial cofibrations for the WIP standard model category structure on SSet.

[Johan Commelin]

Any volunteers for reviewing this? It looks good to me. But model categories are approaching the boundary of my comfort zone. So I would appreciate a 2nd pair of eyes on this.

[Emily Riehl]

@Johan Commelin are you talking about #21118? If so, I can have a look sometime over the next few days.

[Johan Commelin]

Thanks, that would be great. It's a relatively short PR. I mostly would just want to get a :check: from someone who knows that maths that comes after this.

[Johan Commelin]

So a maths-review, as opposed to a Lean-style-review, if that makes sense :wink:

[Emily Riehl]

Phew! :sweat_smile: