P — Mathlib · SciLib

English

A proof-level lemma expressing how PInfty behaves in the Karoubi setting, via a natural composition with Y.p.

Русский

Лемма на уровне доказательства о поведении PInfty в Кароуоби-составе через композицию с Y.p.

LaTeX

$$$ (PInfty.f n).f = Y.p.app (op \langle n \rangle) \circ (PInfty : K[Y.X] ⟶ _).f n $$$

Lean4

/-- This is the inductive definition of the projections `P q : K[X] ⟶ K[X]`,
with `P 0 := 𝟙 _` and `P (q+1) := P q ≫ (𝟙 _ + Hσ q)`. -/
noncomputable def P : ℕ → (K[X] ⟶ K[X])
  | 0 => 𝟙 _
  | q + 1 => P q ≫ (𝟙 _ + Hσ q)

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