English
Auxiliary lemma for lift_d_comp_eq_zero_iff: under certain shape-relations and kernels/cokernels in a left-homology data setup, the condition f' ≫ φ = 0 is equivalent to f'' ≫ φ = 0, given corresponding equations.
Русский
Вспомог lemma для lift_d_comp_eq_zero_iff: при определённых связях формы, ядра и котядра слева по гомологическим данным, равенство f' ≫ φ = 0 эквивалентно f'' ≫ φ = 0 при соответствующих уравнениях.
LaTeX
$$by_cases hij : c.Rel i j; ... (detailed equivalence between f' and f'' under kernels/cokernels and iso relations)$$
Lean4
/-- Auxiliary lemma for `lift_d_comp_eq_zero_iff`. -/
theorem lift_d_comp_eq_zero_iff' ⦃W : C⦄ (f' : K.X i ⟶ cone.pt) (hf' : f' ≫ cone.ι = K.d i j)
(f'' : (K.extend e).X i' ⟶ cone.pt) (hf'' : f'' ≫ cone.ι ≫ (extendXIso K e hj').inv = (K.extend e).d i' j')
(φ : cone.pt ⟶ W) : f' ≫ φ = 0 ↔ f'' ≫ φ = 0 :=
by
by_cases hij : c.Rel i j
· have hi'' : e.f i = i' := by rw [← hi', ← hj', c'.prev_eq' (e.rel hij)]
have : (K.extendXIso e hi'').hom ≫ f' = f'' :=
by
apply Fork.IsLimit.hom_ext hcone
rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'', K.extend_d_eq e hi'' hj']
rw [← cancel_epi (K.extendXIso e hi'').hom, comp_zero, ← this, assoc]
· have h₁ : f' = 0 := by
apply Fork.IsLimit.hom_ext hcone
simp only [zero_comp, hf', K.shape _ _ hij]
have h₂ : f'' = 0 := by
apply Fork.IsLimit.hom_ext hcone
dsimp
rw [← cancel_mono (extendXIso K e hj').inv, assoc, hf'', zero_comp, zero_comp,
K.extend_d_to_eq_zero e i' j' j hj']
rw [hi]
exact hij
simp [h₁, h₂]
