tensor_unit_d₂ — Mathlib

English

The d₂ boundary with tensor unit vanishes under appropriate hypotheses.

Русский

Грань d₂ для тензорной единицы обращается в ноль при подходящих гипотезах.

LaTeX

$$$ \operatorname{mapBifunctor}.d_2(K,\text{tensorUnit}(C,c)) = 0. $$$

Lean4

@[simp]
theorem tensor_unit_d₂ (i₁ i₂ j : I) : mapBifunctor.d₂ K (tensorUnit C c) (curriedTensor C) c i₁ i₂ j = 0 :=
  by
  by_cases h₁ : c.Rel i₂ (c.next i₂)
  · by_cases h₂ : ComplexShape.π c c c (i₁, c.next i₂) = j
    · rw [mapBifunctor.d₂_eq _ _ _ _ _ h₁ _ h₂, single_obj_d, Functor.map_zero, zero_comp, smul_zero]
    · rw [mapBifunctor.d₂_eq_zero' _ _ _ _ _ h₁ _ h₂]
  · rw [mapBifunctor.d₂_eq_zero _ _ _ _ _ _ _ h₁]

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