The pointed mapping simplicial set

For pointed simplicial sets X and Y, the pointed mapping simplicial set Map_*(X, Y) is the subcomplex of the internal hom [X, Y] of the underlying simplicial sets consisting of the based maps. An n-simplex of [X, Y] is a family of maps X_m ⟶ Y_m indexed by the m-simplices of Δ[n] and natural in m (Mathlib's Functor.HomObj); it is based when every map of the family sends the basepoint of X to the basepoint of Y. The basepoint of Map_*(X, Y) is the constant map to the basepoint of Y.

Currying identifies based maps X ∧ Y ⟶ Z out of the smash product with based maps Y ⟶ Map_*(X, Z), naturally in Y and Z, so the smash product of pointed simplicial sets is a closed monoidal structure. Consequently X ∧ - is a left adjoint and preserves all colimits; as the smash product is symmetric, so is - ∧ X, by Mathlib.CategoryTheory.Monoidal.Closed.Braided. Applied to the simplicial circle S¹, this gives the adjunction S¹ ∧ - ⊣ Map_*(S¹, -) between simplicial suspension and loops.

Main definitions

• PointedSSet.basedMaps X Y: the subcomplex of based maps in the internal hom [X.right, Y.right] of simplicial sets.
• PointedSSet.ihom X: the functor Y ↦ Map_*(X, Y), acting by postcomposition.
• PointedSSet.tensorHomEquiv X Y Z: the currying bijection (X ⊗ Y ⟶ Z) ≃ (Y ⟶ Map_*(X, Z)).
• PointedSSet.pointRestriction E K: the constant family of maps to the basepoint of E.

Main statements

• The instance MonoidalClosed PointedSSet, with right adjoint PointedSSet.ihom X to tensorLeft X.
• PointedSSet.homEquiv_def: its hom-set bijection is PointedSSet.tensorHomEquiv.
• Simplex-level descriptions of currying, uncurrying, evaluation and coevaluation.
• PointedSSet.range_le_basedMaps_iff: a family is based exactly when its restriction to the source basepoint is constant at the target basepoint.
• PointedSSet.basedMaps_isPullback: based maps are the fibre of restriction to the basepoint.

References

• M. Hovey, B. Shipley and J. Smith, Symmetric spectra, J. Amer. Math. Soc. 13 (2000), Section 1.

def TauCeti.PointedSSet.basedMaps (X Y : PointedSSet) : ((CategoryTheory.ihom (CategoryTheory.Under.right X)).obj (CategoryTheory.Under.right Y)).Subcomplex

The based maps among the simplices of the internal hom [X, Y] of the underlying simplicial sets: the n-simplices whose every component sends the basepoint of X to the basepoint of Y.

@[simp]

theorem TauCeti.PointedSSet.mem_basedMaps_iff {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} (φ : ((CategoryTheory.ihom (CategoryTheory.Under.right X)).obj (CategoryTheory.Under.right Y)).obj n) : φ ∈ (X.basedMaps Y).obj n ↔ ∀ (m : SimplexCategoryᵒᵖ) (f : n ⟶ m), (CategoryTheory.ConcreteCategory.hom (φ.app m f)) (X.point m) = Y.point m

@[simp]

theorem TauCeti.PointedSSet.basedMaps_app_point {X Y : PointedSSet} {n m : SimplexCategoryᵒᵖ} (φ : ↑((X.basedMaps Y).obj n)) (f : n ⟶ m) : (CategoryTheory.ConcreteCategory.hom ((↑φ).app m f)) (X.point m) = Y.point m

A based simplex of the internal hom sends the basepoint to the basepoint.

def TauCeti.PointedSSet.basedMapsPoint (X Y : PointedSSet) : SSet.stdSimplex.obj { len := 0 } ⟶ (X.basedMaps Y).toSSet

The constant map at the basepoint, as the basepoint of the simplicial set of based maps.

def TauCeti.PointedSSet.ihom (X : PointedSSet) : CategoryTheory.Functor PointedSSet PointedSSet

The pointed mapping simplicial set Map_*(X, Y) of based maps, as a functor of Y; it acts on based maps by postcomposition.

theorem TauCeti.PointedSSet.ihom_obj_right_ext {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} {φ ψ : (CategoryTheory.Under.right (X.ihom.obj Y)).obj n} (h : ∀ (m : SimplexCategoryᵒᵖ) (f : n ⟶ m) (x : (fun (X : Type u) => X) ((CategoryTheory.Under.right X).obj m)), (CategoryTheory.ConcreteCategory.hom ((↑φ).app m f)) x = (CategoryTheory.ConcreteCategory.hom ((↑ψ).app m f)) x) : φ = ψ

Two simplices of Map_*(X, Y) are equal when their components agree on every simplex.

theorem TauCeti.PointedSSet.ihom_obj_right_ext_iff {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} {φ ψ : (CategoryTheory.Under.right (X.ihom.obj Y)).obj n} : φ = ψ ↔ ∀ (m : SimplexCategoryᵒᵖ) (f : n ⟶ m) (x : (fun (X : Type u) => X) ((CategoryTheory.Under.right X).obj m)), (CategoryTheory.ConcreteCategory.hom ((↑φ).app m f)) x = (CategoryTheory.ConcreteCategory.hom ((↑ψ).app m f)) x

def TauCeti.PointedSSet.tensorHomEquiv (X Y Z : PointedSSet) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) ≃ (Y ⟶ X.ihom.obj Z)

Currying identifies based maps X ⊗ Y ⟶ Z out of the smash product with based maps Y ⟶ Map_*(X, Z): a simplex y goes to the based map x ↦ f (x ∧ y).

@[simp]

theorem TauCeti.PointedSSet.tensorHomEquiv_apply_right_app_coe_app_apply {X Y Z : PointedSSet} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) {n m : SimplexCategoryᵒᵖ} (y : (CategoryTheory.Under.right Y).obj n) (g : n ⟶ m) (x : (CategoryTheory.Under.right X).obj m) : (CategoryTheory.ConcreteCategory.hom ((↑((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right ((X.tensorHomEquiv Y Z) f)).app n)) y)).app m g)) x = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right f).app m)) (smashMk x ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right Y).map g)) y))

@[simp]

theorem TauCeti.PointedSSet.tensorHomEquiv_symm_apply_right_app_smashMk {X Y Z : PointedSSet} (g : Y ⟶ X.ihom.obj Z) {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.Under.right X).obj n) (y : (CategoryTheory.Under.right Y).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right ((X.tensorHomEquiv Y Z).symm g)).app n)) (smashMk x y) = (CategoryTheory.ConcreteCategory.hom ((↑((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right g).app n)) y)).app n (CategoryTheory.CategoryStruct.id n))) x

theorem TauCeti.PointedSSet.tensorHomEquiv_symm_comp {X Y Z Y' : PointedSSet} (f : Y' ⟶ Y) (g : Y ⟶ X.ihom.obj Z) : (X.tensorHomEquiv Y' Z).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) ((X.tensorHomEquiv Y Z).symm g)

Currying is natural in the source: precomposition with f corresponds to precomposition with X ◁ f.

theorem TauCeti.PointedSSet.tensorHomEquiv_comp {X Y Z Z' : PointedSSet} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) (g : Z ⟶ Z') : (X.tensorHomEquiv Y Z') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((X.tensorHomEquiv Y Z) f) (X.ihom.map g)

Currying is natural in the target: postcomposition with g corresponds to postcomposition with Map_*(X, g).

@[instance_reducible]

instance TauCeti.PointedSSet.monoidalClosed : CategoryTheory.MonoidalClosed PointedSSet

The smash product of pointed simplicial sets is closed: X ⊗ - is left adjoint to the pointed mapping simplicial set functor Map_*(X, -).

theorem TauCeti.PointedSSet.homEquiv_def (X Y Z : PointedSSet) : (CategoryTheory.ihom.adjunction X).homEquiv Y Z = X.tensorHomEquiv Y Z

The hom-set bijection of the smash–hom adjunction is PointedSSet.tensorHomEquiv.

@[simp]

theorem TauCeti.PointedSSet.curry_right_app_coe_app_apply {X Y Z : PointedSSet} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) {n m : SimplexCategoryᵒᵖ} (y : (CategoryTheory.Under.right Y).obj n) (g : n ⟶ m) (x : (CategoryTheory.Under.right X).obj m) : (CategoryTheory.ConcreteCategory.hom ((↑((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.MonoidalClosed.curry f)).app n)) y)).app m g)) x = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right f).app m)) (smashMk x ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right Y).map g)) y))

