ι_mapBifunctorDesc — Mathlib

English

If the π-shape and the relation h satisfy a certain condition, the d₂ component vanishes.

Русский

Если форма π и отношение h удовлетворяют условию, компонент d₂ равен нулю.

LaTeX

$$d₂ K₁ K₂ F c i₁ i₂ j = 0$$

Lean4

@[reassoc (attr := simp)]
theorem ι_mapBifunctorDesc (i₁ : I₁) (i₂ : I₂) (h : ComplexShape.π c₁ c₂ c ⟨i₁, i₂⟩ = j) :
    ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ mapBifunctorDesc f = f i₁ i₂ h := by apply HomologicalComplex₂.ι_totalDesc

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