Pointed simplicial sets

A pointed simplicial set is an object of the native undercategory of the standard zero-simplex. Evaluating its pointing gives a point in every degree, preserved by all simplicial operators. Conversely, the points of a simplicial object in Pointed define a map from the zero-simplex. These constructions give an explicit equivalence, allowing based simplicial constructions to use either presentation.

@[reducible, inline]

abbrev TauCeti.PointedSSet : Type (u + 1)

Simplicial sets with a chosen point, using the native undercategory.

def TauCeti.PointedSSet.point (X : PointedSSet) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.Under.right X).obj n

The chosen simplex in each degree of a pointed simplicial set.

@[simp]

theorem TauCeti.PointedSSet.point_mk {X : SSet} (p : SSet.stdSimplex.obj { len := 0 } ⟶ X) (n : SimplexCategoryᵒᵖ) : point (CategoryTheory.Under.mk p) n = (CategoryTheory.ConcreteCategory.hom (p.app n)) (SSet.stdSimplex.const 0 0 n)

@[simp]

theorem TauCeti.PointedSSet.hom_app (X : PointedSSet) (n : SimplexCategoryᵒᵖ) (x : (SSet.stdSimplex.obj { len := 0 }).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.hom X).app n)) x = X.point n

@[simp]

theorem TauCeti.PointedSSet.map_point (X : PointedSSet) {n m : SimplexCategoryᵒᵖ} (f : n ⟶ m) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right X).map f)) (X.point n) = X.point m

@[simp]

theorem TauCeti.PointedSSet.app_point {X Y : PointedSSet} (f : X ⟶ Y) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right f).app n)) (X.point n) = Y.point n

theorem TauCeti.PointedSSet.comp_right_app_apply {X Y Z : PointedSSet} (f : X ⟶ Y) (g : Y ⟶ Z) (n : SimplexCategoryᵒᵖ) (x : (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.CategoryStruct.comp f g)).app n)) x = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right g).app n)) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right f).app n)) x)

A composite of based maps acts on simplices as the composite of the two functions. This is not a simp lemma, since simp unfolds the composite through Under.comp_right and NatTrans.comp_app; it gives that unfolding in one rewrite.

def TauCeti.PointedSSet.toSimplicialPointed : CategoryTheory.Functor PointedSSet (CategoryTheory.SimplicialObject Pointed)

Evaluate a pointed simplicial set as a simplicial object in pointed types.

def TauCeti.PointedSSet.fromSimplicialPointed : CategoryTheory.Functor (CategoryTheory.SimplicialObject Pointed) PointedSSet

Recover a pointed simplicial set from its compatible degreewise points.

@[simp]

theorem TauCeti.PointedSSet.toSimplicialPointed_obj_obj (X : PointedSSet) (n : SimplexCategoryᵒᵖ) : (toSimplicialPointed.obj X).obj n = Pointed.of (X.point n)

@[simp]

theorem TauCeti.PointedSSet.fromSimplicialPointed_obj_right (X : CategoryTheory.SimplicialObject Pointed) : CategoryTheory.Under.right (fromSimplicialPointed.obj X) = CategoryTheory.Functor.comp X (CategoryTheory.forget Pointed)

def TauCeti.PointedSSet.forgetIso : toSimplicialPointed.comp ((CategoryTheory.SimplicialObject.whiskering Pointed (Type u)).obj (CategoryTheory.forget Pointed)) ≅ CategoryTheory.Under.forget (SSet.stdSimplex.obj { len := 0 })

Forgetting degreewise points agrees naturally with forgetting the chosen pointing.

theorem TauCeti.PointedSSet.forgetIso_hom_app_app (X : PointedSSet) (n : SimplexCategoryᵒᵖ) : (forgetIso.hom.app X).app n = CategoryTheory.eqToHom ⋯

theorem TauCeti.PointedSSet.forgetIso_inv_app_app (X : PointedSSet) (n : SimplexCategoryᵒᵖ) : (forgetIso.inv.app X).app n = CategoryTheory.eqToHom ⋯

@[simp]

theorem TauCeti.PointedSSet.forgetIso_hom_app_point (X : PointedSSet) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.ConcreteCategory.hom ((forgetIso.hom.app X).app n)) ((toSimplicialPointed.obj X).obj n).point = X.point n

theorem TauCeti.PointedSSet.toSimplicialPointed_obj_map (X : PointedSSet) {n m : SimplexCategoryᵒᵖ} (f : n ⟶ m) (x : ((toSimplicialPointed.obj X).obj n).X) : (CategoryTheory.ConcreteCategory.hom ((forgetIso.hom.app X).app m)) (((toSimplicialPointed.obj X).map f).toFun x) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right X).map f)) ((CategoryTheory.ConcreteCategory.hom ((forgetIso.hom.app X).app n)) x)

