English
A symmetric compatibility for the right component and the null-homotopic map: for each j, inrX K j ≫ (nullHomotopicMap K).f j = inrX K j ≫ (π K ≫ ι0 K − id).f j.
Русский
Симметричное свойство для правой компоненты и нулевой гомотопии: ∀ j, inrX K j ≫ (nullHomotopicMap K).f j = inrX K j ≫ (π K ≫ ι0 K − Id).f j.
LaTeX
$$$inrX K j \;≫\; (nullHomotopicMap K).f j = inrX K j \;≫\; ((π K) \gg ι_0 K - Id).f j$$$
Lean4
theorem inrX_nullHomotopy_f (j : ι) : inrX K j ≫ (nullHomotopicMap K).f j = inrX K j ≫ (π K ≫ ι₀ K - 𝟙 _).f j :=
by
have : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr := biprod.hom_ext _ _ (by simp) (by simp)
obtain ⟨i, hij⟩ := hc j
dsimp [nullHomotopicMap]
by_cases hj : ∃ (k : ι), c.Rel j k
· obtain ⟨k, hjk⟩ := hj
simp only [Homotopy.nullHomotopicMap'_f hij hjk, homotopyCofiber_X, homotopyCofiber_d, assoc, comp_add,
homotopyCofiber.inrX_d_assoc, homotopyCofiber.inrX_sndX_assoc, comp_sub, inrX_π_assoc, comp_id, ← Hom.comm_assoc,
homotopyCofiber.inlX_d _ _ _ _ _ hjk, comp_neg, add_neg_cancel_left]
rw [← cancel_epi (biprodXIso K K j).inv]
ext
· simp [ι₀]
· dsimp
simp only [inr_biprodXIso_inv_assoc, biprod_inr_snd_f_assoc, comp_sub, biprod_inr_desc_f_assoc, id_f, id_comp, ι₀,
comp_f, this, sub_f_apply, sub_comp, homotopyCofiber_X, homotopyCofiber.inr_f]
· simp only [not_exists] at hj
simp only [assoc, Homotopy.nullHomotopicMap'_f_of_not_rel_left hij hj, homotopyCofiber_X, homotopyCofiber_d,
homotopyCofiber.inlX_d' _ _ _ _ (hj _), homotopyCofiber.inrX_sndX_assoc, comp_sub, inrX_π_assoc, comp_id, ι₀,
comp_f, homotopyCofiber.inr_f]
rw [← cancel_epi (biprodXIso K K j).inv]
ext
· simp
· simp [this]
