Q_idem — Mathlib

English

The family of projections P_q acts as idempotents on the whole alternating face map complex; in particular, their compositions agree with the projections themselves.

Русский

Семейство проекций P_q действует как идемпотенты на всем чередующемся комплексе граней; в частности, их композиции совпадают с самими проекциями.

LaTeX

$$$\{P_q\}_{q\in\mathbb{N}}\; \text{gives idempotents on the alternating face map complex; }\; P_q \circ P_q = P_q.$$$

Lean4

@[reassoc (attr := simp)]
theorem Q_idem (q : ℕ) : (Q q : K[X] ⟶ K[X]) ≫ Q q = Q q :=
  by
  ext n
  exact Q_f_idem q n

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