Theorems · Theorem · algebraic topology

TopCat.toSSetObjEquiv_naturality_apply

∀ {X : TopCat} {n m : SimplexCategory} (f : n ⟶ m) (x : (TopCat.toSSet.obj X).obj (Opposite.op m))
  (z : ↑(stdSimplex ℝ (Fin (n.len + 1)))),
  ((X.toSSetObjEquiv (Opposite.op n)) ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map f.op)) x)) z =
    ((X.toSSetObjEquiv (Opposite.op m)) x) (stdSimplex.map (⇑(CategoryTheory.ConcreteCategory.hom f)) z)

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Cited by

0 results in Mathlib

Foundations

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