@[simp]

theorem TauCeti.PointedSSet.uncurry_right_app_smashMk {X Y Z : PointedSSet} (g : Y ⟶ (CategoryTheory.ihom X).obj Z) {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.Under.right X).obj n) (y : (CategoryTheory.Under.right Y).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.MonoidalClosed.uncurry g)).app n)) (smashMk x y) = (CategoryTheory.ConcreteCategory.hom ((↑((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right g).app n)) y)).app n (CategoryTheory.CategoryStruct.id n))) x

@[simp]

theorem TauCeti.PointedSSet.ihom_obj_right_coe_app_point {X Y : PointedSSet} {n m : SimplexCategoryᵒᵖ} (φ : (CategoryTheory.Under.right ((CategoryTheory.ihom X).obj Y)).obj n) (f : n ⟶ m) : (CategoryTheory.ConcreteCategory.hom ((↑φ).app m f)) (X.point m) = Y.point m

A simplex of Map_*(X, Y) sends the basepoint of X to the basepoint of Y.

@[simp]

theorem TauCeti.PointedSSet.ihom_obj_right_map_coe_app_apply {X Y : PointedSSet} {n m k : SimplexCategoryᵒᵖ} (f : n ⟶ m) (φ : (CategoryTheory.Under.right ((CategoryTheory.ihom X).obj Y)).obj n) (g : m ⟶ k) (x : (CategoryTheory.Under.right X).obj k) : (CategoryTheory.ConcreteCategory.hom ((↑((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right ((CategoryTheory.ihom X).obj Y)).map f)) φ)).app k g)) x = (CategoryTheory.ConcreteCategory.hom ((↑φ).app k (CategoryTheory.CategoryStruct.comp f g))) x

The simplicial operator of Map_*(X, Y) along f precomposes the components of a based map with f.

@[simp]

theorem TauCeti.PointedSSet.ihom_obj_point_coe_app_apply {X Y : PointedSSet} {n m : SimplexCategoryᵒᵖ} (f : n ⟶ m) (x : (CategoryTheory.Under.right X).obj m) : (CategoryTheory.ConcreteCategory.hom ((↑(((CategoryTheory.ihom X).obj Y).point n)).app m f)) x = Y.point m

The basepoint of Map_*(X, Y) is the constant map to the basepoint of Y.

@[simp]

theorem TauCeti.PointedSSet.pre_right_app_coe_app_apply {X Y W : PointedSSet} (i : W ⟶ X) {n m : SimplexCategoryᵒᵖ} (φ : (CategoryTheory.Under.right ((CategoryTheory.ihom X).obj Y)).obj n) (f : n ⟶ m) (x : (CategoryTheory.Under.right W).obj m) : (CategoryTheory.ConcreteCategory.hom ((↑((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right ((CategoryTheory.MonoidalClosed.pre i).app Y)).app n)) φ)).app m f)) x = (CategoryTheory.ConcreteCategory.hom ((↑φ).app m f)) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right i).app m)) x)

Precomposition of a based mapping simplex acts on its source components.

@[simp]

theorem TauCeti.PointedSSet.ihom_map_right_app_coe_app_apply {X Y Z : PointedSSet} (g : Y ⟶ Z) {n m : SimplexCategoryᵒᵖ} (φ : (CategoryTheory.Under.right ((CategoryTheory.ihom X).obj Y)).obj n) (f : n ⟶ m) (x : (CategoryTheory.Under.right X).obj m) : (CategoryTheory.ConcreteCategory.hom ((↑((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right ((CategoryTheory.ihom X).map g)).app n)) φ)).app m f)) x = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right g).app m)) ((CategoryTheory.ConcreteCategory.hom ((↑φ).app m f)) x)

The internal hom acts on based maps by postcomposition.

@[simp]

theorem TauCeti.PointedSSet.ihom_ev_app_right_app_smashMk {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.Under.right X).obj n) (φ : (CategoryTheory.Under.right ((CategoryTheory.ihom X).obj Y)).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right ((CategoryTheory.ihom.ev X).app Y)).app n)) (smashMk x φ) = (CategoryTheory.ConcreteCategory.hom ((↑φ).app n (CategoryTheory.CategoryStruct.id n))) x

