map_w — Mathlib

English

For any cocone morphism f: c ⟶ c' and any j ∈ J, G.map (c.ι.app j) ≫ G.map f.hom = G.map (c'.ι.app j).

Русский

Для любого кокон-морфизма f: c ⟶ c' и любого j ∈ J выполнено: G.map (c.ι.app j) ∘ G.map f.hom = G.map (c'.ι.app j).

LaTeX

$$$\forall f:\, c \to c',\; \forall j:\, J,\; G.map (c.ι.app j) \;\circ\; G.map f.hom = G.map (c'.ι.app j)$$$

Lean4

@[reassoc (attr := simp)]
theorem map_w {c c' : Cocone F} (f : c ⟶ c') (G : C ⥤ D) (j : J) :
    G.map (c.ι.app j) ≫ G.map f.hom = G.map (c'.ι.app j) := by simp only [← map_comp, CoconeMorphism.w]

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