postcomp_map_heq' — Mathlib

English

If F = G as functors, then for any morphism f: X → Y, F.map f ≍ G.map f.

Русский

Если F = G как функторы, тогда для любого морфизма f: X → Y, F.map f ≍ G.map f.

LaTeX

$$$ F.map f \\mathrel{≍} G.map f $$$

Lean4

theorem postcomp_map_heq' (H : D ⥤ E) (hobj : ∀ X : C, F.obj X = G.obj X)
    (hmap : ∀ {X Y} (f : X ⟶ Y), F.map f ≍ G.map f) : (F ⋙ H).map f ≍ (G ⋙ H).map f := by
  rw [Functor.hext hobj fun _ _ => hmap]

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