English
Let i1, i2 be indices and i3, i3' be indices with c3.Rel i3 i3'. Then the third differential is given by an ε₂-scalar times the map induced by K3.d i3 i3' composed with the appropriate ι-Or-Zero inclusion.
Русский
Пусть i1, i2 — индексы, и i3, i3' — индексы с условием c3.Rel i3 i3'. Тогда третий дифференциал равен нормируемому множителю ε₂, умножающему отображение, индуцированное K3.d i3 i3', композиционному с правильной инклюзией ι^OrZero.
LaTeX
$$$ d_3 F_{1 2} G K_1 K_2 K_3 c_{1 2} c_4 i_1 i_2 i_3 j = \varepsilon_2 c_{1 2} c_3 c_4 (c_1.\pi c_2 c_{1 2} (i_1,i_2), i_3) \cdot (G.obj (F_{1 2}.obj (K_1.X i_1).obj (K_2.X i_2))).map (K_3.d i_3 i_3') \;\circ\; ι^{\mathrm{OrZero}}_{F_{1 2} G K_1 K_2 K_3 c_{1 2} c_4 i_1 i_2 i_3' j},$$$
Lean4
theorem d₃_eq (i₁ : ι₁) (i₂ : ι₂) {i₃ i₃' : ι₃} (h₃ : c₃.Rel i₃ i₃') (j : ι₄) :
d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
(ComplexShape.ε₂ c₁₂ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃)) •
(G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).map (K₃.d i₃ i₃') ≫ ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ _ j :=
by
obtain rfl := c₃.next_eq' h₃
rfl
