Q_f_naturality — Mathlib

English

Similarly to P_q, the Q_q constructions give idempotent endomorphisms on the alternating face map complex; i.e., (Q_q).f(n) ≫ (Q_q).f(n) = (Q_q).f(n).

Русский

Аналогично P_q конструкциям, Q_q задают идемпотентные эндоморфизмы на чередующемся комплексе граней: (Q_q).f(n) ∘ (Q_q).f(n) = (Q_q).f(n).

LaTeX

$$$\forall q,n:\; (Q_q).f(n) \circ (Q_q).f(n) = (Q_q).f(n).$$$

Lean4

@[reassoc (attr := simp)]
theorem Q_f_naturality (q n : ℕ) {X Y : SimplicialObject C} (f : X ⟶ Y) :
    f.app (op ⦋n⦌) ≫ (Q q).f n = (Q q).f n ≫ f.app (op ⦋n⦌) :=
  by
  simp only [Q, HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, P_f_naturality, sub_comp,
    sub_left_inj]
  dsimp
  simp only [comp_id, id_comp]

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