natTransQ — Mathlib

English

The P_q construction is natural in the simplicial object: for any morphism f of simplicial objects, the square with f and (P_q).f n commutes.

Русский

Конструкция P_q естественна по отношению к симпликсу: для любого морфизма f между симплициальными объектами диаграмма с f и (P_q).f n коммутирует.

LaTeX

$$$(f: X \to Y)$, $((P_q).f n)$ satisfies $f_{obj} \circ (P_q).f n = (P_q).f n \circ f_{obj}$ at level n.$$

Lean4

/-- For each `q`, `Q q` is a natural transformation. -/
@[simps]
def natTransQ (q : ℕ) : alternatingFaceMapComplex C ⟶ alternatingFaceMapComplex C where app _ := Q q

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