alternatingFaceMapComplex_map_f — Mathlib

English

The map between alternating face map complexes respects composition of morphisms.

Русский

Отображение между чередующимися комплексами сохраняет композицию морфизмов.

LaTeX

$$map (f : X ⟶ Y) respects composition: (map f) ∘ (map g) = map (f ∘ g)$$

Lean4

@[simp]
theorem alternatingFaceMapComplex_map_f {X Y : SimplicialObject C} (f : X ⟶ Y) (n : ℕ) :
    ((alternatingFaceMapComplex C).map f).f n = f.app (op ⦋n⦌) :=
  rfl

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