map_map — Mathlib

English

For appropriate A1,B1, A2,B2, A3,B3 with binary products, and f,g,h,k as in the statement, we have map f g ≫ map h k = map (f ≫ h) (g ≫ k).

Русский

Для подходящих пар объектов и морфизмов выполняется map f g ≫ map h k = map (f ≫ h) (g ≫ k).

LaTeX

$$$prod.map f g \\circ prod.map h k = prod.map (f \\circ h) (g \\circ k)$$$

Lean4

@[reassoc (attr := simp)]
theorem map_map {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryProduct A₁ B₁] [HasBinaryProduct A₂ B₂] [HasBinaryProduct A₃ B₃]
    (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) : prod.map f g ≫ prod.map h k = prod.map (f ≫ h) (g ≫ k) :=
  by
  ext <;>
    simp
      -- TODO: is it necessary to weaken the assumption here?

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