ιMapBifunctor_hom₁ — Mathlib

English

The associator-compatible triple differential sums are compatible with each component's bifunctor maps.

Русский

Совместимая с ассоциатором тройная сумма дифференциалов согласуется с отображениями каждого компонента бифунктора.

LaTeX

$$$D_1 + D_2 + D_3$ compat with map$$

Lean4

@[reassoc]
theorem ιMapBifunctor_hom₁ (i₁ i₁' : I₁) (i₂ : I₂) (j j' : J) (h : ComplexShape.π c₁ c₂ c (i₁', i₂) = j)
    (h' : c₁.prev i₁' = i₁) :
    ιMapBifunctor K₁ K₂ F c i₁' i₂ j h ≫ hom₁ h₁ f₂ F c j j' =
      ComplexShape.ε₁ c₁ c₂ c (i₁, i₂) •
        (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
          (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ ιMapBifunctorOrZero L₁ L₂ F c _ _ j' :=
  by
  subst h'
  simp [hom₁]

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