map_Q — Mathlib

English

The Q_q endomorphisms satisfy the same idempotence relation as P_q, i.e., Q_q composed with itself yields Q_q.

Русский

Конструкции Q_q удовлетворяют ту же идемпотентность, что и P_q: композиция Q_q с самим собой равна Q_q.

LaTeX

$$$\forall q:\; Q_q \circ Q_q = Q_q$$$

Lean4

theorem map_Q {D : Type*} [Category D] [Preadditive D] (G : C ⥤ D) [G.Additive] (X : SimplicialObject C) (q n : ℕ) :
    G.map ((Q q : K[X] ⟶ _).f n) = (Q q : K[((whiskering C D).obj G).obj X] ⟶ _).f n :=
  by
  rw [← add_right_inj (G.map ((P q : K[X] ⟶ _).f n)), ← G.map_add, map_P G X q n, P_add_Q_f, P_add_Q_f]
  apply G.map_id

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