PInfty_on_Γ₀_splitting_summand_eq_self

English

The PInfty projector, restricted to the Γ₀-splitting summand, acts as a projection that is compatible with the Γ₀ splitting and its canonical inclusions.

Русский

Проектор PInfty, ограниченный на разложение Γ₀, действует как проекция, совместимая с разложением Γ₀ и его каноническими включениями.

LaTeX

$$$PInfty\circ (\text{Γ₀.splitting}_{K})_{\text{inj}} = (\text{Γ₀.splitting}_{K})_{\text{inj}}$$$

Lean4

@[reassoc (attr := simp)]
theorem PInfty_on_Γ₀_splitting_summand_eq_self (K : ChainComplex C ℕ) {n : ℕ} :
    ((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ (PInfty : K[Γ₀.obj K] ⟶ _).f n =
      ((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) :=
  by
  rw [PInfty_f]
  rcases n with _ | n
  · simpa only [P_f_0_eq] using comp_id _
  · exact (HigherFacesVanish.on_Γ₀_summand_id K n).comp_P_eq_self

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