πSummand — Mathlib

English

Each P_q acts idempotently on X; i.e., (P_q).f(n) ≫ (P_q).f(n) = (P_q).f(n).

Русский

Каждый P_q действует идемпотентно на X: (P_q).f(n) ∘ (P_q).f(n) = (P_q).f(n).

LaTeX

$$$\forall q,n:\; (P_q).f(n) \circ (P_q).f(n) = (P_q).f(n).$$$

Lean4

/-- The projection on a summand of the coproduct decomposition given
by a splitting of a simplicial object. -/
noncomputable def πSummand [HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ} (A : IndexSet Δ) : X.obj Δ ⟶ s.N A.1.unop.len :=
  s.desc Δ
    (fun B => by
      by_cases h : B = A
      · exact eqToHom (by subst h; rfl)
      · exact 0)

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