associator_naturality — Mathlib

English

The associator for the chosen finite products is natural with respect to morphisms in each argument, ensuring a coherent rebracketing under maps.

Русский

Ассоциатор выбранных конечных произведений естественен по всем аргументам относительно морфизмов; сохраняется когерентность смены скобок.

LaTeX

$$$$ (BinaryFan.associatorOfLimitCone ℬ Y_1 Y_2 Y_3).hom \; ≈ \; (BinaryFan.associatorOfLimitCone ℬ X_1 X_2 X_3).hom $$$$

Lean4

theorem associator_naturality (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
    tensorHom ℬ (tensorHom ℬ f₁ f₂) f₃ ≫ (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom =
      (BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫ tensorHom ℬ f₁ (tensorHom ℬ f₂ f₃) :=
  by
  dsimp [tensorHom]
  apply (ℬ _ _).isLimit.hom_ext
  rintro ⟨_ | _⟩
  · simp
  apply (ℬ _ _).isLimit.hom_ext
  rintro ⟨_ | _⟩ <;> simp

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