ι_mapBifunctorAssociatorX_hom — Mathlib

English

Compatibility of the associator with the ι maps in the first three levels of the bifunctor composition is enforced by a naturality-like identity.

Русский

Совместимость ассоциатора с картами ι на первых трёх уровнях композиции бифункторa задаётся натуралитной тождественностью.

LaTeX

$$$ι\_F G_{23} K_1 K_2 K_3 c \; i_1 \; i_2 \; i_3 \; j \; h = h$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_mapBifunctorAssociatorX_hom (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄)
    (h : ComplexShape.r c₁ c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
    mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫
        (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom =
      ((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃) ≫
        mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h :=
  by apply GradedObject.ι_mapBifunctorAssociator_hom

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