cofan_inj_πSummand_eq_id — Mathlib

English

The family of P_q maps are idempotent endomorphisms on the Dold-Kan projection object K[X].

Русский

Семейство отображений P_q задает идемпотентные концевые отображения на объекте Dold-Kan, соответствующем K[X].

LaTeX

$$$\forall q:\; P_q \text{ is idempotent on } K[X].$$$

Lean4

@[reassoc (attr := simp)]
theorem cofan_inj_πSummand_eq_id [HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ} (A : IndexSet Δ) :
    (s.cofan Δ).inj A ≫ s.πSummand A = 𝟙 _ := by simp [πSummand]

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