map_apply — Mathlib

English

For a morphism f: m1 ⟶ m2 of opposite simplex category and x in stdSimplex.obj n at m1, the map sends x to an element equal to the composed bijection with objEquiv.

Русский

Для морфизма f: m1 ⟶ m2 в противоположной категории SIMPLEX и x в stdSimplex.obj n при m1 отображение f отправляет x в элемент, равный композиции с objEquiv.

LaTeX

$$$(stdSimplex.obj n).map f\ x = objEquiv^{-1}(f.unop \; \circ \; objEquiv\ x)$$$

Lean4

theorem map_apply {m₁ m₂ : SimplexCategoryᵒᵖ} (f : m₁ ⟶ m₂) {n : SimplexCategory} (x : (stdSimplex.{u}.obj n).obj m₁) :
    (stdSimplex.{u}.obj n).map f x = objEquiv.symm (f.unop ≫ objEquiv x) := by rfl

Похожие утверждения