Evaluation X ⊗ Map_*(X, Y) ⟶ Y applies a based map to a simplex.

@[simp]

theorem TauCeti.PointedSSet.ihom_coev_app_right_app_coe_app_apply {X Y : PointedSSet} {n m : SimplexCategoryᵒᵖ} (y : (CategoryTheory.Under.right Y).obj n) (f : n ⟶ m) (x : (CategoryTheory.Under.right X).obj m) : (CategoryTheory.ConcreteCategory.hom ((↑((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right ((CategoryTheory.ihom.coev X).app Y)).app n)) y)).app m f)) x = smashMk x ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right Y).map f)) y)

Coevaluation Y ⟶ Map_*(X, X ⊗ Y) sends a simplex y to the based map x ↦ x ∧ y.

@[simp]

theorem TauCeti.PointedSSet.pre_point_app (X E : PointedSSet) {n m : SimplexCategoryᵒᵖ} (φ : ((CategoryTheory.ihom (CategoryTheory.Under.right X)).obj (CategoryTheory.Under.right E)).obj n) (f : n ⟶ m) (z : (SSet.stdSimplex.obj { len := 0 }).obj m) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.MonoidalClosed.pre (CategoryTheory.Under.hom X)).app (CategoryTheory.Under.right E)).app n)) φ).app m f)) z = (CategoryTheory.ConcreteCategory.hom (φ.app m f)) (X.point m)

Restriction of an unpointed mapping simplex to the chosen point of its source.

def TauCeti.PointedSSet.pointRestriction (E : PointedSSet) (K : SSet) : K ⟶ (CategoryTheory.ihom (SSet.stdSimplex.obj { len := 0 })).obj (CategoryTheory.Under.right E)

The constant family of maps from the zero-simplex to the chosen point of E.

@[simp]

theorem TauCeti.PointedSSet.pointRestriction_app_app (E : PointedSSet) (K : SSet) {n m : SimplexCategoryᵒᵖ} (x : K.obj n) (f : n ⟶ m) (z : (SSet.stdSimplex.obj { len := 0 }).obj m) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ConcreteCategory.hom ((E.pointRestriction K).app n)) x).app m f)) z = E.point m

Every component of the constant family is the chosen point.

@[simp]

theorem TauCeti.PointedSSet.comp_pointRestriction (E : PointedSSet) {K L : SSet} (f : K ⟶ L) : CategoryTheory.CategoryStruct.comp f (E.pointRestriction L) = E.pointRestriction K

Constant families at the basepoint are natural in their parameter.

@[simp]

theorem TauCeti.PointedSSet.comp_pointRestriction_assoc (E : PointedSSet) {K L : SSet} (f : K ⟶ L) {Z : SSet} (h : (CategoryTheory.ihom (SSet.stdSimplex.obj { len := 0 })).obj (CategoryTheory.Under.right E) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (E.pointRestriction L) h) = CategoryTheory.CategoryStruct.comp (E.pointRestriction K) h

Constant families at the basepoint are natural in their parameter.

@[simp]

theorem TauCeti.PointedSSet.pointRestriction_comp_ihom_map {E B : PointedSSet} (p : E ⟶ B) (K : SSet) : CategoryTheory.CategoryStruct.comp (E.pointRestriction K) ((CategoryTheory.ihom (SSet.stdSimplex.obj { len := 0 })).map (CategoryTheory.Under.Hom.right p)) = B.pointRestriction K

Based maps preserve the constant family at the basepoint.

@[simp]

theorem TauCeti.PointedSSet.pointRestriction_comp_ihom_map_assoc {E B : PointedSSet} (p : E ⟶ B) (K : SSet) {Z : SSet} (h : (CategoryTheory.ihom (SSet.stdSimplex.obj { len := 0 })).obj (CategoryTheory.Under.right B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.pointRestriction K) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom (SSet.stdSimplex.obj { len := 0 })).map (CategoryTheory.Under.Hom.right p)) h) = CategoryTheory.CategoryStruct.comp (B.pointRestriction K) h

Based maps preserve the constant family at the basepoint.

theorem TauCeti.PointedSSet.range_le_basedMaps_iff (X E : PointedSSet) {K : SSet} (f : K ⟶ (CategoryTheory.ihom (CategoryTheory.Under.right X)).obj (CategoryTheory.Under.right E)) : SSet.Subcomplex.range f ≤ X.basedMaps E ↔ CategoryTheory.CategoryStruct.comp f ((CategoryTheory.MonoidalClosed.pre (CategoryTheory.Under.hom X)).app (CategoryTheory.Under.right E)) = E.pointRestriction K