The forward construction applies each simplicial operator to the underlying simplex.

theorem TauCeti.PointedSSet.toSimplicialPointed_map_app {X Y : PointedSSet} (f : X ⟶ Y) (n : SimplexCategoryᵒᵖ) (x : ((toSimplicialPointed.obj X).obj n).X) : (CategoryTheory.ConcreteCategory.hom ((forgetIso.hom.app Y).app n)) (((toSimplicialPointed.map f).app n).toFun x) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right f).app n)) ((CategoryTheory.ConcreteCategory.hom ((forgetIso.hom.app X).app n)) x)

The forward construction applies each based map to the underlying simplex.

def TauCeti.PointedSSet.fromForgetIso : fromSimplicialPointed.comp (CategoryTheory.Under.forget (SSet.stdSimplex.obj { len := 0 })) ≅ (CategoryTheory.SimplicialObject.whiskering Pointed (Type u)).obj (CategoryTheory.forget Pointed)

The underlying simplicial set of the inverse construction is the forgetful image.

theorem TauCeti.PointedSSet.fromForgetIso_hom_app_app (X : CategoryTheory.SimplicialObject Pointed) (n : SimplexCategoryᵒᵖ) : (fromForgetIso.hom.app X).app n = CategoryTheory.eqToHom ⋯

theorem TauCeti.PointedSSet.fromForgetIso_inv_app_app (X : CategoryTheory.SimplicialObject Pointed) (n : SimplexCategoryᵒᵖ) : (fromForgetIso.inv.app X).app n = CategoryTheory.eqToHom ⋯

@[simp]

theorem TauCeti.PointedSSet.fromForgetIso_hom_app_point (X : CategoryTheory.SimplicialObject Pointed) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.ConcreteCategory.hom ((fromForgetIso.hom.app X).app n)) ((fromSimplicialPointed.obj X).point n) = (X.obj n).point

theorem TauCeti.PointedSSet.fromSimplicialPointed_map_app {X Y : CategoryTheory.SimplicialObject Pointed} (f : X ⟶ Y) (n : SimplexCategoryᵒᵖ) (x : (CategoryTheory.Under.right (fromSimplicialPointed.obj X)).obj n) : (CategoryTheory.ConcreteCategory.hom ((fromForgetIso.hom.app Y).app n)) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (fromSimplicialPointed.map f)).app n)) x) = (f.app n).toFun ((CategoryTheory.ConcreteCategory.hom ((fromForgetIso.hom.app X).app n)) x)

The inverse construction acts by the original degreewise pointed map.

def TauCeti.PointedSSet.unitIso : CategoryTheory.Functor.id PointedSSet ≅ toSimplicialPointed.comp fromSimplicialPointed

The conversion back to a pointed simplicial set preserves every simplex.

def TauCeti.PointedSSet.counitIso : fromSimplicialPointed.comp toSimplicialPointed ≅ CategoryTheory.Functor.id (CategoryTheory.SimplicialObject Pointed)

The degreewise pointed presentation is recovered by the identity maps.

theorem TauCeti.PointedSSet.unitIso_hom_app_right_app (X : PointedSSet) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.Under.Hom.right (unitIso.hom.app X)).app n = CategoryTheory.eqToHom ⋯

theorem TauCeti.PointedSSet.unitIso_inv_app_right_app (X : PointedSSet) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.Under.Hom.right (unitIso.inv.app X)).app n = CategoryTheory.eqToHom ⋯

theorem TauCeti.PointedSSet.counitIso_hom_app_app (X : CategoryTheory.SimplicialObject Pointed) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.forget Pointed).map ((counitIso.hom.app X).app n) = CategoryTheory.eqToHom ⋯

theorem TauCeti.PointedSSet.counitIso_inv_app_app (X : CategoryTheory.SimplicialObject Pointed) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.forget Pointed).map ((counitIso.inv.app X).app n) = CategoryTheory.eqToHom ⋯

def TauCeti.PointedSSet.simplicialPointedEquivalence : PointedSSet ≌ CategoryTheory.SimplicialObject Pointed

The equivalence between native pointed simplicial sets and simplicial pointed types.

@[simp]

theorem TauCeti.PointedSSet.simplicialPointedEquivalence_functor : simplicialPointedEquivalence.functor = toSimplicialPointed

@[simp]

theorem TauCeti.PointedSSet.simplicialPointedEquivalence_inverse : simplicialPointedEquivalence.inverse = fromSimplicialPointed