Theorems · Theorem · algebraic topology

TopCat.toSSetObjEquiv_symm_naturality

∀ {X : TopCat} {n m : SimplexCategory} (f : n ⟶ m) (g : C(↑(stdSimplex ℝ (Fin (m.len + 1))), ↑X)),
  (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map f.op)) ((X.toSSetObjEquiv (Opposite.op m)).symm g) =
    (X.toSSetObjEquiv (Opposite.op n)).symm
      (g.comp { toFun := stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f), continuous_toFun := ⋯ })

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Cited by

0 results in Mathlib

Foundations

Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound