ι_D₂ — Mathlib

English

The d₂ component equals epsilon₂ times the map derived from F and ι maps.

Русский

Компонента d₂ равна эпсилон₂ умноженной на отображение через F и ι-подобные карты.

LaTeX

$$d₂ K₁ K₂ F c i₁ i₂ j = ComplexShape.ε₂ c₁ c₂ c ⟨i₁, i₂⟩ • ((F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ ιMapBifunctor K₁ K₂ F c i₁ i₂' j h')$$

Lean4

@[reassoc (attr := simp)]
theorem ι_D₂ : ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ D₂ K₁ K₂ F c j j' = d₂ K₁ K₂ F c i₁ i₂ j' := by
  apply HomologicalComplex₂.ι_D₂

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