unit_tensor_d₁ — Mathlib

English

The boundary map on d₂ with tensor unit is zero under appropriate hypotheses.

Русский

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

LaTeX

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

Lean4

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

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