map₁_comp — Mathlib

English

map₂ respects composition: YonedaCollection.map₂ F (f ≫ g) equals YonedaCollection.map₂ F f composed with YonedaCollection.map₂ F g.

Русский

map₂ сохраняет композицию: map₂ F (f ≫ g) = map₂ F f ∘ map₂ F g.

LaTeX

$$$\\forall {f : X \\to Y} {g : Y \\to Z},\\; YonedaCollection.map₂ F (f ≫ g) = YonedaCollection.map₂ F f \\circ YonedaCollection.map₂ F g$$$

Lean4

@[simp]
theorem map₁_comp {G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (η : F ⟶ G) (μ : G ⟶ H) :
    YonedaCollection.map₁ (η ≫ μ) (X := X) = YonedaCollection.map₁ μ (X := X) ∘ YonedaCollection.map₁ η (X := X) := by
  ext; all_goals simp

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