English
The inclusion ι_D1 intertwines with the first differential, i.e., the composition of ι with D1 equals the corresponding d1 on the target side.
Русский
Инклюзия ι_D1 совместима с первым дифференциалом: композиция ι с D1 равна соответствующему d1 на целевой стороне.
LaTeX
$$$\iota_{F 12 G K_1 K_2 K_3 c_{1 2} c_4 i_1 i_2 i_3 j} \;\Rrightarrow\; D_1 F G K_1 K_2 K_3 c_{1 2} c_4 j j' = d_1 F G K_1 K_2 K_3 c_{1 2} c_4 i_1 i_2 i_3 j',$$$
Lean4
@[reassoc (attr := simp)]
theorem ιOrZero_mapBifunctorAssociatorX_hom (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j ≫
(mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom =
((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃) ≫
mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j :=
by
by_cases h : ComplexShape.r c₁ c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
·
rw [mapBifunctor₁₂.ιOrZero_eq _ _ _ _ _ _ _ _ _ _ _ h, mapBifunctor₂₃.ιOrZero_eq _ _ _ _ _ _ _ _ _ _ _ _ h,
ι_mapBifunctorAssociatorX_hom]
·
rw [mapBifunctor₁₂.ιOrZero_eq_zero _ _ _ _ _ _ _ _ _ _ _ h,
mapBifunctor₂₃.ιOrZero_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h, zero_comp, comp_zero]
