hcongr_hom — Mathlib

English

If F = G as functors, then for any morphism f: X → Y, the equality of maps F.map f equals the composed map with eqToHom between F.obj X and G.obj X and between F.obj Y and G.obj Y holds.

Русский

Если F = G как функторы, то для любого f: X → Y равенство F.map f равно композиции с eqToHom между F.obj X и G.obj X и между F.obj Y и G.obj Y.

LaTeX

$$$ F.map f = eqToHom (congr_obj h X) \\; \\circ\\; G.map f \\; \\circ\\; eqToHom (congr_obj h Y)^{-1} $$$

Lean4

theorem hcongr_hom {F G : C ⥤ D} (h : F = G) {X Y} (f : X ⟶ Y) : F.map f ≍ G.map f := by rw [h]

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