A family of unpointed maps is based exactly when restriction to the source basepoint is the constant family at the target basepoint.

@[simp]

theorem TauCeti.PointedSSet.basedMaps_ι_comp_pre (X E : PointedSSet) : CategoryTheory.CategoryStruct.comp (X.basedMaps E).ι ((CategoryTheory.MonoidalClosed.pre (CategoryTheory.Under.hom X)).app (CategoryTheory.Under.right E)) = E.pointRestriction (X.basedMaps E).toSSet

The inclusion of based maps restricts to the constant family at the basepoint.

@[simp]

theorem TauCeti.PointedSSet.basedMaps_ι_comp_pre_assoc (X E : PointedSSet) {Z : SSet} (h : (CategoryTheory.ihom (SSet.stdSimplex.obj { len := 0 })).obj (CategoryTheory.Under.right E) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.basedMaps E).ι (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre (CategoryTheory.Under.hom X)).app (CategoryTheory.Under.right E)) h) = CategoryTheory.CategoryStruct.comp (E.pointRestriction (X.basedMaps E).toSSet) h

The inclusion of based maps restricts to the constant family at the basepoint.

theorem TauCeti.PointedSSet.basedMaps_isPullback (X E : PointedSSet) : CategoryTheory.IsPullback (X.basedMaps E).ι (SSet.stdSimplex.isTerminalObj₀.from (X.basedMaps E).toSSet) ((CategoryTheory.MonoidalClosed.pre (CategoryTheory.Under.hom X)).app (CategoryTheory.Under.right E)) (E.pointRestriction (SSet.stdSimplex.obj { len := 0 }))

The based mapping simplicial set is the fibre of restriction to the source basepoint at the target basepoint, expressed as a pullback over the zero-simplex.

@[simp]

theorem TauCeti.PointedSSet.ihom_map_right_comp_ι {E B : PointedSSet} (X : PointedSSet) (p : E ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right (X.ihom.map p)) (X.basedMaps B).ι = CategoryTheory.CategoryStruct.comp (X.basedMaps E).ι ((CategoryTheory.ihom (CategoryTheory.Under.right X)).map (CategoryTheory.Under.Hom.right p))

Inclusion of based maps into unpointed maps commutes with postcomposition.

theorem TauCeti.PointedSSet.ihom_map_right_comp_ι_assoc {E B : PointedSSet} (X : PointedSSet) (p : E ⟶ B) {Z : SSet} (h : (CategoryTheory.ihom (CategoryTheory.Under.right X)).obj (CategoryTheory.Under.right B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right (X.ihom.map p)) (X.basedMaps B).ι) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (X.basedMaps E).ι ((CategoryTheory.ihom (CategoryTheory.Under.right X)).map (CategoryTheory.Under.Hom.right p))) h

Inclusion of based maps into unpointed maps commutes with postcomposition.

@[simp]

theorem TauCeti.PointedSSet.pre_right_comp_ι {W X : PointedSSet} (i : W ⟶ X) (E : PointedSSet) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right ((CategoryTheory.MonoidalClosed.pre i).app E)) (W.basedMaps E).ι = CategoryTheory.CategoryStruct.comp (X.basedMaps E).ι ((CategoryTheory.MonoidalClosed.pre (CategoryTheory.Under.Hom.right i)).app (CategoryTheory.Under.right E))

Inclusion of based maps into unpointed maps commutes with precomposition.

theorem TauCeti.PointedSSet.pre_right_comp_ι_assoc {W X : PointedSSet} (i : W ⟶ X) (E : PointedSSet) {Z : SSet} (h : (CategoryTheory.ihom (CategoryTheory.Under.right W)).obj (CategoryTheory.Under.right E) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right ((CategoryTheory.MonoidalClosed.pre i).app E)) (W.basedMaps E).ι) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (X.basedMaps E).ι ((CategoryTheory.MonoidalClosed.pre (CategoryTheory.Under.Hom.right i)).app (CategoryTheory.Under.right E))) h

Inclusion of based maps into unpointed maps commutes with precomposition.