P_f_idem — Mathlib

English

If φ satisfies HigherFacesVanish q φ, then composing with (P_q).f(n+1) leaves φ unchanged: φ ≫ (P_q).f(n+1) = φ.

Русский

Если φ удовлетворяет условию HigherFacesVanish q φ, то композиция с (P_q).f(n+1) не изменяет φ: φ ≫ (P_q).f(n+1) = φ.

LaTeX

$$$\forall q,n,\; \forall \phi:\n Y \to X_{\langle n+1 \rangle},\; HigherFacesVanish_q(\phi) \Rightarrow\; \phi \circ (P_q).f(n+1) = \phi.$$$

Lean4

@[reassoc (attr := simp)]
theorem P_f_idem (q n : ℕ) : ((P q).f n : X _⦋n⦌ ⟶ _) ≫ (P q).f n = (P q).f n :=
  by
  rcases n with (_ | n)
  · rw [P_f_0_eq q, comp_id]
  · exact (HigherFacesVanish.of_P q n).comp_P_eq_self

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