d₁_eq_zero — Mathlib

English

The differential d1 in the composed bifunctor is equal to the explicit combination of ε₁-terms and the underlying maps, up to the appropriate associator and i-map components.

Русский

Дифференциал d1 в составном бифункторе равен явному сочетанию факторов ε₁ и соответствующих отображений, с учётом ассоциатора и i-мэп компонентов.

LaTeX

$$$d_1 = (\mathsf{ε}_1 \; \text{terms}) \cdot (F\,\mapsto\text{maps}) \cdot ι^{-1}$$$

Lean4

theorem d₁_eq_zero (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : ¬c₁.Rel i₁ (c₁.next i₁)) :
    d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j = 0 := by
  dsimp [d₁]
  rw [shape _ _ _ h, Functor.map_zero, zero_app, zero_comp, smul_zero]

Похожие утверждения