English
For any Z and morphism f: Z → X_n, f ≫ PInfty.f n = 0 iff f ≫ s.πSummand(Id) = 0; i.e., PInfty detects the complementary part of the splitting.
Русский
Для любого Z и морфизма f: Z → X_n, f ≫ PInfty.f n = 0 тогда и только тогда, когда f ≫ s.πSummand(Id) = 0; то есть PInfty обнаруживает комплементарную часть разложения.
LaTeX
$$$\forall Z, f:\; Z \to X_{\langle n \rangle},\; f \circ PInfty.f n = 0 \iff f \circ πSummand(Id) = 0$$$
Lean4
theorem comp_PInfty_eq_zero_iff {Z : C} {n : ℕ} (f : Z ⟶ X _⦋n⦌) :
f ≫ PInfty.f n = 0 ↔ f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0 :=
by
constructor
· intro h
rcases n with _ | n
· dsimp at h
rw [comp_id] at h
rw [h, zero_comp]
· have h' := f ≫= PInfty_f_add_QInfty_f (n + 1)
dsimp at h'
rw [comp_id, comp_add, h, zero_add] at h'
rw [← h', assoc, QInfty_f, decomposition_Q, Preadditive.sum_comp, Preadditive.comp_sum, Finset.sum_eq_zero]
intro i _
simp only [assoc, σ_comp_πSummand_id_eq_zero, comp_zero]
· intro h
rw [← comp_id f, assoc, s.decomposition_id, Preadditive.sum_comp, Preadditive.comp_sum, Fintype.sum_eq_zero]
intro A
by_cases hA : A.EqId
· dsimp at hA
subst hA
rw [assoc, reassoc_of% h, zero_comp]
· simp only [assoc, s.cofan_inj_comp_PInfty_eq_zero A hA, comp_zero]
