P_f_naturality — Mathlib

English

Under a functor G between preadditive categories, the map of P_q at X corresponds to the P_q at the mapped object; i.e., G.map((P_q).f n) equals the f n component of the mapped P_q.

Русский

При применении дисциплинированной функции G между предадитивными категориями отображение P_q для X соответствует отображению P_q для преобразованного объекта; то есть G.map((P_q).f n) = (P_q).f n на соответствующем объекте.

LaTeX

$$$\forall q,n:\; G.map\bigl((P_q : K[X] \to _).f n\bigr) = (P_q : K[((whiskering C D).obj G).obj X] \to _).f n.$$$

Lean4

@[reassoc (attr := simp)]
theorem P_f_naturality (q n : ℕ) {X Y : SimplicialObject C} (f : X ⟶ Y) :
    f.app (op ⦋n⦌) ≫ (P q).f n = (P q).f n ≫ f.app (op ⦋n⦌) :=
  HomologicalComplex.congr_hom ((natTransP q).naturality f) n

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