d₁_eq — Mathlib

English

The d1 expression for the symmetric triple bifunctor equals the explicit ε₁-ε₂ combination with the mapped differential and the connecting morphisms.

Русский

Выражение d1 для симметричного тройного бифунктора равняется явной комбинации ε₁-ε₂ с отображением дифференциала и соединяющими морфизмами.

LaTeX

$$$d_1 = (ε_2 \cdot ε_1) \circ (F\,\mapsto\text{differential}) \circ ι$$$

Lean4

theorem d₁_eq {i₁ i₁' : ι₁} (h₁ : c₁.Rel i₁ i₁') (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
    d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j =
      (ComplexShape.ε₁ c₁ c₂₃ c₄ (i₁, ComplexShape.π c₂ c₃ c₂₃ (i₂, i₃))) •
        ((F.map (K₁.d i₁ i₁'))).app ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ≫ ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ _ i₂ i₃ j :=
  by
  obtain rfl := c₁.next_eq' h₁
  rfl

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