English
In the right-hand side description, the descent through the cocone yields a zero condition equivalent to a zero condition for the extended map.
Русский
Описание через десценцию в кококоне эквивалентно нулю для расширенной карты.
LaTeX
$$d_comp_desc_eq_zero_iff$$
Lean4
theorem d_comp_desc_eq_zero_iff' ⦃W : C⦄ (f' : cocone.pt ⟶ K.X k) (hf' : cocone.π ≫ f' = K.d j k)
(f'' : cocone.pt ⟶ (K.extend e).X k') (hf'' : (extendXIso K e hj').hom ≫ cocone.π ≫ f'' = (K.extend e).d j' k')
(φ : W ⟶ cocone.pt) : φ ≫ f' = 0 ↔ φ ≫ f'' = 0 :=
by
by_cases hjk : c.Rel j k
· have hk'' : e.f k = k' := by rw [← hk', ← hj', c'.next_eq' (e.rel hjk)]
have : f' ≫ (K.extendXIso e hk'').inv = f'' :=
by
apply Cofork.IsColimit.hom_ext hcocone
rw [reassoc_of% hf', ← cancel_epi (extendXIso K e hj').hom, hf'', K.extend_d_eq e hj' hk'']
rw [← cancel_mono (K.extendXIso e hk'').inv, zero_comp, assoc, this]
· have h₁ : f' = 0 := by
apply Cofork.IsColimit.hom_ext hcocone
simp only [hf', comp_zero, K.shape _ _ hjk]
have h₂ : f'' = 0 := by
apply Cofork.IsColimit.hom_ext hcocone
rw [← cancel_epi (extendXIso K e hj').hom, hf'', comp_zero, comp_zero, K.extend_d_from_eq_zero e j' k' j hj']
rw [hk]
exact hjk
simp [h₁, h₂]
