English
In the definition of the map bifunctor in a homological setting, the differential d2 is given by the explicit formula relating ε components, the functor maps, and the inclusion ι.
Русский
В определении двойного отображения для бифункторов в гомологической структуре дифференциал d2 задан явной формулой, связывающей ε-компоненты, отображения функторов и включение ι.
LaTeX
$$$d_2 F_{12} G K_1 K_2 K_3 c_{12} c_4 i_1 i_2 i_3 j = \left(c_{12}.\varepsilon_1 c_3 c_4 (\operatorname{ComplexShape.\pi} c_1 c_2 c_{12} \langle i_1,i_2\rangle, i_3) \cdot c_1.\varepsilon_2 c_2 c_{12} (i_1,i_2)\right) \bullet \left( G.map\left((F_{12}.obj (K_1.X i_1)).map (K_2.d i_2 i_2')\right)).app (K_3.X i_3) \circ \iota^{O} F_{12} G K_1 K_2 K_3 c_{12} c_4 i_1 _ i_3 j$$$
Lean4
theorem d₂_eq (i₁ : ι₁) {i₂ i₂' : ι₂} (h₂ : c₂.Rel i₂ i₂') (i₃ : ι₃) (j : ι₄) :
d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
(c₁₂.ε₁ c₃ c₄ (ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂⟩, i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)) •
(G.map ((F₁₂.obj (K₁.X i₁)).map (K₂.d i₂ i₂'))).app (K₃.X i₃) ≫ ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ _ i₃ j :=
by
obtain rfl := c₂.next_eq' h₂
rfl
