QInfty_f_naturality — Mathlib

English

Let X and Y be simplicial objects in a category C and f: X → Y a morphism. Then, for every n, the degree-n component of QInfty is natural with respect to f; i.e., the degree-n map f induces a commutative square with QInfty at level n.

Русский

Пусть X и Y — симплициальные объекты в категории C, и f: X → Y — морфизм. Тогда для каждого n компонент QInfty на уровне n естествен по отношению к f; т. е. в степени n получаем диаграмму с коммутированием.

LaTeX

$$$ f_n \circ QInfty_n = QInfty_n \circ f_n $$$

Lean4

@[reassoc (attr := simp)]
theorem QInfty_f_naturality (n : ℕ) {X Y : SimplicialObject C} (f : X ⟶ Y) :
    f.app (op ⦋n⦌) ≫ QInfty.f n = QInfty.f n ≫ f.app (op ⦋n⦌) :=
  Q_f_naturality n n f

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