English
A detailed compatibility relation holds between the left component and the null-homotopic map, relating it to the π-ι0 combination component: inlX K i j hij ≫ (nullHomotopicMap K).f j equals inlX K i j hij ≫ (π K ≫ ι0 K − id).f j.
Русский
Согласование левой компоненты с нулевой гомотопией: inlX K i j hij ≫ (nullHomotopicMap K).f j = inlX K i j hij ≫ ((π K) ≫ ι0 K − id).f j.
LaTeX
$$$inlX K i j hij \;≫\; (nullHomotopicMap K).f j = inlX K i j hij \;≫\; ((π K \gg ι_0 K) - \mathrm{Id}).f j$$$
Lean4
theorem inlX_nullHomotopy_f (i j : ι) (hij : c.Rel j i) :
inlX K i j hij ≫ (nullHomotopicMap K).f j = inlX K i j hij ≫ (π K ≫ ι₀ K - 𝟙 _).f j :=
by
dsimp [nullHomotopicMap]
by_cases hj : ∃ (k : ι), c.Rel k j
· obtain ⟨k, hjk⟩ := hj
simp only [assoc, Homotopy.nullHomotopicMap'_f hjk hij, homotopyCofiber_X, homotopyCofiber_d,
homotopyCofiber.d_sndX_assoc _ _ _ hij, add_comp, comp_add, homotopyCofiber.inlX_fstX_assoc,
homotopyCofiber.inlX_sndX_assoc, zero_comp, add_zero, comp_sub, inlX_π_assoc, comp_id, zero_sub,
← HomologicalComplex.comp_f_assoc, biprod.lift_snd, neg_f_apply, id_f, neg_comp, id_comp]
· simp only [not_exists] at hj
simp only [Homotopy.nullHomotopicMap'_f_of_not_rel_right hij hj, homotopyCofiber_X, homotopyCofiber_d, assoc,
comp_sub, comp_id, homotopyCofiber.d_sndX_assoc _ _ _ hij, add_comp, comp_add, zero_comp, add_zero,
homotopyCofiber.inlX_fstX_assoc, homotopyCofiber.inlX_sndX_assoc, ← HomologicalComplex.comp_f_assoc,
biprod.lift_snd, neg_f_apply, id_f, neg_comp, id_comp, inlX_π_assoc, zero_sub]
