map_comp_heq' — Mathlib

English

A variant of map_comp_heq that only requires a global pointwise equality of objects and a pointwise HEq of maps; then F.map (f ≫ g) ≍ G.map (f ≫ g).

Русский

Вариант map_comp_heq: требуется лишь глобальное по‑объектно равенство F.obj X = G.obj X и по‑морфизмному HEq равенство F.map f ≍ G.map f; тогда F.map (f ≫ g) ≍ G.map (f ≫ g).

LaTeX

$$$ (\\forall X, F.obj X = G.obj X) \\Rightarrow (\\forall f, F.map f \\approx G.map f) \\Rightarrow F.map (f ≫ g) \\mathrel{≍} G.map (f ≫ g) $$$

Lean4

theorem map_comp_heq' (hobj : ∀ X : C, F.obj X = G.obj X) (hmap : ∀ {X Y} (f : X ⟶ Y), F.map f ≍ G.map f) :
    F.map (f ≫ g) ≍ G.map (f ≫ g) := by rw [Functor.hext hobj fun _ _ => hmap]

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