English
On the Karoubi-augmented simplicial object, the degree-n component of PInfty is determined by the structure map Y.p and the PInfty on Y.X.
Русский
На сопряженном Каруоби-объекте компонента PInfty в степени n задается через Y.p и PInfty на Y.X.
LaTeX
$$$ ((PInfty : K[(karoubiEmbedding().obj Y] ⟶ _).f n).f = Y.p. app (op \langle n \rangle) \circ (PInfty : K[Y.X] ⟶ _).f n$$$
Lean4
/-- Given an object `Y : Karoubi (SimplicialObject C)`, this lemma
computes `PInfty` for the associated object in `SimplicialObject (Karoubi C)`
in terms of `PInfty` for `Y.X : SimplicialObject C` and `Y.p`. -/
theorem karoubi_PInfty_f {Y : Karoubi (SimplicialObject C)} (n : ℕ) :
((PInfty : K[(karoubiFunctorCategoryEmbedding _ _).obj Y] ⟶ _).f n).f =
Y.p.app (op ⦋n⦌) ≫ (PInfty : K[Y.X] ⟶ _).f n :=
by
-- We introduce P_infty endomorphisms P₁, P₂, P₃, P₄ on various objects Y₁, Y₂, Y₃, Y₄.
let Y₁ := (karoubiFunctorCategoryEmbedding _ _).obj Y
let Y₂ := Y.X
let Y₃ := ((whiskering _ _).obj (toKaroubi C)).obj Y.X
let Y₄ := (karoubiFunctorCategoryEmbedding _ _).obj ((toKaroubi _).obj Y.X)
let P₁ : K[Y₁] ⟶ _ := PInfty
let P₂ : K[Y₂] ⟶ _ := PInfty
let P₃ : K[Y₃] ⟶ _ := PInfty
let P₄ : K[Y₄] ⟶ _ := PInfty
change (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n
have h₃₂ : (P₃.f n).f = P₂.f n := Karoubi.hom_ext_iff.mp (map_PInfty_f (toKaroubi C) Y₂ n)
have h₄₃ : P₄.f n = P₃.f n :=
by
have h := Functor.congr_obj (toKaroubi_comp_karoubiFunctorCategoryEmbedding _ _) Y₂
simp only [P₃, P₄, ← natTransPInfty_f_app]
congr 1
have h₁₄ :=
Idempotents.natTrans_eq
((𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)) ◫ (natTransPInfty_f (Karoubi C) n)) Y
dsimp [natTransPInfty_f] at h₁₄
rw [id_comp, id_comp, comp_id, comp_id] at h₁₄
rw [← h₃₂, ← h₄₃, h₁₄]
simp only [KaroubiFunctorCategoryEmbedding.map_app_f, Karoubi.decompId_p_f, Karoubi.decompId_i_f, Karoubi.comp_f]
let π : Y₄ ⟶ Y₄ := (toKaroubi _ ⋙ karoubiFunctorCategoryEmbedding _ _).map Y.p
have eq := Karoubi.hom_ext_iff.mp (PInfty_f_naturality n π)
simp only [Karoubi.comp_f] at eq
dsimp [π] at eq
rw [← eq, app_idem_assoc Y (op ⦋n⦌)]
