English
For X, Y simplicial sets and a morphism f: X ⟶ Y, the op-map of f at level n is computed by transporting via the canonical identification X.op.obj n ≃ X.obj n, applying f, and transporting back.
Русский
Для X, Y симпликальные множества и морфизма f: X ⟶ Y отображение через противоположность на уровне n вычисляется посредством переноса через каноническое соответствие X.op.obj n ≃ X.obj n, применения f и обратного переноса.
LaTeX
$$$(X.op.map f)\\,x = opObjEquiv.symm\\bigl( X.map(\\mathrm{SimplexCategory.rev.map} f.unop).op (opObjEquiv x) \\bigr)$$$
Lean4
theorem op_map (X : SSet.{u}) {n m : SimplexCategoryᵒᵖ} (f : n ⟶ m) (x : X.op.obj n) :
X.op.map f x = opObjEquiv.symm (X.map (SimplexCategory.rev.map f.unop).op (opObjEquiv x)) :=
rfl
