map₁_map₂ — Mathlib

English

A commuting square of arrows satisfies the compatibility: mapping through map₁ after map₂ equals mapping through map₂ after map₁.

Русский

Квадрат одинаковых стрелок удовлетворяет совместимости: применение map₁ затем map₂ равносильно применению map₂ затем map₁.

LaTeX

$$$ ((u.map_1 \epsilon h\epsilon).map_2 f hf) = ((u.map_2 f hf).map_1 \epsilon h\epsilon) $$$

Lean4

@[simp]
theorem map₁_map₂ {F G : Cᵒᵖ ⥤ Type v} {η : F ⟶ A} {μ : G ⟶ A} (ε : F ⟶ G) (hε : ε ≫ μ = η) {X Y : C}
    {s : yoneda.obj X ⟶ A} {t : yoneda.obj Y ⟶ A} (f : X ⟶ Y) (hf : yoneda.map f ≫ t = s) (u : OverArrows η t) :
    (u.map₁ ε hε).map₂ f hf = (u.map₂ f hf).map₁ ε hε :=
  OverArrows.ext <| (elementwise_of% (ε.naturality f.op).symm) u.val

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