comp_P_eq_self_iff — Mathlib

English

Let X be a simplicial object in a preadditive category. For any q and n, and any φ with HigherFacesVanish q φ, we have φ ≫ (P_q).f(n+1) = φ; the projector acts as the identity on such φ.

Русский

Пусть X — симплициальный объект в предадитивной категории. Для любых q и n и любого φ с свойством HigherFacesVanish q φ имеем φ ≫ (P_q).f(n+1) = φ; проекция действует как тождественный отображение на такие φ.

LaTeX

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

Lean4

theorem comp_P_eq_self_iff {Y : C} {n q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} : φ ≫ (P q).f (n + 1) = φ ↔ HigherFacesVanish q φ :=
  by
  constructor
  · intro hφ
    rw [← hφ]
    apply HigherFacesVanish.of_comp
    apply HigherFacesVanish.of_P
  · exact HigherFacesVanish.comp_P_eq_self

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