tensorHom_comp_tensorHom — Mathlib

English

The tensorHom operation on graded objects is compatible with composition: tensorHom f1 g1 followed by tensorHom f2 g2 equals tensorHom of the composed morphisms f1 ≫ f2 and g1 ≫ g2.

Русский

Операция tensorHom на градуированных объектах совместима с композиции: tensorHom f1 g1 затем tensorHom f2 g2 равняется tensorHom применённому к композициям f1 ≫ f2 и g1 ≫ g2.

LaTeX

$$$\tensorHom f_1 g_1 \; ⋅ \; \tensorHom f_2 g_2 = \tensorHom (f_1 ≫ f_2) (g_1 ≫ g_2).$$$

Lean4

@[reassoc]
theorem tensorHom_comp_tensorHom {X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂)
    (g₂ : Y₂ ⟶ Y₃) [HasTensor X₁ Y₁] [HasTensor X₂ Y₂] [HasTensor X₃ Y₃] :
    tensorHom f₁ g₁ ≫ tensorHom f₂ g₂ = tensorHom (f₁ ≫ f₂) (g₁ ≫ g₂) :=
  by
  dsimp only [tensorHom, mapBifunctorMapMap]
  rw [← mapMap_comp]
  apply congr_mapMap
  simp

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